More feasible programs from (non-constructive) proofs by the Light (Monotone) Dialectica interpretation. MD Hernest Ecole Polytechnique X, 2006 | 24* | 2006 |
Hybrid functional interpretations MD Hernest, P Oliva Logic and Theory of Algorithms: 4th Conference on Computability in Europe …, 2008 | 19 | 2008 |
Light functional interpretation: an optimization of Gödel’s technique towards the extraction of (more) efficient programs from (classical) proofs MD Hernest Computer Science Logic: 19th International Workshop, CSL 2005, 14th Annual …, 2005 | 18 | 2005 |
A complexity analysis of functional interpretations MD Hernest, U Kohlenbach Theoretical Computer Science 338 (1-3), 200-246, 2005 | 17 | 2005 |
Light Dialectica program extraction from a classical Fibonacci proof MD Hernest Electronic Notes in Theoretical Computer Science 171 (3), 43-53, 2007 | 15 | 2007 |
A comparison between two techniques of program extraction from classical proofs MD Hernest LPAR 2002: Short Contributions; CSL 2003: Extended Posters - Collegium …, 2004 | 13 | 2004 |
Synthesis of moduli of uniform continuity by the Monotone Dialectica Interpretation in the proof-system MinLog MD Hernest Electronic Notes in Theoretical Computer Science 174 (5), 141-149, 2007 | 11 | 2007 |
Minimal Logic for Dialectica Interpretation D Hernest, T Trifonov Free software, with full code source and documentation@ https://triffon …, 2021 | 10* | 2021 |
Light dialectica revisited MD Hernest, T Trifonov Annals of Pure and Applied Logic 161 (11), 1379-1389, 2010 | 6 | 2010 |
Light monotone Dialectica methods for proof mining MD Hernest Mathematical Logic Quarterly 55 (5), 551-561, 2009 | 1 | 2009 |
Modal Functional (Dialectica) Interpretation D Hernest, T Trifonov Logical Methods in Computer Science 17, 2021 | | 2021 |
Experiments with a PCCoder extension D Hernest arXiv preprint arXiv:1912.00781, 2019 | | 2019 |
Classical Logic and Computation (2008) R Adams, Z Luo, W Heijltjes, D Ilik, G Lee, H Herbelin, MD Hernest, ... Elsevier, 2010 | | 2010 |