Zermelo's Well-Ordering Theorem in Type Theory. - Danko Ilik (TYPES, 2006)

Kripke models for classical logic. - Danko Ilik; Gyesik Lee; Hugo Herbelin (Ann. Pure Appl. Log., 2010)

Constructive Completeness Proofs and Delimited Control. (Preuves constructives de complétude et contrôle délimité). - Danko Ilik (2010)

Delimited control operators prove Double-negation Shift. - Danko Ilik (Ann. Pure Appl. Log., 2012)

A Constructive Proof of Open Induction Using Delimited Control Operators - Danko Ilik; Keiko Nakata 001 (CoRR, 2012)

An achievable Pre-log Region for the Non-coherent Block Fading MIMO Multiple Access Channel. - Zoran Utkovski; Danko Ilik; Ljupco Kocarev (ISWCS, 2013)

A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. - Danko Ilik; Keiko Nakata 001 (TYPES, 2013)

Continuation-passing style models complete for intuitionistic logic. - Danko Ilik (Ann. Pure Appl. Log., 2013)

A formalized type-directed partial evaluator for shift and reset - Danko Ilik (COS, 2013)

Double-negation Shift as a constructive principle - Danko Ilik (CoRR, 2013)

Axioms and decidability for type isomorphism in the presence of sums. - Danko Ilik (CSL-LICS, 2014)

Proofs in continuation-passing style: normalization of Gödel's System T extended with sums and delimited control operators: Distilled Tutorial. - Danko Ilik (PPDP, 2014)

The Exp-Log Normal Form of Types and Canonical Terms for Lambda Calculus with Sums. - Danko Ilik; Zakaria Chihani (CoRR, 2015)

The exp-log normal form of types: decomposing extensional equality and representing terms compactly. - Danko Ilik (POPL, 2017)

Perspectives for Proof Unwinding by Programming Languages Techniques. - Danko Ilik (FLAP, 2017)

Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms. - Danko Ilik (CoRR, 2019)

An intuitionistic formula hierarchy based on high-school identities. - Taus Brock-Nannestad; Danko Ilik (Math. Log. Q., 2019)