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