Dan Hernest  [ last updated 21.09.2021 ]   Homepage:  dan.hernest.eu  ORCID  ResearcherID  LinkedIn   E-mail:  danhernest gmail com

Open for integration in research teams (projects). I was associate researcher of the Romanian Institute for Science and Technology until 2020. Check out https://github.com/danhernest-rist/google-research/tree/master/automl_zero. In 2017 - 2018 I worked as Data Scientist in the Business Intelligence unit of eServGlobal. Previously I was associate researcher (project manager) of the Stoilow Institute of Mathematics. I wrote the first Dialectica extraction modules for the proof-system MinLog. Check out the 2021 Minimal Logic For Dialectica Interpretation page maintained by me and Triffon (still no monotone extraction module ported from my 2006 tuples variant).

[ My papers at DBLP (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, (September 2021, final version to appear in Logical Methods in Computer Science). 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.

peer-veviewed papers (after PhD)

[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 ]

papers published before 2007

[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