Hugo Herbelin

According to our database1, Hugo Herbelin authored at least 41 papers between 1989 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

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

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

On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles.
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

2021
On the logical structure of choice and bar induction principles.
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.
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.
CoRR, 2018

Realizability Interpretation and Normalization of Typed Call-by-Need \lambda -calculus with Control.
Proceedings of the Foundations of Software Science and Computation Structures, 2018

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

Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant.
Proceedings of the CICM 2015, 2015

2014
30 years of research and development around Coq.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013
The Rooster and the Syntactic Bracket.
Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

Proving with Side Effects.
Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.
Proceedings of the Intelligent Computer Mathematics, 2013

2012
Pure Type System conversion is always typable.
J. Funct. Program., 2012

A Constructive Proof of Dependent Choice, Compatible with Classical Logic.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts.
Proceedings of the Functional and Logic Programming - 11th International Symposium, 2012

2011
Classical Call-by-Need and Duality.
Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

2010
Kripke models for classical logic.
Ann. Pure Appl. Log., 2010

Equality Is Typable in Semi-full Pure Type Systems.
Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

An Intuitionistic Logic that Proves Markov's Principle.
Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

2009
An overview of the Oregon programming languages summer school.
ACM SIGPLAN Notices, 2009

A type-theoretic foundation of delimited continuations.
High. Order Symb. Comput., 2009

Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus.
Proceedings of the Logic, 2009

An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form.
Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

2008
Control reduction theories: the benefit of structural substitution.
J. Funct. Program., 2008

A New Elimination Rule for the Calculus of Inductive Constructions.
Proceedings of the Types for Proofs and Programs, International Conference, 2008

An approach to call-by-name delimited continuations.
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

2007
A proof-theoretic foundation of abortive continuations.
High. Order Symb. Comput., 2007

Abstract machines for dialogue games
CoRR, 2007

2005
On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

2004
A type-theoretic foundation of continuations and prompts.
Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, 2004

2003
Minimal Classical Logic and Control Operators.
Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

2001
Explicit Substitutions and Reducibility.
J. Log. Comput., 2001

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

1998
Computing with Abstract Böhm Trees.
Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, 1998

1997
Games and Weak-Head Reduction for Classical PCF.
Proceedings of the Typed Lambda Calculi and Applications, 1997

1996
Game Semantics & Abstract Machines.
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).
PhD thesis, 1995

1994
A - Translation and Looping Combinators in Pure Type Systems.
J. Funct. Program., 1994

A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure.
Proceedings of the Computer Science Logic, 8th International Workshop, 1994

1989
The two list algorithm for the knapsack problem on a FPS T20.
Parallel Comput., 1989


  Loading...