Dan Hernest 
[ last updated 22 September 2015, no longer maintained ]
  Homepage: 
dan.hernest.eu 
(check it for latest infos) 
 E-mail: 
danhernest yahoo 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) ]