[Colloquium] Nathan Mull Candidacy Exam/Jun 6, 2022

[Megan Woodward]

This is an announcement of Nathan Mull's Candidacy Exam.
===============================================
Candidate: Nathan Mull

Date: Monday, June 06, 2022

Time:  2 pm CST

Location: JCL 298

Title: On Normalization for Pure Type Systems

Abstract: A type system exhibits weak normalization if all typeable terms have normal forms, and strong normalization if no typable term appears in an infinite reduction sequence. Strong normalization is often difficult to prove, so techniques have been developed to infer strong normalization from weak normalization. The Barendregt-Geuvers-Klop conjecture posits that this is possible in a wide setting, that weak normalization implies strong normalization for pure type systems, a class of systems that contains the lambda cube and generalizes it by providing more freedom in the dependencies for abstraction. In this presentation, I'll give an overview of techniques for proving normalization for pure type systems, as well as the state of affairs for this conjecture, with an eye toward which techniques may be amenable to generalization to subclasses of pure type systems.

Advisors: Stuart Kurtz

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