Cody Roux
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.