Equipe de recherche PI.R2

Publications de l'équipe PI.R2

2014

Communications avec actes

Titre
Universe Polymorphism in Coq
Auteurs
Matthieu Sozeau; Nicolas Tabareau
Détail
Interactive Theorem Proving, Jul 2014, Vienna, Austria.
Accès au bibtex
BibTex
Titre
The duality of construction
Auteurs
Paul Downen url; Zena Ariola url
Détail
ESOP 2014 : European Symposium on Programming, Apr 2014, Grenoble, France. European Symposium on Programming (ESOP), 15 p.
Accès au bibtex
BibTex

Documents sans référence de publication

Titre
Polygraphs of finite derivation type
Auteurs
Yves Guiraud url; Philippe Malbos url
Détail
Jan. 2014. 46 pages
Accès au texte intégral et bibtex
ihdr.pdf BibTex

2013

Articles dans des revues avec comité de lecture

Titre
Certifying and reasoning about cost annotations of functional programs
Auteurs
Roberto M. Amadio; Yann Régis-Gianas
Détail
Higher-Order and Symbolic Computation, Springer, 2013
Accès au texte intégral et bibtex
main.pdf main.ps BibTex

Communications avec actes

Titre
Lightweight proof by reflection using a posteriori simulation of effectful computation
Auteurs
Guillaume Claret; Lourdes Del Carmen Gonzalez Huesca; Yann Régis-Gianas url; Beta Ziliani
Détail
Interactive Theorem Proving, Jul 2013, Rennes, France.
Accès au texte intégral et bibtex
simulation-based-pbr-final.pdf BibTex
Titre
A Homotopical Completion Procedure with Applications to Coherence of Monoids
Auteurs
Yves Guiraud url; Philippe Malbos url; Samuel Mimram url
Détail
Van Raamsdonk, Femke. RTA - 24th International Conference on Rewriting Techniques and Applications - 2013, Jun 2013, Eindhoven, Netherlands. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 21, pp. 223-238, Leibniz International Proceedings in Informatics (LIPIcs)
Accès au texte intégral et bibtex
rta13FinalLong.pdf BibTex
Titre
Un régime au concentré d'automate
Auteurs
Pierre-Marie Pédrot
Détail
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France.
Accès au texte intégral et bibtex
jfla2013-10.pdf BibTex
Titre
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
Auteurs
Bruno Barras; Lourdes Del Carmen Gonzalez Huesca; Hugo Herbelin; Yann Régis-Gianas; Enrico Tassi; Makarius Wenzel; Burkhart Wolff
Détail
MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp. 359-363
Accès au bibtex
BibTex

Ouvrages scientifiques

Titre
Homotopy Type Theory: Univalent Foundations of Mathematics
Auteurs
Peter Aczel; Benedikt Ahrens; Thorsten Altenkirch; Steve Awodey; Bruno Barras; Andrej Bauer; Yves Bertot; Marc Bezem; Thierry Coquand; Eric Finster; Daniel Grayson; Hugo Herbelin; André Joyal; Dan Licata; Peter Lumsdaine; Assia Mahboubi; Per Martin-Löf; Sergey Melikhov; Alvaro Pelayo; Andrew Polonsky; Michael Shulman; Matthieu Sozeau; Bas Spitters; Benno Van Den Berg; Vladimir Voevodsky; Michael Warren; Carlo Angiuli; Anthony Bordg; Guillaume Brunerie; Chris Kapulkin; Egbert Rijke; Kristina Sojakova; Jeremy Avigad; Cyril Cohen; Robert Constable; Pierre-Louis Curien; Peter Dybjer; Martín Escardó; Kuen-Bang Hou; Nicola Gambino; Richard Garner; Georges Gonthier; Thomas Hales; Robert Harper; Martin Hofmann; Pieter Hofstra; Joachim Koch; Nicolai Kraus; Nuo Li; Zhaohui Luo; Michael Nahas; Erik Palmgren; Emily Riehl; Dana Scott; Philip Scott; Sergei Soloviev
Détail
Aucun, pp. 448, 2013
Accès au bibtex
BibTex

Chapitres d'ouvrages scientifiques

Titre
Identities among relations for higher-dimensional rewriting systems
Auteurs
Yves Guiraud url; Philippe Malbos
Détail
Operads 2009, 26, Société Mathématique de France, pp. 145-161, 2013, Séminaires et Congrès
Accès au texte intégral et bibtex
niar.pdf BibTex

Thèses

Titre
Syntaxe et modèles d'une composition non-associative des programmes et des preuves
Auteurs
Guillaume Munch-Maccagnoni url
Détail
informatique. Université Paris-Diderot - Paris VII, Dec. 2013. English
Accès au texte intégral et bibtex
these-screen-final.pdf BibTex

Documents sans référence de publication

Titre
Simple simpl
Auteurs
Pierre Boutillier
Détail
Mar. 2013
Accès au texte intégral et bibtex
ITP13_Boutillier.pdf ITP13_Boutillier.ps BibTex
Titre
A dependently-typed construction of semi-simplicial types
Auteurs
Hugo Herbelin url
Détail
Mar. 2013
Accès au texte intégral et bibtex
simplicial-revise-final.pdf BibTex
Titre
Univalence for free
Auteurs
Matthieu Sozeau; Nicolas Tabareau url
Détail
Feb. 2013
Accès au texte intégral et bibtex
main.pdf BibTex

2012

Articles dans des revues avec comité de lecture

Titre
Delimited control operators prove Double-negation Shift
Auteurs
Danko Ilik
Détail
Annals of Pure and Applied Logic, Elsevier, 2012, Kurt Goedel Research Prize Fellowships 2010, 163 (11), pp. 1549-1559
Accès au texte intégral et bibtex
article.pdf article.ps BibTex
Titre
Böhm theorem and Böhm trees for the Lambda-mu-calculus
Auteurs
Alexis Saurin url
Détail
Theoretical Computer Science, 2012, 435, pp. 106-138
Accès au bibtex
BibTex
Titre
Continuation-passing Style Models Complete for Intuitionistic Logic
Auteurs
Danko Ilik
Détail
Annals of Pure and Applied Logic, Elsevier, 2012
Accès au texte intégral et bibtex
intcomp.pdf intcomp.ps BibTex
Titre
Pure Type System conversion is always typable
Auteurs
Vincent Siles; Hugo Herbelin
Détail
Journal of Functional Programming, Cambridge Journals, 2012, 22 (2), pp. 153 - 180
Accès au texte intégral et bibtex
PTSATR.pdf BibTex
Titre
Partiality and Recursion in Interactive Theorem Provers - An Overview
Auteurs
Ana Bove; Alexander Krauss; Matthieu Sozeau url
Détail
Mathematical Structures in Computer Science, CUP, 2012
Accès au texte intégral et bibtex
main.pdf BibTex
Titre
Coherence in monoidal track categories
Auteurs
Yves Guiraud; Philippe Malbos
Détail
Mathematical Structures in Computer Science, 2012, 22 (6), pp. 931-969
Accès au texte intégral et bibtex
cohe.pdf BibTex
Titre
Higher-dimensional normalisation strategies for acyclicity
Auteurs
Yves Guiraud; Philippe Malbos url
Détail
Advances in Mathematics, 2012, 231 (3-4), pp. 2294-2351
Accès au texte intégral et bibtex
ktheory.pdf BibTex

Conférences invitées

Titre
Coq avec Classes
Auteurs
Matthieu Sozeau url
Détail
JFLA - Journées Françaises des Langages Applicatifs, Feb 2012, Carnac, France.
Accès au bibtex
BibTex
Titre
Operads, clones, and distributive laws
Auteurs
Pierre-Louis Curien
Détail
Chengming Bai, Li Guo and Jean-Louis Loday. Operads and Universal Algebra : Proceedings of China-France Summer Conference, Jul 2010, Tianjin, China. World Scientific, Proceedings of the International Conference on Operads and Universal Algebra, pp. 25-50, 2012, Nankai Series in Pure, Applied Mathematics and Theoretical Physics, Vol. 9
Accès au texte intégral et bibtex
Operads-PLC.pdf Operads-PLC.ps BibTex

Communications avec actes

Titre
Certifying and reasoning on cost annotations in C programs
Auteurs
Nicolas Ayache; Roberto Amadio; Yann Régis-Gianas
Détail
FMICS 2012 - 17th International Workshop on Formal Methods for Industrial Critical Systems, Aug 2012, Paris, France.
Accès au texte intégral et bibtex
ccac-fmics-final.pdf BibTex
Titre
Extending Type Theory with Forcing
Auteurs
Guilhem Jaber; Nicolas Tabareau; Matthieu Sozeau
Détail
LICS 2012 : Logic In Computer Science, Jun 2012, Dubrovnik, Croatia. Proceedings of LICS'12, pp. 0-0
Accès au texte intégral et bibtex
forcing_lics.pdf BibTex
Titre
A relaxation of Coq's guard condition
Auteurs
Pierre Boutillier url
Détail
JFLA - Journées Francophones des langages applicatifs - 2012, Feb 2012, Carnac, France. Actes des Journées Francophones des langages Applicatifs, pp. 1 - 14
Accès au texte intégral et bibtex
boutillier.pdf boutillier.ps BibTex
Titre
A Constructive Proof of Dependent Choice, Compatible with Classical Logic
Auteurs
Hugo Herbelin url
Détail
LICS 2012 - 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2012, Dubrovnik, Croatia. IEEE Computer Society, Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, 25-28 June 2012, Dubrovnik, Croatia, pp. 365-374
Accès au texte intégral et bibtex
Herbelin-lics12.pdf BibTex
Titre
Classical call-by-need sequent calculi : The unity of semantic artifacts
Auteurs
Zena Ariola; Paul Downen; Hugo Herbelin url; Keiko Nakata url; Alexis Saurin
Détail
Tom Schrijvers and Peter Thiemann. FLOPS 2012 - 11th International Symposium on Functional and Logic Programming, May 2012, Kobe, Japan. Springer, Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, 7294, pp. 32-46, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
classical-need-artifacts.pdf BibTex

Communications sans actes

Titre
Safe Incremental Type Checking
Auteurs
Matthias Puech url; Yann Régis-Gianas url
Détail
TLDI 2012 - Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation, Jan 2012, Philadelphia, United States.
Accès au texte intégral et bibtex
abstract.pdf BibTex

Rapports

Titre
Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability
Auteurs
Federico Aschieri url; Margherita Zorzi
Détail
[Technical Report], 2012
Accès au texte intégral et bibtex
ConservativeSKFull.pdf ConservativeSKFull.ps BibTex
Titre
Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms
Auteurs
Federico Aschieri url
Détail
[Technical Report], 2012
Accès au texte intégral et bibtex
RealizabilityPAfull.pdf RealizabilityPAfull.ps BibTex

Autres publications

Titre
Forcing in Coq
Auteurs
Matthieu Sozeau url; Nicolas Tabareau; Guilhem Jaber
Détail
Sep. 2012. A plugin for Coq that implements a generic Forcing translation for any given set of conditions. Includes an example of a step-indexed model of pure lambda calculus.
Accès au bibtex
BibTex
Titre
A gentle introduction to type classes and relations in Coq
Auteurs
Pierre Castéran url; Matthieu Sozeau
Détail
May. 2012. This document presents the main features of type classes and user-defined relations in the Coq proof assistant. Available at http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf
Accès au bibtex
BibTex

Documents sans référence de publication

Titre
Coherent presentations of Artin groups
Auteurs
Stéphane Gaussent url; Yves Guiraud url; Philippe Malbos url
Détail
Mar. 2012. 68 pages
Accès au texte intégral et bibtex
polycox.pdf BibTex
Titre
Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1
Auteurs
Federico Aschieri url
Détail
Jan. 2012
Accès au texte intégral et bibtex
RealizersHASEM1final.pdf RealizersHASEM1final.ps BibTex

2011

Articles dans des revues avec comité de lecture

Titre
Preface to Girard's Festschrift
Auteurs
Pierre-Louis Curien
Détail
Theoretical Computer Science, 2011, 412 (20), pp. 1853-1859
Accès au texte intégral et bibtex
girard-preface.pdf girard-preface.ps BibTex

Communications avec actes

Titre
Classical Call-by-need and duality
Auteurs
Zena Ariola; Hugo Herbelin; Alexis Saurin
Détail
C.-H. Luke Ong. TLCA 2011 - Typed Lambda Calculi and Applications, Jun 2011, Novi Sad, Serbia. Springer, Typed Lambda Calculi and Applications - 10th International Conference, 6690, pp. 27-44, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
tlca.pdf BibTex
Titre
On the Meaning of Focalization
Auteurs
Alexis Saurin; Michele Basaldella; Kazushige Terui
Détail
Lecomte and Tronçon. workshop on Games, Dialog and Interaction, Sep 2009, Paris, France. Springer-Verlag, PRELUDE 2010, 6505, pp. 78-87, 2011, LNAI
Accès au bibtex
BibTex

2010

Articles dans des revues avec comité de lecture

Titre
Kripke Models for Classical Logic
Auteurs
Danko Ilik; Gyesik Lee; Hugo Herbelin
Détail
Annals of Pure and Applied Logic, Elsevier, 2010, Special Issue: Classical Logic and Computation (2008), 161 (11), pp. 1367-1378
Accès au texte intégral et bibtex
classical_kripke_rev3.pdf classical_kripke_rev3.ps BibTex
Titre
Typing streams in the $\Lambda\mu$-calculus
Auteurs
Alexis Saurin
Détail
ACM Transactions on Computational Logic, 2010, 11 (4), pp. 28-61
Accès au bibtex
BibTex
Titre
Proof and Refutation in MALL as a game
Auteurs
Olivier Delande; Dale Miller; Alexis Saurin
Détail
Annals of Pure and Applied Logic, 2010, 161 (5), pp. 654-672
Accès au bibtex
BibTex

Conférences invitées

Titre
Elaborations in Type Theory
Auteurs
Matthieu Sozeau url
Détail
DTP'10 - Dependently Typed Programming - 2010, Jul 2010, Edinburgh, United Kingdom.
Accès au bibtex
BibTex

Communications avec actes

Titre
Equality is typable in Semi-Full Pure Type Systems
Auteurs
Vincent Siles; Hugo Herbelin
Détail
Logic In Computer Science - LICS 2010, Jul 2010, Edinburgh, United Kingdom. Logic In Computer Science, 10 p.
Accès au texte intégral et bibtex
herbelin.siles.LICS2010.pdf BibTex
Titre
From Focalization of Logic to the Logic of Focalization
Auteurs
Michele Basaldella; Alexis Saurin; Kazushige Terui
Détail
Twenty-Sixth Conference on the Mathematical Foundations of Programming Semantics - MFPS XXVI, May 2010, Ottawa, Canada. Proceedings of the Twenty-Sixth Conference on the Mathematical Foundations of Programming Semantics - MFPS XXVI, pp. 161-176, Electronic Notes Theoretical Computer Science
Accès au bibtex
BibTex
Titre
A Hierarchy for Delimited Continuations in Call-by-Name
Auteurs
Alexis Saurin
Détail
13th International Conference on Software Science and Computational Structures - FOSSACS 2010, Mar 2010, Paphos, Cyprus. Springer, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, 6014, pp. 374-388, Lecture notes in computer science
Accès au bibtex
BibTex
Titre
Standardization and Böhm Trees for $\Lambda\mu$-Calculus
Auteurs
Alexis Saurin
Détail
Tenth International Symposium on Functional and Logic Programming - FLOPS 2010, Apr 2010, Sendai, Japan. Springer, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings, 6009, pp. 134-149, Lecture notes in computer science
Accès au bibtex
BibTex
Titre
Polarity and the Logic of Delimited Continuations
Auteurs
Noam Zeilberger
Détail
25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Jul 2010, Edinburgh, United Kingdom. Polarity and the Logic of Delimited Continuations, pp. 219 - 227
Accès au bibtex
BibTex
Titre
An intuitionistic logic that proves Markov's principle
Auteurs
Hugo Herbelin
Détail
Logic In Computer Science, Jul 2010, Edinburgh, United Kingdom. IEEE Computer Society, Proceedings, 25th Annual IEEE Symposium on Logic in Computer Science (LICS '10), Edinburgh, UK, 11-14 July 2010, pp. 50-56
Accès au texte intégral et bibtex
herbelin.LICS2010.pdf BibTex
Titre
The duality of computation under focus
Auteurs
Pierre-Louis Curien; Guillaume Munch-Maccagnoni
Détail
IFIP International Conference on Theoretical Computer Science, Sep 2010, Brisbane, Australia. Springer Verlag, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
TCS-2010.pdf TCS-2010.ps BibTex

Communications sans actes

Titre
Towards typed repositories of proofs
Auteurs
Matthias Puech; Yann Regis-Gianas
Détail
Mathematically Intelligent Proof Search - MIPS 2010, Jul 2010, Paris, France.
Accès au texte intégral et bibtex
puech-regis-gianas-mips-2010.pdf BibTex

Thèses

Titre
Etude sur le typage de l'égalité dans les systèmes de types
Auteurs
Vincent Siles
Détail
Informatique. Ecole Polytechnique X, Nov. 2010. English
Accès au texte intégral et bibtex
these.pdf BibTex
Titre
Preuves constructives de complétude et contrôle délimité
Auteurs
Danko Ilik
Détail
Ecole Polytechnique X, Oct. 2010. English
Accès au texte intégral et bibtex
thesis-danko-ilik.pdf BibTex
Titre
Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq.
Auteurs
Elie Soubiran
Détail
informatique. Ecole Polytechnique X, Sep. 2010. French
Accès au texte intégral et bibtex
these.pdf BibTex

Rapports

Titre
Certifying cost annotations in compilers
Auteurs
Roberto M. Amadio; Nicolas Ayache; Yann Régis-Gianas; Ronan Saillard
Détail
[Report], 2010
Accès au texte intégral et bibtex
ccac-hal.pdf ccac-hal.ps BibTex

2009

Communications avec actes

Titre
Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus
Auteurs
Hugo Herbelin; Gyesik Lee
Détail
Hiroakira Ono and Makoto Kanazama and Ruy de Queiroz. Workshop on Logic, Language, Information and Computation, Jun 2009, Tokyo, Japan. Springer, Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-25, 2009, Proceedings, 5514, pp. 209-217, Lecture Notes in Artificial Intelligence
Accès au texte intégral et bibtex
wollic-HerLee09-kripke-cut-elim.pdf BibTex
Titre
An Operational Account of Call-By-Value Minimal and Classical $\lambda$-calculus in ''Natural Deduction'' Form
Auteurs
Hugo Herbelin; Stéphane Zimmermann
Détail
Pierre-Louis Curien. TLCA 2009 - 9th International Conference on Typed Lambda-Calculi and Applications, Jul 2009, Brasilia, Brazil. Springer-Verlag, Typed Lambda Calculi and Applications, 5608, pp. 142-156, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
ndcbv.pdf BibTex
Titre
Focalisation and Classical Realisability (version with appendices)
Auteurs
Guillaume Munch-Maccagnoni
Détail
Erich Grädel and Reinhard Kahle. 18th EACSL Annual Conference on Computer Science Logic - CSL 09, Sep 2009, Coimbra, Portugal. Springer-Verlag, Lecture notes in computer science, 5771, pp. 409-423
Accès au texte intégral et bibtex
focalisation_and_classical_realisability_long.pdf BibTex

Ouvrages scientifiques

Titre
Introduction to ''Interactive models of computation and program behaviour"
Auteurs
Pierre-Louis Curien
Détail
Société Mathématique de France, pp. xi-xv, 2009, Panoramas et Synthèses
Accès au texte intégral et bibtex
intro-pano.pdf intro-pano.ps BibTex

Chapitres d'ouvrages scientifiques

Titre
Sequential algorithms as bistable maps
Auteurs
Pierre-Louis Curien
Détail
Yves Bertot, Gérard Huet, Jean-Jacques Lévy and Gordon Plotkin. From semantics to computer science: essays in honour of Gilles Kahn, Cambridge University Press, pp. 51-71, 2009
Accès au texte intégral et bibtex
laird-sa.pdf BibTex

Documents sans référence de publication

Titre
λμ-calculus and Λμ-calculus: a Capital Difference
Auteurs
Hugo Herbelin; Alexis Saurin
Détail
2009
Accès au texte intégral et bibtex
apal-HerSau10-lambda-mu-Lambda-mu.pdf BibTex