Hugo HerbelinResearcher at INRIA, RocquencourtParis, π r^{2} team, within the PPS group of the IRIF labCoordinator of the Coq development team Email: Hugo.Herbelin at inria.fr Office : number 3029, 3th floor, Building Sophie Germain, 9 Place Aurélie Nemours, 75013 Paris (at the level of 56 avenue de France) Surface mail: Laboratoire IRIFPPS, Université Paris Diderot  Paris 7, Case 7014, 75205 Paris Cedex 13, France Phone: +33 (0) 1 57 27 90 87 Main research interests
My research globally centres around the syntactic unity
between proofs and programs, with applications to:
Commented research
My master is from 1988, but in the 19891992 period, it happens that I was more
concerned with my newlyborn nowold daughter than with research.
I worked from 1993 on the computational content of sequent
calculus and on its relation to the theory of programming
languages (ch. 2
of PhD
thesis, CSL94), contributing at the same time to a better understanding of the
proofasprogram correspondence for classical logic (ch. 3
of PhD thesis,
ICFP00 with PierreLouis Curien, ch. 1 to 3 of Habilitation).
I worked from 1994 on the syntactic view at game semantics
(ch. 5 and 6 of PhD
thesis, LICS96 with Vincent
Danos and Laurent
Régnier, TLCA97, FLOPS98
with PierreLouis Curien), which is closely connected to sequent
calculus and abstract machines. After some time, I prefered to work
directly with syntax than via a "semantical" gametheoretic
abstraction of it. I liked my
old note decomposing AJM games into
HO games and Pdigitalisation, but I felt this was not at all an
approach the atthistime dominant British school was interested in.
In the 19961999 period, I devoted relatively quite a lot of time to
teaching, system engineering, and
understanding Coq's insides, fascinated
by what Gérard Huet and Thierry Coquand created, altogether with the team they
built. It was not a period for intense foundational research and the
refusal at LICS of the ad hoc aritybased abstract machine for
System F I was so proud about hurt me a lot. The paper is still
not published (the referees were however right that the presentation
was obscured by overly complex notations).
With Zena Ariola, I started to apply the proofasprogram
correspondence for classical logic to a better understanding of
control operators in programming languages
(ICALP03/HOSC05, JFP07, TLCA09
with Stéphane Zimmermann, and a yet unpublished kind
of survey with
Alexis Saurin), what eventually also targeted callbyneed
evaluation
(TLCA11, FLOPS12).
From 2003 to 2008, I approached Felleisen and DanvyFilinski's notion
of delimited control in programming languages using Parigot's tools to
the proofasprogram correspondence for classical logic. This resulted,
first with Zena
Ariola and Amr Sabry, then with Silvia Ghilezan,
in a finegrained account of delimited control
(ICFP04/HOSC07, ch. 4 of Habilitation,
POPL08).
I've never been able to figure out whether it was already clear from
1993 for Catarina Coquand, Thierry Coquand, Ulrich Berger or others that reducibility
proofs had the same computational structure as
normalisationbyevaluation proofs, so, around 2008, I wrote a note on
it. I still don't know if what it says was known or not.
Inspired by the use of delimited control by Olivier Danvy in TypedDirected
Partial Evaluation (TDPE) and by the relation between TDPE and
NormalisationbyEvaluation (NbE), I started to work with Danko Ilik
on the computational content of completeness proofs in relation with
NbE and delimited control. This has turned to be a very fruitful field of
investigation.
First, it moved to a precise analysis of the computational
content of Gödel's completeness therorem proofs (in progress) and to
the analysis of Krikpe semantics in a classical setting (WOLLIC09,
APAL10).
More importantly, it moved to the study of the proofasprogram
correspondence in the presence of other side effects than
classical logic, especially delimiters
(LICS10), sharing (with
application to computing with dependent
choice, LICS12)
or memory assignment. In the latter case, this directly connects to
forcing as shown by JeanLouis Krivine in the context of realisability.
Recently, I started to take a computational view at reverse
mathematics, with Gyesik Lee, Keiko Nakata and Ludovic Patey (the
constructive content of the big five, an effective typetheoretic
presentation of PRA).
These days, as an entertainment related to the homotopical foundations
of type theory, I'm also working on the formal representation of
semisimplicial types
(MSCS14, and
more is to come).
All over the period from 1988 to
now, Coq was a faithful
companion to the loneliness of my mind. I contributed to
its implementation, especially intensively from 1996 to 2008,
as well as to the coordination of its development. From time to
time, I also contributed to the foundations of type theory
(JFP94 on a proposal of
Thierry
Coquand, TLCA05, TYPES08,
as well as
LICS10 and JFP11 with Vincent Siles).
