Associate Adjunct Professor -- CMU Philosophy Department.
The Structural Theory of Pure Type Systems
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.
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
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.
Friday, February 28, 2014
& Hillman Centers 6501
of Programming Seminars