default search action
Hugo Herbelin
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c25]Hugo Herbelin, Jad Koleilat:
On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles. FSCD 2024: 26:1-26:15 - [i10]Hugo Herbelin, Ramkumar Ramachandra
:
A parametricity-based formalization of semi-simplicial and semi-cubical sets. CoRR abs/2401.00512 (2024) - [i9]Hugo Herbelin:
On the logical structure of some maximality and well-foundedness principles equivalent to choice principles. CoRR abs/2405.09946 (2024) - 2021
- [c24]Nuria Brede
On the logical structure of choice and bar induction principles. LICS 2021: 1-13 - [i8]Nuria Brede
On the logical structure of choice and bar induction principles. CoRR abs/2105.08951 (2021) - 2020
- [c23]Hugo Herbelin, Étienne Miquey
A calculus of expandable stores: Continuation-and-environment-passing style translations. LICS 2020: 564-577
2010 – 2019
- 2018
- [c22]Étienne Miquey
Realizability Interpretation and Normalization of Typed Call-by-Need \lambda -calculus with Control. FoSSaCS 2018: 276-292 - [i7]Étienne Miquey, Hugo Herbelin:
Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control. CoRR abs/1803.00914 (2018) - 2015
- [j10]Hugo Herbelin:
A dependently-typed construction of semi-simplicial types. Math. Struct. Comput. Sci. 25(5): 1116-1131 (2015) - [e1]Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau:
20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France. LIPIcs 39, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2015, ISBN 978-3-939897-88-0 [contents] - [i6]Théo Zimmermann, Hugo Herbelin:
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. CICM (Work in Progress) 2015: 50-62 - [i5]Théo Zimmermann
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. CoRR abs/1505.05028 (2015) - 2014
- [c21]Gérard P. Huet, Hugo Herbelin:
30 years of research and development around Coq. POPL 2014: 249-250 - 2013
- [c20]Bruno Barras, Lourdes Del Carmen González-Huesca
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. MKM/Calculemus/DML 2013: 359-363 - [c19]Hugo Herbelin:
Proving with Side Effects. TLCA 2013: 2 - [c18]Hugo Herbelin, Arnaud Spiwack:
The Rooster and the Syntactic Bracket. TYPES 2013: 169-187 - [i4]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 abs/1305.7360 (2013) - [i3]Hugo Herbelin, Arnaud Spiwack:
The Rooster and the Syntactic Bracket. CoRR abs/1309.5767 (2013) - 2012
- [j9]Vincent Siles, Hugo Herbelin:
Pure Type System conversion is always typable. J. Funct. Program. 22(2): 153-180 (2012) - [c17]Zena M. Ariola, Paul Downen
Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. FLOPS 2012: 32-46 - [c16]Hugo Herbelin:
A Constructive Proof of Dependent Choice, Compatible with Classical Logic. LICS 2012: 365-374 - 2011
- [c15]Zena M. Ariola, Hugo Herbelin, Alexis Saurin:
Classical Call-by-Need and Duality. TLCA 2011: 27-44 - 2010
- [j8]Danko Ilik
Kripke models for classical logic. Ann. Pure Appl. Log. 161(11): 1367-1378 (2010) - [c14]Vincent Siles, Hugo Herbelin:
Equality Is Typable in Semi-full Pure Type Systems. LICS 2010: 21-30 - [c13]Hugo Herbelin:
An Intuitionistic Logic that Proves Markov's Principle. LICS 2010: 50-56
2000 – 2009
- 2009
- [j7]Zena M. Ariola, Hugo Herbelin, Amr Sabry
A type-theoretic foundation of delimited continuations. High. Order Symb. Comput. 22(3): 233-273 (2009) - [j6]Jim Allen, Zena M. Ariola, Pierre-Louis Curien, Matthew Fluet, Jeffrey S. Foster, Dan Grossman, Robert Harper, Hugo Herbelin, Yannis Smaragdakis, David Walker
An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 44(11): 1-3 (2009) - [c12]Hugo Herbelin, Stéphane Zimmermann:
An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. TLCA 2009: 142-156 - [c11]Hugo Herbelin, Gyesik Lee:
Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. WoLLIC 2009: 209-217 - [i2]Danko Ilik, Gyesik Lee, Hugo Herbelin:
Kripke Models for Classical Logic. CoRR abs/0904.0071 (2009) - 2008
- [j5]Zena M. Ariola, Hugo Herbelin:
Control reduction theories: the benefit of structural substitution. J. Funct. Program. 18(3): 373-419 (2008) - [c10]Hugo Herbelin, Silvia Ghilezan
An approach to call-by-name delimited continuations. POPL 2008: 383-394 - [c9]Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini:
A New Elimination Rule for the Calculus of Inductive Constructions. TYPES 2008: 32-48 - 2007
- [j4]Zena M. Ariola, Hugo Herbelin, Amr Sabry
A proof-theoretic foundation of abortive continuations. High. Order Symb. Comput. 20(4): 403-429 (2007) - [i1]Pierre-Louis Curien, Hugo Herbelin:
Abstract machines for dialogue games. CoRR abs/0706.2544 (2007) - 2005
- [c8]Hugo Herbelin:
On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. TLCA 2005: 209-220 - 2004
- [c7]Zena M. Ariola, Hugo Herbelin, Amr Sabry
A type-theoretic foundation of continuations and prompts. ICFP 2004: 40-53 - 2003
- [c6]Zena M. Ariola, Hugo Herbelin:
Minimal Classical Logic and Control Operators. ICALP 2003: 871-885 - 2001
- [j3]Hugo Herbelin:
Explicit Substitutions and Reducibility. J. Log. Comput. 11(3): 431-451 (2001) - 2000
- [c5]Pierre-Louis Curien, Hugo Herbelin:
The duality of computation. ICFP 2000: 233-243
1990 – 1999
- 1998
- [c4]Pierre-Louis Curien, Hugo Herbelin:
Computing with Abstract Böhm Trees. Fuji International Symposium on Functional and Logic Programming 1998: 20-39 - 1997
- [c3]Hugo Herbelin:
Games and Weak-Head Reduction for Classical PCF. TLCA 1997: 214-230 - 1996
- [c2]Vincent Danos, Hugo Herbelin, Laurent Regnier:
Game Semantics & Abstract Machines. LICS 1996: 394-405 - 1995
- [b1]Hugo Herbelin:
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). Paris Diderot University, France, 1995 - 1994
- [j2]Thierry Coquand, Hugo Herbelin:
A - Translation and Looping Combinators in Pure Type Systems. J. Funct. Program. 4(1): 77-88 (1994) - [c1]Hugo Herbelin:
A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure. CSL 1994: 61-75
1980 – 1989
- 1989
- [j1]Michel Cosnard, Afonso Ferreira, Hugo Herbelin:
The two list algorithm for the knapsack problem on a FPS T20. Parallel Comput. 9(3): 385-388 (1989)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:14 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: