Hugo Herbelin

According to our database, Hugo Herbelin authored at least 39 papers between 1989 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

A parametricity-based formalization of semi-simplicial and semi-cubical sets.

Hugo Herbelin, Ramkumar Ramachandra

CoRR, 2024

2021

On the logical structure of choice and bar induction principles.

Nuria Brede, Hugo Herbelin

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

A calculus of expandable stores: Continuation-and-environment-passing style translations.

Hugo Herbelin, Étienne Miquey

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2018

Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control.

Étienne Miquey, Hugo Herbelin

CoRR, 2018

Realizability Interpretation and Normalization of Typed Call-by-Need \lambda -calculus with Control.

Étienne Miquey, Hugo Herbelin

Proceedings of the Foundations of Software Science and Computation Structures, 2018

2015

A dependently-typed construction of semi-simplicial types.

Hugo Herbelin

Math. Struct. Comput. Sci., 2015

Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant.

Théo Zimmermann, Hugo Herbelin

Proceedings of the CICM 2015, 2015

2014

30 years of research and development around Coq.

Gérard P. Huet, Hugo Herbelin

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013

The Rooster and the Syntactic Bracket.

Hugo Herbelin, Arnaud Spiwack

Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

Proving with Side Effects.

Hugo Herbelin

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.

Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff

Proceedings of the Intelligent Computer Mathematics, 2013

2012

Pure Type System conversion is always typable.

Vincent Siles, Hugo Herbelin

J. Funct. Program., 2012

A Constructive Proof of Dependent Choice, Compatible with Classical Logic.

Hugo Herbelin

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts.

Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin

Proceedings of the Functional and Logic Programming - 11th International Symposium, 2012

2011

Classical Call-by-Need and Duality.

Zena M. Ariola, Hugo Herbelin, Alexis Saurin

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

2010

Kripke models for classical logic.

Danko Ilik, Gyesik Lee, Hugo Herbelin

Ann. Pure Appl. Log., 2010

Equality Is Typable in Semi-full Pure Type Systems.

Vincent Siles, Hugo Herbelin

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

An Intuitionistic Logic that Proves Markov's Principle.

Hugo Herbelin

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

2009

An overview of the Oregon programming languages summer school.

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

ACM SIGPLAN Notices, 2009

A type-theoretic foundation of delimited continuations.

Zena M. Ariola, Hugo Herbelin, Amr Sabry

High. Order Symb. Comput., 2009

Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus.

Hugo Herbelin, Gyesik Lee

Proceedings of the Logic, 2009

An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form.

Hugo Herbelin, Stéphane Zimmermann

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

2008

Control reduction theories: the benefit of structural substitution.

Zena M. Ariola, Hugo Herbelin

J. Funct. Program., 2008

A New Elimination Rule for the Calculus of Inductive Constructions.

Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini

Proceedings of the Types for Proofs and Programs, International Conference, 2008

An approach to call-by-name delimited continuations.

Hugo Herbelin, Silvia Ghilezan

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

2007

A proof-theoretic foundation of abortive continuations.

Zena M. Ariola, Hugo Herbelin, Amr Sabry

High. Order Symb. Comput., 2007

Abstract machines for dialogue games

Pierre-Louis Curien, Hugo Herbelin

CoRR, 2007

2005

On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic.

Hugo Herbelin

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

2004

A type-theoretic foundation of continuations and prompts.

Zena M. Ariola, Hugo Herbelin, Amr Sabry

Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, 2004

2003

Minimal Classical Logic and Control Operators.

Zena M. Ariola, Hugo Herbelin

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

2001

Explicit Substitutions and Reducibility.

Hugo Herbelin

J. Log. Comput., 2001

2000

The duality of computation.

Pierre-Louis Curien, Hugo Herbelin

Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

1998

Computing with Abstract Böhm Trees.

Pierre-Louis Curien, Hugo Herbelin

Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, 1998

1997

Games and Weak-Head Reduction for Classical PCF.

Hugo Herbelin

Proceedings of the Typed Lambda Calculi and Applications, 1997

1996

Game Semantics & Abstract Machines.

Vincent Danos, Hugo Herbelin, Laurent Regnier

Proceedings of the Proceedings, 1996

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

PhD thesis, 1995

1994

A - Translation and Looping Combinators in Pure Type Systems.

Thierry Coquand, Hugo Herbelin

J. Funct. Program., 1994

A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure.

Hugo Herbelin

Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1989

The two list algorithm for the knapsack problem on a FPS T20.

Michel Cosnard, Afonso Ferreira, Hugo Herbelin

Parallel Comput., 1989