<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">This is an announcement of Nathan Mull's Dissertation Defense.<br>
===============================================<br>
Candidate: Nathan Mull<br>
<br>
Date: Tuesday, May 16, 2023<br>
<br>
Time: 3:30 pm CST<br>
<br>
Location: JCL 298<br>
<br>
Title: Weak and Strong Normalization of Tiered Pure Type Systems via Type-Preserving Translation<br>
<br>
Abstract: A type system is weakly normalizing if every typable expression has a normal<br>
form, and is strongly normalizing if no typable expression appears in an<br>
infinite reduction sequence. The Barendregt-Geuvers-Klop conjecture asks if<br>
weak normalization implies strong normalization for all pure type systems, a<br>
class of systems which generalizes the lambda cube. There are two natural<br>
techniques based on type-preserving translations for proving strong<br>
normalization from weak normalization. The first is to define a translation to<br>
I-expressions (i.e., expressions in which lambda bound variables must be used).<br>
Strong normalization then readily follows from weak normalization by a<br>
conservation result along the lines of the one proved by Church for the untyped<br>
lambda calculus. The second technique is to define an infinite-reduction-path<br>
preserving translation to a weak sub-system for which the conjecture is known<br>
to hold. By a straightforward boot-strapping argument, the conjecture can be<br>
shown to hold for the full system.<br>
<br>
I present three translations, one of the first form and two of the second form.<br>
The first is a generalization of the thunkification translation of Xi, which<br>
translates to I-expressions using a new padding scheme, leading to fewer<br>
technical restrictions on the class of systems to which it applies. The second<br>
is a generalization of the dependency-eliminating translation of Geuvers and<br>
Nederhof to a class of pure type systems which are known to be strongly<br>
normalizing, but for which the stronger form of the conjecture is demonstrated<br>
for the first time. The third is a novel application of ideas of Roux and van<br>
Doorn for a class of pure type systems with “irrelevant" structure, extending<br>
the conjecture to a larger class of system with properties like dependent types<br>
(albeit, a very weak notion of dependent types) which have not appeared in any<br>
of the classes of systems previously considered.<br>
<br>
All of this work is done in the framework of tiered pure type systems, a simple<br>
class of persistent pure type systems which are concretely specified but<br>
sufficient to study in most cases regarding questions of normalization. I<br>
consider the introduction of this class of systems one of the more important<br>
contributions of this work, as its combinatorial nature makes it easier to<br>
study than previously considered classes of systems.<br>
<br>
Advisors: Stuart Kurtz<br>
<br>
Committee Members: John Reppy, Stuart Kurtz, and Robert Rand<br>
<br>
<br>
</div>
</span></font></div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText"><br>
<br>
</div>
</span></font></div>
</body>
</html>