Danko Ilik / Danko Ilić / Данко Илиќ

Welcome to my academic web page!

You can find here my work in Logic and Programming, about the:

computational content of choice axioms and of completeness theorems;
meta-theory of intuitionistic logic, such an intuitionistic arithmetical hierarchy;
formula and type isomorphism, canonical forms of proofs and functional programs;
type-directed partial evaluation using dependently typed continuations;
various proof formalizations in Coq and Agda, including one of historical interest: Zermelo's 1904 proof of the well-ordering theorem.