The Structural Theory of Pure Type Systems

Date

July 31, 2013

Speaker

Cody Roux

Affiliation

Carnegie Mellon University

Overview

By an analysis of the global structure of the set of pure type systems (PTS), we identify and classify various transformations of PTS which preserve
normalization. In particular we identify predicative quantification and the Q-logic of P terms to be two interesting examples of such transformations

Speakers

Cody Roux

Cody Roux is a postdoc in the Philosophy Department at Carnegie Mellon University, Pittsburgh, working on Type Theory and Theorem Proving. Formerly he was at INRIA Saclay/Universite Pierre et Marie Curie working on “An Axiomatic Theory of Floating Point Numbers in SMT”. Cody Roux did his undergraduate studies in mathematics at Joseph Fourier in Grenoble, France, and the Dieudonne institute in Nice. He received a PhD in Computer Science at the Henri Poincare University in Nancy. For more information, visit his website: http://www.andrew.cmu.edu/user/croux/