Associate Adjunct Professor -- CMU Philosophy Department.

The Structural Theory of Pure Type Systems

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.

These results suggest a new approach to the study of the meta-theory of PTSs, by examination of the relationships between different calculi and predicative extensions which allow more expressiveness with equivalent logical strength.

Bio:

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

Principles
of Programming Seminars