The Structural Theory of Pure Type Systems

  • 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

Speaker Details

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/

Series: Microsoft Research Talks