Cody Roux

Info

I am currently a Postdoc in the Philosophy Department at Carnegie Mellon University, working on topics related to type theory.

I was previously in the Proval INRIA team, working on the Alt-Ergo theorem prover; and before that, I was a PhD student in the Pareo INRIA team, under the direction of Claude Kirchner and Frederic Blanqui.

Teaching

• Constructive Type Theory
• Introduction to Logic and Mathematical Reasoning

PhD

Type Based Termination: Semantics and Generalizations. In English, with introduction in French.

Publications in the proceedings of international conferences

• Size Based Termination as Semantic Labeling. with Frédéric Blanqui, in Computer Science and Logic, 2009.
• Refinement Types as Higher Order Dependency Pairs in Rewriting Techniques and Applications, 2011.

Publications in workshops

• Built-In Treatment of an Axiomatic Floating-Point Theory for SMT Solvers with Sylvain Conchon, Guillaume Melquiond and Mohammed Iguernelala, in SMT Workshop 2012.
• Types Simples, Logique et Coercions Implicites, in Journées Francophones des Langages Applicatifs 2008.

Other Stuff

1. Some (very modest!) Coq developments:
   • Normalization by evaluation in a free monoid as explained by P. Dybjer
   • System F in coq
   • Type correctness of a tiny pattern matching language