There is an error, I can confess now. Some 40 years after the paper was published, the logician Robert M. Solovay from the University of California sent me a communication pointing out the error. I thought: “How could it be?” I started to look at it and finally I realized […] (John F. Nash Jr. 2015)

Publications of Danko Ilik

Articles | Theses & Reports | Reviews in zbMATH and MathSciNet

I am generally interested in important and long-standing open questions in foundations, such as a (simpler) constructive interpretation of proofs that use the classical axiom of choice, finding constructive versions of completeness theorems, defining criteria of simplicity for formal proofs and identity of proofs, and understanding the meta-theory of formula isomorphism.

My contributions often involve application of techniques from the theory of programming languages, like partial evaluators, control operators, and type isomorphisms. I also try to contribute back to computer science by work on equational theories of terms for typed lambda calculi in presence of delimited control operators, recursion, and co-product types.


The exp-log normal form of types
This paper presents a normal form for types, that is, formulas of intuitionistic propositional logic, that is an extension of the classic disjunctive normal forms that also handles exponentials (implication). The normal form is then used to obtain a new decomposition of the axioms of beta-eta-equality for the lambda calculus with coproducts, and a new compact representation of that lambda calculus.
arXiv:1502.04634 -- to appear in Proceedings of POPL 2017 -- Coq implementation
Perspectives for proof unwinding by programming languages techniques
In this chapter, we propose some future directions of work, potentially beneficial to Mathematics and its foundations, based on the recent import of methodology from the theory of programming languages into proof theory. This scientific essay, written for the audience of proof theorists as well as the working mathematician, is not a survey of the field, but rather a personal view of the author who hopes that it may inspire future and fellow researchers.
arXiv:1605.09177 -- Book chapter (to appear)
An Intuitionistic Formula Hierarchy Based on High-School Identities (with Taus Brock-Nannestad)
This paper makes a link between sequent calculi and multivariate exponential polynomials, showng that proof rules are valid when interpreted as inequalities between such polynomials. A first application is to building an intuitionistic proof calculus that does not contain invertible rules. A second one is obtaining a hierarchy of first-order intuitionistic formulas that preserves identity of proofs.
arXiv:1601.04876 -- Formal Coq proofs
Classical polarizations yield double negation translations (with Zakaria Chihani and Dale Miller)
We show how the most well-known forms of double-negation translation can be defined by a simple polarization of formulas. This allows to arrive at a definition of what a double-negation translation is, in view of recent results of Gaspar showing that there exist formulas obtained by double-negation translation which are not intuitionistically equivalent. Moreover, by using polarization, the structure of proofs is preserved by the translation, while it is known that a double-negation translation is a non-local proof transformation.
An interpretation of the Sigma-2 fragment of classical Analysis in System T
This paper gives a computational interpretation of the Sigma-2 fragment of classical analysis as terms of Gödel's system T, circumventing bar recursion. This was predicted as possible by a 1979 result of Schwichtenberg. Delimited control operators no longer appear in the language of realizers neither, although the system T terms are extracted by partially evaluating terms terms that use control operators. This procedure was formalized in the Agda proof assistant.
arXiv:1301.5089 -- Errata for old versions -- Formal Agda proof in Formalization
Axioms and decidability for type isomorphism in presence of sums
Type isomorphism can logically be seen as formula isomorphism or constructive set cardinality. Using the link between this type language and exponential polynomials, and relying on classic results of Levitz, Henson, Rubel, Wilkie, Macintyre, and Gurevič, around Tarski's high-school algebra problem, in this paper it is shown that the theory of type isomorphism is both axiomatizable and decidable.
Author's version -- CSL-LICS 2014 -- Erratum
A direct version of Veldman's proof of open induction on Cantor space via delimited control operators (with Keiko Nakata)
The open induction principle is the only known form of the classical axiom of choice which is stable under the double-negation translation. In this work, we unwound Veldman's proof of the principle from double negation shift and Markov's principle, and obtained a direct proof which only uses an extension of intuitionistic logic with delimited control operators. This suggests a computational interpretation of open induction alternative to Ulrich Berger's open recursion.
Author's version -- LIPIcs 26, 2014 -- Formal Coq proof in Formalization
Type Directed Partial Evaluation for Level-1 Shift and Reset
This paper presents a type-directed partial evaluator for the shift and reset delimited control operators of Danvy and Filinski. Both in the call-by-name and the call-by-value case, we compare the results of running the partial evaluator (within the Coq proof assistant where it is formalized) with the currently available equational theories. Sum types are also covered in the evaluator.
EPTCS 127, 2013 -- Erratum -- Formal Coq proof in Formalization
An achievable pre-log region for the non-coherent block fading MIMO multiple access channel (with Zoran Utkovski and Ljupco Kocarev)
In this paper in network information theory, we analyze the theoretically achievable pre-log region of a MIMO MAC channel for the case of non-coherent communication. In the non-coherent setting, the parties are only aware of the statistics of fading, but do not know of its realization. This problem is modeled by geometric methods that involve Grassmann manifolds.
Proceedings of ISWCS 2013 -- If you need but cannot access this paper, write me an e-mail
Continuation-passing style models complete for intuitionistic logic
Intuitionistic logic is at the basis of constructive proofs, but its own completeness proof with respect to Kripke semantics is not constructive: additional semi-constructive principles like the fan theorem are necessary for the proof. In this paper, it is shown how to avoid the extra principles by modifying the notion of model so as to allow performing a proof in continuation-passing style; this is another technique imported from programming languages theory. The proof was formalized in the Coq proof assistant and can act as a type-directed partial evaluator for lambda calculus with coproducts.
Author's version -- Annals of Pure and Applied Logic 164(6), 2013 -- Formal Coq proof in Formalization
Delimited control operators prove double-negation shift
The double negation shift is a logical principle which is the key to the computational interpretation of the classical axiom of choice. This winning paper for the Kurt Gödel Research Prize fellowships (in the doctoral category) gives a computational interpretation of double negation shift in terms of delimited control operators from the theory of programming languages. This presents an alternative to the classic approach of using the bar recursion schema going back to Spector.
Author's version -- Annals of Pure and Applied Logic 163(11), 2012
Kripke models for classical logic (with Gyesik Lee and Hugo Herbelin)
Kripke models are a standard semantic for intuitionistic logic. In this paper, we showed how a form of Kripke models can be used to give sound and complete semantics for classical first-order logic as well. The proof is constructive and the development is accompanied by a formal proof in the Coq proof assistant. This proof can be directly `run' as a program in Coq, and its algorithmic content is that of a type-directed partial evaluator for lambda-bar-mu-mu-tilde, a sequent calculus version of lambda calculus extended with control operators and let-expressions.
Author's version -- Annals of Pure and Applied Logic 161(11), 2010 -- Formal Coq proof in Formalization
Zermelo's well-ordering theorem in type theory
The well-ordering theorem is one of the early landmark results of set theory. In this paper, we give a reconstruction of Zermelo's first 1904 proof of the theorem, that we formalized in intuitionistic type theory extended with an extensional axiom of choice. This demonstrates that type theory can be used to
Author's version -- Lecture Notes in Computer Science 4502, 2007 -- Formal AgdaLight proof in Formalization

Theses & Reports

Constructive completeness proofs and delimited control (PhD thesis, 2010, supervised by Hugo Herbelin)
This thesis studies the constructive versions of some known forms of completeness for classical logic (Gödel, Krivine) and develops new forms of completeness theorems for classical and intuitionistic logic. During these investigations, an intermediary form of logic, based on delimited control operators, was suggested, that can prove extra-intuitionistic principles, but does not lead to non-constructivity as full classical logic does.
Thesis -- Formal Coq proofs in Formalization
An efficient model of constructive real numbers in Coq (Masterclass report, 2007, supervised by Bas Spitters)
This masterclass graduation report describes an experiment of efficient formalization of constructive real numbers in the Coq proof assistant.
Report -- Formal Coq proof in Formalization
Zermelo's well-ordering theorem in type theory (MSc thesis, 2006, supervised by Thierry Coquand)
This is the thesis version of the homonymous paper described at above.
Published as paper -- Formal Coq proof in Formalization

Reviews in zbMATH and MathSciNet

Back to home page | Formal Proofs and Software | Teaching | CV | Contact