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⟩