Dan Hernest
[ last updated 15 december 2020 ]
Homepage:
dan.hernest.eu
(check it for latest infos)
E-mail:
danhernest gmail com
I have been associate researcher of Romanian Institute for Science and Technology.
Previously I was associate researcher of the Stoilow Institute of Mathematics.
I have 9 published papers, 3 of which in journals.
I wrote the first
Dialectica extraction modules for the proof-system
MinLog.
[
My papers at DBLP-Trier (not all of them) | Curriculum Vitae (CV) |
My PhD Thesis |
Recent Photos of me ]
I am philosophiae doctor of Ecole Polytechnique
(and in co-tutelle
of Universitaet Muenchen).
I got my M.Sc. in Computer Science in August 2001 from
BRICS,
University of Aarhus
with
Prof. Kohlenbach.
I got my B.Sc. (4 years)
in Mathematics in July 1998 from the
University of Bucharest
with Prof. Georgescu.
Modal functional (`Dialectica') interpretation, (in progress).
The associated Scheme software is
here.
I believe that certified computer programs are better obtained from non-constructive proofs
of given specifications. Either modularly, by means of light variants of
Dialectica interpretation.
Or target-oriented, by means of refined variants of
A-translation.
Published papers (after PhD)
[ 2 journal + 1 conference = 3 peer reviewed ]
[3]
Light Dialectica revisited
[ + Trifon Trifonov]
[
Final version in APAL,
volume 2032 (2010), Pages 1379-1389, Elsevier ]
[2]
Hybrid functional interpretations
[ + Paulo Oliva]
[ Final version in LNCS, volume 5028 (2008),
Pages 251-260,
Springer Verlag]
[1]
Light Monotone Dialectica methods for Proof Mining
[ Final version in Mathematical Logic Quarterly,
volume 55 (2009), issue 5, Pages 551-561,
Wiley-VCH ]
Older published papers
[ 1 journal + 5 conference = 4 peer reviewed + 2 invited ]:
[6]
Synthesis of moduli of uniform continuity by the Monotone Dialectica Interpretation
in the proof-system MINLOG
[
LFMTP@FLoC'06 |
Final version in
ENTCS,
volume 174 (2007), issue 5, Pages 141-149, Elsevier ]
[5]
Light Dialectica program extraction from a classical Fibonacci proof
[
DCM@ICALP'06 |
Final version in
ENTCS,
volume 171 (2007), issue 3, Pages 43-53, Elsevier ]
[4]
Light Functional Interpretation - an optimization of Goedel's
technique towards the extraction of (more) efficient programs from (classical) proofs -
[
CSL'05 |
Final version in LNCS,
volume 3634 (2005) ,
Pages 477 - 492, Springer ]
[3]
A complexity analysis of functional interpretations
[ + Ulrich Kohlenbach,
70 pp. | abstract ]
published by Theoretical Computer Science,
338(1-3):200--246, 2005, Elsevier,
as shortened and revised version of the
BRICS Tech. Rep. RS-03-12
[2]
A comparison between two techniques of program extraction from classical proofs
[ 3 pp. ]
Poster paper presented at Computer Science Logic, Vienna, AT, 26 Aug 2003 (CSL'03)
[1]
Classical models are particular cases of Probabilistic models
[ 11 pp. ]
Published in the Proceedings of the 4th International Symposium on Economic Informatics,
the Academy of Economic Sciences (ASE), Bucharest, May 6-9, 1999