Danko Ilik

According to our database, Danko Ilik authored at least 17 papers between 2006 and 2019.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2019

An intuitionistic formula hierarchy based on high-school identities.

Taus Brock-Nannestad, Danko Ilik

Math. Log. Q., 2019

Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms.

Danko Ilik

CoRR, 2019

2017

Perspectives for Proof Unwinding by Programming Languages Techniques.

Danko Ilik

FLAP, 2017

The exp-log normal form of types: decomposing extensional equality and representing terms compactly.

Danko Ilik

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2015

The Exp-Log Normal Form of Types and Canonical Terms for Lambda Calculus with Sums.

Danko Ilik, Zakaria Chihani

CoRR, 2015

2014

Proofs in continuation-passing style: normalization of Gödel's System T extended with sums and delimited control operators: Distilled Tutorial.

Danko Ilik

Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, 2014

Axioms and decidability for type isomorphism in the presence of sums.

Danko Ilik

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013

Double-negation Shift as a constructive principle

Danko Ilik

CoRR, 2013

A formalized type-directed partial evaluator for shift and reset

Danko Ilik

Proceedings of the Proceedings First Workshop on Control Operators and their Semantics, 2013

Continuation-passing style models complete for intuitionistic logic.

Danko Ilik

Ann. Pure Appl. Log., 2013

A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators.

Danko Ilik, Keiko Nakata

Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

An achievable Pre-log Region for the Non-coherent Block Fading MIMO Multiple Access Channel.

Zoran Utkovski, Danko Ilik, Ljupco Kocarev

Proceedings of the ISWCS 2013, 2013

2012

A Constructive Proof of Open Induction Using Delimited Control Operators

Danko Ilik, Keiko Nakata

CoRR, 2012

Delimited control operators prove Double-negation Shift.

Danko Ilik

Ann. Pure Appl. Log., 2012

2010

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

Danko Ilik

PhD thesis, 2010

Kripke models for classical logic.

Danko Ilik, Gyesik Lee, Hugo Herbelin

Ann. Pure Appl. Log., 2010

2006

Zermelo's Well-Ordering Theorem in Type Theory.

Danko Ilik

Proceedings of the Types for Proofs and Programs, International Workshop, 2006