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
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.
- oi-delcont.v
- 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.
- kripke_completeness.zip
- 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.
- boolean_completeness.zip
- 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.
- reals-coq-source.tar.gz
- 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.
- http://hashtest.sourceforge.net/
Back to home page
| Publications
| Teaching
| CV
| Contact