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.
- Applications of the analogy between formulas and exponential
polynomials to equivalence and normal forms
- This is a short paper synthesizing the results of my
previous papers on the formulas-as-polynomials correspondence,
and giving two applications of it: 1) a method for (dis)proving
formula isomorphism and equivalence based on showing
(in)equality; 2) a constructive analogue of the arithmetical
hierarchy, based on the exp-log normal form. The results are
valid intuitionistically, as well as classically.
- arXiv:1905.07621
-- 12th
Panhellenic Logic Symposium, June 26-30, 2019, Anogeia,
Crete
- 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, showing 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 and perhaps more important one is obtaining an
arithmetical hierarchy for intuitionistic first-order
logic.
- arXiv:1601.04876
-- Mathematical
Logic Quarterly, volume 65, 2019 --
Formal Coq
proofs
- 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
-- IfColog Journal of Logics and their Applications, volume 4 (10), 2017
- 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
-- Proceedings
of POPL 2017 -- Coq
implementation
- 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.
- Manuscript
- 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 to 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
- 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
Here are some of my reviews for the ZB and MR reference journals: reviews/
Back
to home page | Formal Proofs and
Software | Teaching | CV | Contact