21 citations · 70 across the 12 of their papers we have counts for
12 papers
An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem
Hugo Herbelin, Danko Ilik
G{ö}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of va…
Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms
Danko Ilik
We show some applications of the formulas-as-polynomials correspondence: 1) a method for (dis)proving formula isomorphism and equivalence based on showing (in)equality; 2) a constr…
Perspectives for proof unwinding by programming languages techniques
Danko Ilik
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…
An Intuitionistic Formula Hierarchy Based on High-School Identities
Taus Brock-Nannestad, Danko Ilik
We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials. After observing that most of the i…
The exp-log normal form of types
Danko Ilik
Lambda calculi with algebraic data types lie at the core of functional programming languages and proof assistants, but conceal at least two fundamental theoretical problems already…
Axioms and Decidability for Type Isomorphism in the Presence of Sums
Danko Ilik
We consider the problem of characterizing isomorphisms of types, or, equivalently, constructive cardinality of sets, in the simultaneous presence of disjoint unions, Cartesian prod…
An interpretation of the Sigma-2 fragment of classical Analysis in System T
Danko Ilik
We show that it is possible to define a realizability interpretation for the -fragment of classical Analysis using Gödel's System T only. This supplements a previous result of…
Type Directed Partial Evaluation for Level-1 Shift and Reset
Danko Ilik
We present an implementation in the Coq proof assistant of type directed partial evaluation (TDPE) algorithms for call-by-name and call-by-value versions of shift and reset delimit…
A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
Danko Ilik, Keiko Nakata
First, we reconstruct Wim Veldman's result that Open Induction on Cantor space can be derived from Double-negation Shift and Markov's Principle. In doing this, we notice that one h…
Continuation-passing Style Models Complete for Intuitionistic Logic
Danko Ilik
A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. T…
Delimited control operators prove Double-negation Shift
Danko Ilik
We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the Double-negation Shift sc…
Kripke Models for Classical Logic
Danko Ilik, Gyesik Lee, Hugo Herbelin
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potent…