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