Hugo Herbelin

Publication Activity (10 Years)

Years Active: 1989-2024
Publications (10 Years): 9

Top Venues

CoRR

LICS

FoSSaCS

Math. Struct. Comput. Sci.

Paris Diderot University, France (PHD)

Education History

Paris Diderot University, France

PHD

Publications

Hugo Herbelin, Ramkumar Ramachandra
A parametricity-based formalization of semi-simplicial and semi-cubical sets. CoRR (2024)
Nuria Brede, Hugo Herbelin
On the logical structure of choice and bar induction principles. LICS (2021)
Nuria Brede, Hugo Herbelin
On the logical structure of choice and bar induction principles. CoRR (2021)
Hugo Herbelin, Étienne Miquey
A calculus of expandable stores: Continuation-and-environment-passing style translations. LICS (2020)
Étienne Miquey, Hugo Herbelin
Realizability Interpretation and Normalization of Typed Call-by-Need \lambda -calculus with Control. FoSSaCS (2018)
Étienne Miquey, Hugo Herbelin
Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control. CoRR (2018)
Hugo Herbelin
A dependently-typed construction of semi-simplicial types. Math. Struct. Comput. Sci. 25 (5) (2015)
Théo Zimmermann, Hugo Herbelin
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. CICM (Work in Progress) (2015)
Théo Zimmermann, Hugo Herbelin
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. CoRR (2015)
Gérard P. Huet, Hugo Herbelin
30 years of research and development around Coq. POPL (2014)
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. MKM/Calculemus/DML (2013)
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. CoRR (2013)
Hugo Herbelin
Proving with Side Effects. TLCA (2013)
Hugo Herbelin, Arnaud Spiwack
The Rooster and the Syntactic Bracket. CoRR (2013)
Hugo Herbelin, Arnaud Spiwack
The Rooster and the Syntactic Bracket. TYPES (2013)
Hugo Herbelin
A Constructive Proof of Dependent Choice, Compatible with Classical Logic. LICS (2012)
Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin
Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. FLOPS (2012)
Vincent Siles, Hugo Herbelin
Pure Type System conversion is always typable. J. Funct. Program. 22 (2) (2012)
Zena M. Ariola, Hugo Herbelin, Alexis Saurin
Classical Call-by-Need and Duality. TLCA (2011)
Hugo Herbelin
An Intuitionistic Logic that Proves Markov's Principle. LICS (2010)
Vincent Siles, Hugo Herbelin
Equality Is Typable in Semi-full Pure Type Systems. LICS (2010)
Danko Ilik, Gyesik Lee, Hugo Herbelin
Kripke models for classical logic. Ann. Pure Appl. Log. 161 (11) (2010)
Hugo Herbelin, Gyesik Lee
Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. WoLLIC (2009)
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
An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 44 (11) (2009)
Hugo Herbelin, Stéphane Zimmermann
An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. TLCA (2009)
Zena M. Ariola, Hugo Herbelin, Amr Sabry
A type-theoretic foundation of delimited continuations. High. Order Symb. Comput. 22 (3) (2009)
Danko Ilik, Gyesik Lee, Hugo Herbelin
Kripke Models for Classical Logic CoRR (2009)
Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini
A New Elimination Rule for the Calculus of Inductive Constructions. TYPES (2008)
Zena M. Ariola, Hugo Herbelin
Control reduction theories: the benefit of structural substitution. J. Funct. Program. 18 (3) (2008)
Hugo Herbelin, Silvia Ghilezan
An approach to call-by-name delimited continuations. POPL (2008)
Zena M. Ariola, Hugo Herbelin, Amr Sabry
A proof-theoretic foundation of abortive continuations. High. Order Symb. Comput. 20 (4) (2007)
Pierre-Louis Curien, Hugo Herbelin
Abstract machines for dialogue games CoRR (2007)
Hugo Herbelin
On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. TLCA (2005)
Zena M. Ariola, Hugo Herbelin, Amr Sabry
A type-theoretic foundation of continuations and prompts. ICFP (2004)
Zena M. Ariola, Hugo Herbelin
Minimal Classical Logic and Control Operators. ICALP (2003)
Hugo Herbelin
Explicit Substitutions and Reducibility. J. Log. Comput. 11 (3) (2001)
Pierre-Louis Curien, Hugo Herbelin
The duality of computation. ICFP (2000)
Pierre-Louis Curien, Hugo Herbelin
Computing with Abstract Böhm Trees. Fuji International Symposium on Functional and Logic Programming (1998)
Hugo Herbelin
Games and Weak-Head Reduction for Classical PCF. TLCA (1997)
Vincent Danos, Hugo Herbelin, Laurent Regnier
Game Semantics & Abstract Machines. LICS (1996)
Thierry Coquand, Hugo Herbelin
A - Translation and Looping Combinators in Pure Type Systems. J. Funct. Program. 4 (1) (1994)
Hugo Herbelin
A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure. CSL (1994)
Michel Cosnard, Afonso Ferreira, Hugo Herbelin
The two list algorithm for the knapsack problem on a FPS T20. Parallel Comput. 9 (3) (1989)

Hugo Herbelin.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Hugo Herbelin