FacebookTwitterGoogle PlusRSS News Feed

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