[Colloquium] Nathan Mull Dissertation Defense/May 16, 2023

[Megan Woodward]

This is an announcement of Nathan Mull's Dissertation Defense.
===============================================
Candidate: Nathan Mull

Date: Tuesday, May 16, 2023

Time:  3:30 pm CST

Location: JCL 298

Title: Weak and Strong Normalization of Tiered Pure Type Systems via Type-Preserving Translation

Abstract: A type system is weakly normalizing if every typable expression has a normal
form, and is strongly normalizing if no typable expression appears in an
infinite reduction sequence.  The Barendregt-Geuvers-Klop conjecture asks if
weak normalization implies strong normalization for all pure type systems, a
class of systems which generalizes the lambda cube.  There are two natural
techniques based on type-preserving translations for proving strong
normalization from weak normalization.  The first is to define a translation to
I-expressions (i.e., expressions in which lambda bound variables must be used).
Strong normalization then readily follows from weak normalization by a
conservation result along the lines of the one proved by Church for the untyped
lambda calculus.  The second technique is to define an infinite-reduction-path
preserving translation to a weak sub-system for which the conjecture is known
to hold.  By a straightforward boot-strapping argument, the conjecture can be
shown to hold for the full system.

I present three translations, one of the first form and two of the second form.
The first is a generalization of the thunkification translation of Xi, which
translates to I-expressions using a new padding scheme, leading to fewer
technical restrictions on the class of systems to which it applies.  The second
is a generalization of the dependency-eliminating translation of Geuvers and
Nederhof to a class of pure type systems which are known to be strongly
normalizing, but for which the stronger form of the conjecture is demonstrated
for the first time.  The third is a novel application of ideas of Roux and van
Doorn for a class of pure type systems with “irrelevant" structure, extending
the conjecture to a larger class of system with properties like dependent types
(albeit, a very weak notion of dependent types) which have not appeared in any
of the classes of systems previously considered.

All of this work is done in the framework of tiered pure type systems, a simple
class of persistent pure type systems which are concretely specified but
sufficient to study in most cases regarding questions of normalization.  I
consider the introduction of this class of systems one of the more important
contributions of this work, as its combinatorial nature makes it easier to
study than previously considered classes of systems.

Advisors: Stuart Kurtz

Committee Members: John Reppy, Stuart Kurtz, and Robert Rand




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20230502/929cafeb/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: main.pdf
Type: application/pdf
Size: 751137 bytes
Desc: main.pdf
URL: <http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20230502/929cafeb/attachment-0001.pdf>