**Dan Hernest**
[ last updated **22 September 2015**, no longer maintained ]
** Homepage:
dan.hernest.eu
(check it for latest infos)**

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.

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.

[ 16 pp. | Final version in APAL, volume 2032 (2010), Pages 1379-1389, Elsevier ]

[ 10 pp. | CiE'08 | Final version in LNCS, volume 5028 (2008), Pages 251-260, Springer Verlag]

[ 10 pp. | Final version in Mathematical Logic Quarterly, volume 55 (2009), issue 5, Pages 551-561, Wiley-VCH ]

[ 12pp. | LFMTP@FLoC'06 | Final version in ENTCS, volume 174 (2007), issue 5, Pages 141-149, Elsevier ]

[ 09pp. | DCM@ICALP'06 | Final version in ENTCS, volume 171 (2007), issue 3, Pages 43-53, Elsevier ]

[ 16 pp. | CSL'05 | Appendix | Final version in LNCS, volume 3634 (2005) , Pages 477 - 492, Springer ]

published by

Poster paper presented at Computer Science Logic, Vienna, AT, 26 Aug 2003 (CSL'03)

Published in the Proceedings of the 4th International Symposium on Economic Informatics, the Academy of Economic Sciences (ASE), Bucharest, May 6-9, 1999

[ LFMTP@FLoC'06 --

[ DCM @ ICALP 2006 --

[ EST Training Workshop 2005 --

[ Proof Theory and Algorithms --