 |
 |
 |
 |
|
|
||
|---|---|---|
|
hal-00730913v1
Communication dans un congrès
Chantal Keller, Marc Lasson. Parametricity in an Impredicative Sort Patrick Cégielski and Arnaud Durand. CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012, Sep 2012, Fontainebleau, France. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 16, pp.381-395, 2012, CSL. <10.4230/LIPIcs.CSL.2012.399> |
||
|
hal-00757620v1
Communication dans un congrès
Chantal Keller, Marc Lasson. The Refined Calculus of Inductive Construction: Parametricity and Abstraction LICS - 27th Annual IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnik, Croatia. 2012 |
||
|
inria-00520604v1
Communication dans un congrès
Chantal Keller, Benjamin Werner. Importing HOL Light into Coq Matt Kaufmann and Lawrence C. Paulson. ITP - Interactive Theorem Proving, First International Conference - 2010, Jul 2010, Edimbourg, United Kingdom. Springer, 6172, pp.307-322, 2010, Lecture Notes in Computer Science; Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. <http://www.springerlink.com/content/a74714134ut7316n/> |
||
|
inria-00520606v1
Communication dans un congrès
Chantal Keller, Thorsten Altenkirch. Hereditary Substitutions for Simple Types, Formalized Capretta, V. and Chapman, J. MSFP - Third Workshop on Mathematically Structured Functional Programming - 2010, Sep 2010, Baltimore, United States. ACM Press, 2010, Proceedings of the Mathematically Structured Functional Programming workshop, ACM Press 2010, Baltimore, Marylan, USA, September 25, 2010 |
||
|
|
||
