Hugo Herbelin

50 papers A* 9A 2B 3C 1Misc 1Journal 22Unranked 10
YearRankTypeTitle / Venue / Authors
2026 J jnl
Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice.
CoRR
Zena M. Ariola, Paul Downen, Hugo Herbelin
2026 J jnl
The very dependent recursive structure of iterated parametricity in indexed form.
CoRR
Hugo Herbelin, Ramkumar Ramachandra
2025 J jnl
A parametricity-based formalization of semi-simplicial and semi-cubical sets.
Math. Struct. Comput. Sci.
Hugo Herbelin, Ramkumar Ramachandra
2024 J jnl
A parametricity-based formalization of semi-simplicial and semi-cubical sets.
CoRR
Hugo Herbelin, Ramkumar Ramachandra
2024 B conf
On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles.
FSCD
Hugo Herbelin, Jad Koleilat
2024 J jnl
On the logical structure of some maximality and well-foundedness principles equivalent to choice principles.
CoRR
Hugo Herbelin
2021 A* conf
On the logical structure of choice and bar induction principles.
LICS
Nuria Brede, Hugo Herbelin
2021 J jnl
On the logical structure of choice and bar induction principles.
CoRR
Nuria Brede, Hugo Herbelin
2020 A* conf
A calculus of expandable stores: Continuation-and-environment-passing style translations.
LICS
Hugo Herbelin, Étienne Miquey
2018 B conf
Realizability Interpretation and Normalization of Typed Call-by-Need \lambda -calculus with Control.
FoSSaCS
Étienne Miquey, Hugo Herbelin
2018 J jnl
Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control.
CoRR
Étienne Miquey, Hugo Herbelin
2015 — ed.
20th International Conference on Types for Proofs and Programs, TYPES 2014, Paris, France, May 12-15, 2014
TYPES
Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau
2015 J jnl
A dependently-typed construction of semi-simplicial types.
Math. Struct. Comput. Sci.
Hugo Herbelin
2015 — conf
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant.
CICM (Work in Progress)
Théo Zimmermann, Hugo Herbelin
2015 J jnl
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant.
CoRR
Théo Zimmermann, Hugo Herbelin
2014 A* conf
30 years of research and development around Coq.
POPL
Gérard P. Huet, Hugo Herbelin
2013 — conf
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.
MKM/Calculemus/DML
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
2013 J jnl
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.
CoRR
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
2013 — conf
Proving with Side Effects.
TLCA
Hugo Herbelin
2013 — conf
The Rooster and the Syntactic Bracket.
TYPES
Hugo Herbelin, Arnaud Spiwack
2013 J jnl
The Rooster and the Syntactic Bracket.
CoRR
Hugo Herbelin, Arnaud Spiwack
2012 A* conf
A Constructive Proof of Dependent Choice, Compatible with Classical Logic.
LICS
Hugo Herbelin
2012 Misc conf
Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts.
FLOPS
Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin
2012 J jnl
Pure Type System conversion is always typable.
J. Funct. Program.
Vincent Siles, Hugo Herbelin
2011 — conf
Classical Call-by-Need and Duality.
TLCA
Zena M. Ariola, Hugo Herbelin, Alexis Saurin
2010 A* conf
An Intuitionistic Logic that Proves Markov's Principle.
LICS
Hugo Herbelin
2010 A* conf
Equality Is Typable in Semi-full Pure Type Systems.
LICS
Vincent Siles, Hugo Herbelin
2010 J jnl
Kripke models for classical logic.
Ann. Pure Appl. Log.
Danko Ilik, Gyesik Lee, Hugo Herbelin
2009 J jnl
A type-theoretic foundation of delimited continuations.
High. Order Symb. Comput.
Zena M. Ariola, Hugo Herbelin, Amr Sabry
2009 — conf
An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form.
TLCA
Hugo Herbelin, Stéphane Zimmermann
2009 J jnl
An overview of the Oregon programming languages summer school.
ACM SIGPLAN Notices
Jim Allen, Zena M. Ariola, Pierre-Louis Curien, Matthew Fluet, Jeffrey S. Foster, Dan Grossman, Robert Harper, Hugo Herbelin, Yannis Smaragdakis, David Walker, Steve Zdancewic
2009 C conf
Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus.
WoLLIC
Hugo Herbelin, Gyesik Lee
2009 J jnl
Kripke Models for Classical Logic
CoRR
Danko Ilik, Gyesik Lee, Hugo Herbelin
2008 — conf
A New Elimination Rule for the Calculus of Inductive Constructions.
TYPES
Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge luis Sacchini
2008 A* conf
An approach to call-by-name delimited continuations.
POPL
Hugo Herbelin, Silvia Ghilezan
2008 J jnl
Control reduction theories: the benefit of structural substitution.
J. Funct. Program.
Zena M. Ariola, Hugo Herbelin
2007 J jnl
A proof-theoretic foundation of abortive continuations.
High. Order Symb. Comput.
Zena M. Ariola, Hugo Herbelin, Amr Sabry
2007 J jnl
Abstract machines for dialogue games
CoRR
Pierre-Louis Curien, Hugo Herbelin
2005 — conf
On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic.
TLCA
Hugo Herbelin
2004 A conf
A type-theoretic foundation of continuations and prompts.
ICFP
Zena M. Ariola, Hugo Herbelin, Amr Sabry
2003 A* conf
Minimal Classical Logic and Control Operators.
ICALP
Zena M. Ariola, Hugo Herbelin
2001 J jnl
Explicit Substitutions and Reducibility.
J. Log. Comput.
Hugo Herbelin
2000 A conf
The duality of computation.
ICFP
Pierre-Louis Curien, Hugo Herbelin
1998 — conf
Computing with Abstract Böhm Trees.
Fuji International Symposium on Functional and Logic Programming
Pierre-Louis Curien, Hugo Herbelin
1997 — conf
Games and Weak-Head Reduction for Classical PCF.
TLCA
Hugo Herbelin
1996 A* conf
Game Semantics & Abstract Machines.
LICS
Vincent Danos, Hugo Herbelin, Laurent Regnier
1995 — —
Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes. (Computing with sequents: on the interpretation of sequent calculus as a calculus of lambda-terms and as a calculus of winning strategies).
Hugo Herbelin
1994 J jnl
A - Translation and Looping Combinators in Pure Type Systems.
J. Funct. Program.
Thierry Coquand, Hugo Herbelin
1994 B conf
A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure.
CSL
Hugo Herbelin
1989 J jnl
The two list algorithm for the knapsack problem on a FPS T20.
Parallel Comput.
Michel Cosnard, Afonso Ferreira, Hugo Herbelin