The two list algorithm for the knapsack problem on a FPS T20. - Michel Cosnard; Afonso Ferreira; Hugo Herbelin (Parallel Comput., 1989)

A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure. - Hugo Herbelin (CSL, 1994)

A - Translation and Looping Combinators in Pure Type Systems. - Thierry Coquand; Hugo Herbelin (J. Funct. Program., 1994)

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 (1995)

Game Semantics & Abstract Machines. - Vincent Danos; Hugo Herbelin; Laurent Regnier (LICS, 1996)

Games and Weak-Head Reduction for Classical PCF. - Hugo Herbelin (TLCA, 1997)

Computing with Abstract Böhm Trees. - Pierre-Louis Curien; Hugo Herbelin (Fuji International Symposium on Functional and Logic Programming, 1998)

The duality of computation. - Pierre-Louis Curien; Hugo Herbelin (ICFP, 2000)

Explicit Substitutions and Reducibility. - Hugo Herbelin (J. Log. Comput., 2001)

Minimal Classical Logic and Control Operators. - Zena M. Ariola; Hugo Herbelin (ICALP, 2003)

A type-theoretic foundation of continuations and prompts. - Zena M. Ariola; Hugo Herbelin; Amr Sabry (ICFP, 2004)

On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. - Hugo Herbelin (TLCA, 2005)

Abstract machines for dialogue games - Pierre-Louis Curien; Hugo Herbelin (CoRR, 2007)

A proof-theoretic foundation of abortive continuations. - Zena M. Ariola; Hugo Herbelin; Amr Sabry (High. Order Symb. Comput., 2007)

An approach to call-by-name delimited continuations. - Hugo Herbelin; Silvia Ghilezan (POPL, 2008)

A New Elimination Rule for the Calculus of Inductive Constructions. - Bruno Barras; Pierre Corbineau; Benjamin Grégoire; Hugo Herbelin; Jorge Luis Sacchini (TYPES, 2008)

Control reduction theories: the benefit of structural substitution. - Zena M. Ariola; Hugo Herbelin (J. Funct. Program., 2008)

An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. - Hugo Herbelin; Stéphane Zimmermann (TLCA, 2009)

Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. - Hugo Herbelin; Gyesik Lee (WoLLIC, 2009)

A type-theoretic foundation of delimited continuations. - Zena M. Ariola; Hugo Herbelin; Amr Sabry (High. Order Symb. Comput., 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 001; Hugo Herbelin; Yannis Smaragdakis; David Walker 001; Steve Zdancewic (ACM SIGPLAN Notices, 2009)

An Intuitionistic Logic that Proves Markov's Principle. - Hugo Herbelin (LICS, 2010)

Equality Is Typable in Semi-full Pure Type Systems. - Vincent Siles; Hugo Herbelin (LICS, 2010)

Kripke models for classical logic. - Danko Ilik; Gyesik Lee; Hugo Herbelin (Ann. Pure Appl. Log., 2010)

Classical Call-by-Need and Duality. - Zena M. Ariola; Hugo Herbelin; Alexis Saurin (TLCA, 2011)

Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. - Zena M. Ariola; Paul Downen; Hugo Herbelin; Keiko Nakata 001; Alexis Saurin (FLOPS, 2012)

A Constructive Proof of Dependent Choice, Compatible with Classical Logic. - Hugo Herbelin (LICS, 2012)

Pure Type System conversion is always typable. - Vincent Siles; Hugo Herbelin (J. Funct. Program., 2012)

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 (MKM/Calculemus/DML, 2013)

Proving with Side Effects. - Hugo Herbelin (TLCA, 2013)

The Rooster and the Syntactic Bracket. - Hugo Herbelin; Arnaud Spiwack (TYPES, 2013)

30 years of research and development around Coq. - Gérard P. Huet; Hugo Herbelin (POPL, 2014)

Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. - Théo Zimmermann; Hugo Herbelin (CICM (Work in Progress), 2015)

A dependently-typed construction of semi-simplicial types. - Hugo Herbelin (Math. Struct. Comput. Sci., 2015)

Realizability Interpretation and Normalization of Typed Call-by-Need lambda -calculus with Control. - Étienne Miquey; Hugo Herbelin (FoSSaCS, 2018)

Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control. - Étienne Miquey; Hugo Herbelin (CoRR, 2018)

A calculus of expandable stores: Continuation-and-environment-passing style translations. - Hugo Herbelin; Étienne Miquey (LICS, 2020)

On the logical structure of choice and bar induction principles. - Nuria Brede; Hugo Herbelin (LICS, 2021)

On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles. - Hugo Herbelin; Jad Koleilat (FSCD, 2024)

A parametricity-based formalization of semi-simplicial and semi-cubical sets. - Hugo Herbelin; Ramkumar Ramachandra (CoRR, 2024)

On the logical structure of some maximality and well-foundedness principles equivalent to choice principles. - Hugo Herbelin (CoRR, 2024)