Principles of Programming Seminar (POP)

Seminars
CODY ROUX
Associate Adjunct Professor
Department of Philosophy
Carnegie Mellon University
The Structural Theory of Pure Type Systems
Friday, February 28, 2014 - 1:30pm to 3:00pm
Traffic21 Classroom 6501 
Gates&Hillman Centers
Abstract:

We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union P+Q of two PTSs P and Q, the PTS \forall P.Q which intuitively captures the "Q logic of P-terms'" and Ppoly which intuitively denotes the predicative polymorphism extension of P.

***

Cody Roux did his undergraduate at Grenoble and Nice in the south of France, and completed his PhD in computer science at Nancy in the north-east, on the subject of higher-order rewrite systems. Cody did a post-doc at Inria Saclay in Paris on formal verification of floating-point numbers, and is now an Associate Adjunct Professor at CMU, in the philosophy department. He works mostly on formal proofs, type theory and automated reasoning.

Keywords:
For More Information, Please Contact:

dcm [atsymbol] cs ~replace-with-a-dot~ cmu ~replace-with-a-dot~ edu