| Constructive completeness proofs and delimited control D Ilik Ecole Polytechnique X, 2010 | 44 | 2010 |
| Kripke models for classical logic D Ilik, G Lee, H Herbelin Annals of Pure and Applied Logic 161 (11), 1367-1378, 2010 | 31 | 2010 |
| Delimited control operators prove double-negation shift D Ilik Annals of Pure and Applied logic 163 (11), 1549-1559, 2012 | 30 | 2012 |
| Continuation-passing style models complete for intuitionistic logic D Ilik Annals of Pure and Applied Logic 164 (6), 651-662, 2013 | 19 | 2013 |
| An analysis of the constructive content of Henkin's proof of G\" odel's completeness theorem H Herbelin, D Ilik arXiv preprint arXiv:2401.13304, 2024 | 15 | 2024 |
| Axioms and decidability for type isomorphism in the presence of sums D Ilik Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer …, 2014 | 15 | 2014 |
| A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators D Ilik, K Nakata Leibniz International Proceedings in Informatics (LIPIcs) 26, 188--201, 2014 | 7* | 2014 |
| Normalization of gödel’s system t extended with control delimited at the type of natural numbers D Ilik | 7 | |
| The exp-log normal form of types: Decomposing extensional equality and representing terms compactly D Ilik Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming …, 2017 | 6* | 2017 |
| A formalized type-directed partial evaluator for shift and reset D Ilik COS, 86-100, 2013 | 6* | 2013 |
| Zermelo’s well-ordering theorem in type theory D Ilik International Workshop on Types for Proofs and Programs, 175-187, 2006 | 6 | 2006 |
| An intuitionistic formula hierarchy based on high‐school identities T Brock‐Nannestad, D Ilik Mathematical Logic Quarterly 65 (1), 57-79, 2019 | 5 | 2019 |
| An achievable pre-log region for the non-coherent block fading MIMO multiple access channel Z Utkovski, D Ilik, L Kocarev ISWCS 2013; The Tenth International Symposium on Wireless Communication …, 2013 | 4 | 2013 |
| Classical polarizations yield double-negation translations Z Chihani, D Ilik, D Miller | 3 | 2016 |
| An interpretation of the Sigma-2 fragment of classical Analysis in System T D Ilik | 3* | 2014 |
| Demo Paper: Coqlex, an approach to generate verified lexers W Ouedraogo, D Ilik, L Strassburger ML 2021-ACM SIGPLAN Workshop on ML, 2021 | 1 | 2021 |
| Perspectives for proof unwinding by programming languages techniques D Ilik arXiv preprint arXiv:1605.09177, 2016 | 1 | 2016 |
| Proofs in continuation-passing style: normalization of Gödel's System T extended with sums and delimited control operators: Distilled Tutorial D Ilik Proceedings of the 16th International Symposium on Principles and Practice …, 2014 | 1 | 2014 |
| Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms D Ilik arXiv preprint arXiv:1905.07621, 2019 | | 2019 |
| An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem DRAFT H Herbelin, D Ilik | | 2016 |
Keiko NakataSAP SEVerified email at cs.ioc.ee
