Skip to Main content Skip to Navigation

inria-00159085v1  Journal articles
Thierry CoquandHugo Herbelin. A-Translation and Looping Combinators in Pure Type Systems
Journal of Functional Programming, Cambridge University Press (CUP), 1994, 4 (1), pp.77-88
inria-00497177v2  Journal articles
Vincent SilesHugo Herbelin. Pure Type System conversion is always typable
Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (2), pp.153 - 180. ⟨10.1017/S0956796812000044⟩
inria-00524949v1  Conference papers
Hugo HerbelinSilvia Ghilezan. An Approach to Call-by-Name Delimited Continuations
Symposium on Principles of Programming Languages, Jan 2008, San Francisco, United States. pp.383-394, ⟨10.1145/1328438.1328484⟩
inria-00481815v1  Conference papers
Hugo Herbelin. An intuitionistic logic that proves Markov's principle
Logic In Computer Science, Jul 2010, Edinburgh, United Kingdom. pp.50-56
inria-00381525v1  Conference papers
Hugo Herbelin. A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure
Computer Science Logic, Sep 1994, Kazimierz, Poland. pp.61--75
hal-00697241v1  Conference papers
Zena AriolaPaul DownenHugo HerbelinKeiko NakataAlexis Saurin. Classical call-by-need sequent calculi : The unity of semantic artifacts
FLOPS 2012 - 11th International Symposium on Functional and Logic Programming, May 2012, Kobe, Japan. pp.32-46, ⟨10.1007/978-3-642-29822-6⟩
inria-00381554v1  Conference papers
Hugo HerbelinGyesik Lee. Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus
Workshop on Logic, Language, Information and Computation, Jun 2009, Tokyo, Japan. pp.209-217
inria-00389903v1  Conference papers
Hugo HerbelinStéphane Zimmermann. An Operational Account of Call-By-Value Minimal and Classical $\lambda$-calculus in ''Natural Deduction'' Form
TLCA 2009 - 9th International Conference on Typed Lambda-Calculi and Applications, Mauricio Ayala Rincón, Jul 2009, Brasilia, Brazil. pp.142-156, ⟨10.1007/978-3-642-02273-9_12⟩
inria-00630156v1  Conference papers
Zena AriolaHugo HerbelinAlexis Saurin. Classical Call-by-need and duality
TLCA 2011 - Typed Lambda Calculi and Applications, Silvia Ghilezan, Jun 2011, Novi Sad, Serbia. pp.27-44, ⟨10.1007/978-3-642-21691-6_6⟩
hal-01645486v1  Journal articles
Sandrine BlazyPierre CastéranHugo Herbelin. L'Assistant de Preuve Coq Table des matières
Techniques de l'Ingenieur, Techniques de l'ingénieur, 2017
hal-03144849v3  Conference papers
Nuria BredeHugo Herbelin. On the logical structure of choice and bar induction principles
Logic in Computer Science, Jun 2021, Rome, Italy
inria-00156377v1  Conference papers
Hugo HerbelinPierre-Louis Curien. The duality of computation
Fifth ACM SIGPLAN International Conference on Functional Programming : ICFP '00, Sep 2000, Montréal, Canada. pp.233-243
hal-00935446v1  Journal articles
Hugo Herbelin. A dependently-typed construction of semi-simplicial types
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. ⟨10.1017/S0960129514000528⟩
hal-01671994v1  Conference papers
Théo ZimmermannHugo Herbelin. Coq's Prolog and application to defining semi-automatic tactics
Type Theory Based Tools, Jan 2017, Paris, France
inria-00496988v1  Conference papers
Vincent SilesHugo Herbelin. Equality is typable in Semi-Full Pure Type Systems
Logic In Computer Science - LICS 2010, Jul 2010, Edinburgh, United Kingdom. 10 p
inria-00371959v4  Journal articles
Danko IlikGyesik LeeHugo Herbelin. Kripke Models for Classical Logic
Annals of Pure and Applied Logic, Elsevier Masson, 2010, Special Issue: Classical Logic and Computation (2008), 161 (11), pp.1367-1378. ⟨10.1016/j.apal.2010.04.007⟩
hal-01152588v4  Conference papers
Théo ZimmermannHugo Herbelin. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
Conference on Intelligent Computer Mathematics, 2015, Washington, D.C., United States
hal-00155295v1  Book sections
Pierre-Louis CurienHugo Herbelin. Abstract machines for dialogue games
Interactive models of computation and program behavior, Société Mathématique de France, pp.231-275, 2009, Panoramas et Synthèses
inria-00177326v1  Journal articles
Zena AriolaHugo HerbelinAmr Sabry. A Type-Theoretic Foundation of Delimited Continuations
Higher-Order and Symbolic Computation, Springer Verlag, 2007
hal-00697242v1  Journal articles
Zena AriolaHugo HerbelinAmr Sabry. A Proof-Theoretic Foundation of Abortive Continuations
Higher-Order and Symbolic Computation, Springer Verlag, 2007, 20 (4), ⟨10.1007/s10990-007-9007-z⟩
inria-00177320v1  Journal articles
Zena AriolaHugo Herbelin. Control Reduction Theories: the Benefit of Structural Substitution
Journal of Functional Programming, Cambridge University Press (CUP), 2007
hal-02557823v2  Conference papers
Hugo HerbelinÉtienne Miquey. A calculus of expandable stores
LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken / Virtual, Germany. pp.564-577, ⟨10.1145/3373718.3394792⟩