Dan Hernest  [ last updated 22 September 2015 ]   Homepage:  dan.hernest.eu  (check it for latest infos)   E-mail:  danhernest gmail com

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 | Rapports de these | Rapport de soutenance | Photos soutenance | Recent Photos of me ]

I am philosophiae doctor of Ecole Polytechnique (and in co-tutelle of Universitaet Muenchen). I got my Master in theoretical 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, recent paper (September 2015). 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]
[ 16 pp. | Final version in APAL, volume 2032 (2010), Pages 1379-1389, Elsevier ]

[2] Hybrid functional interpretations [ + Paulo Oliva]
[ 10 pp. | CiE'08 | Final version in LNCS, volume 5028 (2008), Pages 251-260, Springer Verlag]

[1] Light Monotone Dialectica methods for Proof Mining
[ 10 pp. | 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
[ 12pp. | 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
[ 09pp. | 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 -
[ 16 pp. | CSL'05 | Appendix | Final version in LNCS, volume 3634 (2005) , Pages 477 - 492, Springer ]

[3] A complexity analysis of functional interpretations  [ + Ulrich Kohlenbach, 70 pp. | abstract | PDF ]
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. | PDF ]
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.| PDF ]
Published in the Proceedings of the 4th International Symposium on Economic Informatics, the Academy of Economic Sciences (ASE), Bucharest, May 6-9, 1999

Some slides of my past talks [4]:

[1] Synthesis of moduli of uniform continuity by the Light Monotone Dialectica
[ LFMTP@FLoC'06 -- August 2006 -- Seattle, U.S.A ]
[2] Light Dialectica program extraction from a classical Fibonacci proof
[ DCM @ ICALP 2006 -- July 2006 -- Venezia, Italy ]
[3] Light Functional (``Dialectica'') Interpretation
[ EST Training Workshop 2005 -- Sept 2005 -- Fischbachau (near Munich, Germany) ]
[4] A complexity analysis of functional interpretations
[ Proof Theory and Algorithms -- March 2003 -- Edinburgh (Scotland, UK) ]