We cannot hope to prove that every definition, every symbol, every abbreviation that we introduce is free from potential ambiguities, that it does not bring about the possibility of a contradiction that might not otherwise have been present. [N. Bourbaki 1949]

Formalization and Software of Danko Ilik

Formal proofs | Software

Formal Proofs

In my daily work, I use Coq and Agda a lot; proof assistants are my microscope for analyzing mathematical arguments. Some of the more self-contained formalization are presented below.

Intuitionistic arithmetical hierarchy, 2016
A primitive-recursive formalization of the procedure for bringing a first-order formula to its exp-log normal form.
github link
Exp-log normal form of types, 2016
A primitive-recursive formalization of the procedure for bringing a type to its exp-log normal form. We also supply a normalization-by-evaluation procedure for lambda calculus with coproducts, working modulo type isomorphisms, and show examples where it allows to obtain a canonical normal form terms of the lambda calculus.
github link
Intuitionistic first-order hierarchy preserving formula isomorphism, 2015
We give Coq definitions of normalization procedures for propositional and first-order intuitionistic formulas, that proceed along high-school identities, and therefore preserve isomorphism of formulas. The propositional case is accompanied with a formal correctness proof establishing equations for the first theorem of the paper "An Intuitionistic Formula Hierarchy Based on High-School Identities".
github link
Normalization-by-evaluation for Gödel's system T extended with shift and reset in Agda, 2014
This is an Agda-formalized type-directed partial evaluator for Gödel's system T extended with shift and reset. In fact, what is actually shown is that shift and reset can be completely partially evaluated away from the calculus. For the first time (in comparison to our previous formalizations), the normalization procedure is shown correct with respect to an external equational theory. The application of this is actually to shown that bar recursion can be circumvented, i.e. that system T terms can be extracted directly from proofs of classical Analysis.
github link
Open induction on Cantor space from delimited control operators, 2013
This is a Coq-formalized proof of the main result from my paper with Nakata. One assumes shift and reset as axioms, as they are not available in Coq. There are a couple of admitted lemmas about equality of finite lists: these are Pi_1 statements and as such do not have an effect on the extracted algorithm - the algorithm itself, however, can not be produced by Coq, for it uses the intensional axiom of choice in addition to the assumed axioms. Finally, the main use of this formalization was to certify that the result from the paper with Nakata is correct.
Type-directed partial evaluation for level-1 shift and reset in Coq, 2011
This is a Coq-formalization of a normalization-by-evaluation procedure for the lambda calculus (with coproducts and) in presence of shift-reset delimited control operators of Danvy and Filinski. Both call-by-name and call-by-value variants are considered, and comparison for the known equational theories are made.
github link
Constructive completeness of first-order classical and intuitionistic predicate logic with respect to Kripke-CPS models, 2009
This development in Coq regroups two constructive completeness proofs for Kripke-CPS models. First, we have the completeness for classical propositional and predicate logic, in the form of Herbelin-Curien's lambda-bar-mu-mu-tilde sequent calculus. Second, we have the completeness for intuitionistic propositional and predicate logic, in the form of a natural deduction calculi -- in presence of disjunction and the existential quantifier, it is not known how to give a constructive proof of completeness with respect to standard (non-CPS) Kripke models. It is interesting to observe how little the notion of Kripke-CPS model differs between the classical and the intuitionistic version. The formalization can also be used as type-directed partial evaluator for lambda-bar-mu-mu-tilde, that is lambda calculus with coproduct types.
Constructive ultrafilter theorem and completeness for classical predicate logic, 2008
This formalizes almost all of Krivine-Berardi-Valentini's constructive reconstruction of Gödel's proof of completeness of classical predicate logic in Coq. In particular, fully formalized is the constructive ultra-filter theorem for setoids. The similarity between the statement of completeness and Hilbert's epsilon-substitution theorems is striking. Exactly one part remains non-finished (for lack of time): the procedure for sorting the Henkin axioms in the context, before they can be eliminated; the difficulty for formalizing this comes from the adhoc nature of the sorting procedure.
Computing constructive real numbers in Coq, 2007
This is an experiment in formalizing and computing with arbitrary precision real numbers inside the Coq proof assistant. We do not use the Cauchy sequence representation, but rather approximation with fine and consistent rational intervals. Computing Euler's number turns out to be relatively efficient.
Zermelo's well-ordering theorem in type theory, 2006
This is a formalization of Zermelo's first proof from 1904. This is before he proposed the axioms for what is today known as ZFC set theory. The second 1908 proof of the well-ordering theorem is not as intuitive as the first one. To formalize the argument we do not use set theoretic axioms, but rather add an extensional choice axiom to Martin-Löf type theory. By Diaconescu's argument, this gives rise to classical logic. Then, the whole of Zermelo's proof can be formalized in setoids (types modulo an equivalence relation).
zermelo.zip -- implemented in an ancient version of Agda: agdaLight v061019


As a kid, I did a lot of programming, from engineering for artistic projects to writing web spiders for search engines. From that period, only the following piece of software remains today in presentable form.

Testing cryptographic hash functions, 2004
Modular utility for testing properties of cryptographic hash functions (avalanche property, collision resistance, Maurer's test, Möbius analysis). Written in C.

Back to home page | Publications | Teaching | CV | Contact