The Structural Theory of Pure Type Systems


July 31, 2013


Cody Roux


Carnegie Mellon University


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


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: