inria
Inria.fr
Inria Channel
- Présentation
- Publications HAL
- Rapports d'activité
Equipe de recherche PI.R2
Publications de l'équipe PI.R2
2013
Articles dans des revues avec comité de lecture
- Titre
- Certifying and reasoning about cost annotations of functional programs
- Auteurs
- Roberto M. Amadio; Yann Regis-Gianas
- Détail
- Higher-Order and Symbolic Computation, Springer, 2013
- Accès au texte intégral et bibtex
-
Documents sans référence de publication
- Titre
- A Homotopical Completion Procedure with Applications to Coherence of Monoids
- Auteurs
- Yves Guiraud
; Philippe Malbos ; Samuel Mimram - Détail
- Apr. 2013
- Accès au texte intégral et bibtex
-
- Titre
- Simple simpl
- Auteurs
- Pierre Boutillier
- Détail
- Mar. 2013
- Accès au texte intégral et bibtex
-
- Titre
- Univalence for free
- Auteurs
- Matthieu Sozeau; Nicolas Tabareau
- Détail
- Feb. 2013
- Accès au texte intégral et 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
-
- Titre
- Böhm theorem and Böhm trees for the Lambda-mu-calculus
- Auteurs
- Alexis Saurin
- Détail
- Theoretical Computer Science, 2012, 435, pp. 106-138
- Accès au 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
-
- 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
-
- Titre
- Partiality and Recursion in Interactive Theorem Provers - An Overview
- Auteurs
- Ana Bove; Alexander Krauss; Matthieu Sozeau
- Détail
- Mathematical Structures in Computer Science, CUP, 2012
- Accès au texte intégral et 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
-
- Titre
- Higher-dimensional normalisation strategies for acyclicity
- Auteurs
- Yves Guiraud; Philippe Malbos
- Détail
- Advances in Mathematics, 2012, 231 (3-4), pp. 2294-2351
- Accès au texte intégral et 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
-
- 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. pp. _
- Accès au texte intégral et bibtex
-
- Titre
- A relaxation of Coq's guard condition
- Auteurs
- Pierre Boutillier
- Détail
- JFLA - Journées Francophones des langages applicatifs - 2012, Feb 2012, Carnac, France. pp. 1 - 14
- Accès au texte intégral et bibtex
-
- Titre
- A Constructive Proof of Dependent Choice, Compatible with Classical Logic
- Auteurs
- Hugo Herbelin
- 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
-
- Titre
- Classical call-by-need sequent calculi : The unity of semantic artifacts
- Auteurs
- Zena Ariola; Paul Downen; Hugo Herbelin ; Keiko Nakata ; 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
-
Communications sans actes
- Titre
- Safe Incremental Type Checking
- Auteurs
- Matthias Puech ; Yann Régis-Gianas
- 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
-
Conférences invitées
- Titre
- Coq avec Classes
- Auteurs
- Matthieu Sozeau
- Détail
- JFLA - Journées Françaises des Langages Applicatifs, Feb 2012, Carnac, France.
- Accès au 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, pp. 25-50, 2012, Nankai Series in Pure, Applied Mathematics and Theoretical Physics, Vol. 9
- Accès au texte intégral et bibtex
-
Autres publications
- Titre
- Forcing in Coq
- Auteurs
- Matthieu Sozeau ; 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
-
- Titre
- A gentle introduction to type classes and relations in Coq
- Auteurs
- Pierre Castéran ; 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
-
Rapports
- Titre
- Eliminating Skolem Functions in Peano Arithmetic with Interactive Realizability
- Auteurs
- Federico Aschieri ; Margherita Zorzi
- Détail
- [Technical Report], 2012
- Accès au texte intégral et bibtex
-
- Titre
- Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms
- Auteurs
- Federico Aschieri
- Détail
- [Technical Report], 2012
- Accès au texte intégral et bibtex
-
Documents sans référence de publication
- Titre
- Coherent presentations of Artin groups
- Auteurs
- Stéphane Gaussent ; Yves Guiraud ; Philippe Malbos
- Détail
- Mar. 2012. 68 pages
- Accès au texte intégral et bibtex
-
- Titre
- Interactive Realizability for Second-Order Heyting Arithmetic with EM1 and SK1
- Auteurs
- Federico Aschieri
- Détail
- Jan. 2012
- Accès au texte intégral et 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
-
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
-
- 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, 6505, pp. 78-87, 2011, LNAI
- Accès au 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
-
- 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
-
- 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
-
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. 10 p.
- Accès au texte intégral et 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. pp. 161-176, Electronic Notes Theoretical Computer Science
- Accès au 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, 6014, pp. 374-388, Lecture notes in computer science
- Accès au 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, 6009, pp. 134-149, Lecture notes in computer science
- Accès au 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. pp. 219 - 227
- Accès au 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
-
- 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
-
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
-
Conférences invitées
- Titre
- Elaborations in Type Theory
- Auteurs
- Matthieu Sozeau
- Détail
- DTP'10 - Dependently Typed Programming - 2010, Jul 2010, Edinburgh, United Kingdom.
- Accès au 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
-
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
-
- 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
-
- 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
-
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
-
- 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. Typed Lambda-Calculi and Applications, Jul 2009, Brasilia, Brazil. Springer-Verlag, 5608, pp. 142-156, Lecture Notes in Computer Science
- Accès au texte intégral et 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
-
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
-
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
-
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
-
Archives
En savoir plus
Retrouvez toutes les publications scientifiques de nos équipes de recherche sur HAL Inria
Voir aussi
