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