Nombre de documents

9

CV de Pierre Letouzey


Article dans une revue1 document

  • Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg. Program extraction from normalization proofs. Studia Logica, Springer Verlag (Germany), 2006, 82 (1), pp.25-49. <10.1007/s11225-006-6604-5>. <hal-00150904>

Thèse1 document

  • Pierre Letouzey. Programmation fonctionnelle certifiée :
    L'extraction de programmes dans l'assistant Coq. Autre [cs.OH]. Université Paris Sud - Paris XI, 2004. Français. <tel-00150912>

Communication dans un congrès5 documents

  • Pierre Letouzey. Extraction in Coq, an Overview. Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, Jun 2008, Athens, Greece. Springer-Verlag, 5028, 2008, Lecture Notes in Computer Science. <10.1007/978-3-540-69407-6>. <hal-00338973>
  • Luís Cruz-Filipe, Pierre Letouzey. A Large-Scale Experiment in Executing Extracted Programs. F.J. López Fraguas. Calculemus 2005, Mar 2006, Newcastle upon Tyne, United Kingdom. Elsevier, pp.75-91, 2006, Electronic Notes in Theoretical Computer Science. <10.1016/j.entcs.2005.11.024>. <hal-00150908>
  • Jean-Christophe Filliâtre, Pierre Letouzey. Functors for Proofs and Programs. D. Schmidt. 13th European Symposium on Programming, ESOP 2004, Feb 2004, Barcelona, Spain. Springer, pp.370-384, 2004, Lecture Notes in Computer Science. <10.1007/b96702>. <hal-00150913>
  • Pierre Letouzey. A New Extraction for Coq. Herman Geuvers and Freek Wiedijk. Types for Proofs and Programs: International Workshop, TYPES 2002, Feb 2004, Berg en Dal, Netherlands. Springer, pp.617, 2004, Lecture Notes in Computer Science. <hal-00150914>
  • Pierre Letouzey, Laurent Théry. Formalizing Stalmarck's algorithm in Coq. Aagaard, Mark; Harrison, John. Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, 2000, Portland, United States. springer, pp.388, 2000, Lecture Notes in Computer Science, Vol. 1869. <hal-00150915>

Pré-publication, Document de travail1 document

  • Pierre Letouzey, Bas Spitters. Implicit and noncomputational arguments using monads. 2005. <hal-00150900>

Rapport1 document

  • Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, et al.. Coq 8.4 Reference Manual. [Research Report] Inria. 2014. <hal-01114602>