Dr. Mircea Dan HERNEST [ 1st June 2010, CV ]
E-mail:    Dan @ MyLastName . EU

I will be a research fellow of the Department of Computer Science of Queen Mary University of London. Previously, I have been a research Post-Doc within the TIMA Laboratory of Polytech Grenoble team VDS, contractual on ANR project FME3.

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 revised PhD Thesis | Rapports Parigot et Jouannaud | Rapport de soutenance | Photos soutenance | Recent Photos of me ]

I am a doctor of Ecole Polytechnique (and, in co-tutelle, of Universitaet Muenchen). I got my Master in theoretical Informatics 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.


Recent published papers [ 2 journal + 1 conference = 3 peer reviewed ]

Modal Functional Interpretation, short paper recently submitted to a journal.

[3] Light Dialectica revisited [ + Trifon Trifonov]
[ 16 pp. | CL&C'08 | Final version in special issue of APAL journal, Elsevier,
volume 2032, year 2010, allocated DOI reference 10.1016/j.apal.2010.04.008 ]

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

[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],
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
[ 70 pp. | abstract | bib | DVI 60pp. | PDF | slides ]

[2] A comparison between two techniques of program extraction from classical proofs
Poster paper presented at Computer Science Logic, Vienna, AT, 26 Aug 2003 (CSL'03)
[ 3 pp. | DVI | PDF]

[1] Classical models are particular cases of Probabilistic models
Published in the Proceedings of the 4th International Symposium on Economic Informatics,
the Academy of Economic Sciences (ASE), Bucharest, May 6-9, 1999
[ 11 pp.| PS ]

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) ]
[ 25pp. | abstract | DVI | 4PS.zip | PS.zip ]

PastEvents: The Romanian CSL Winter Meeting 2002 [Bucharest, December 23, 2002]