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

I work at Inria and LIX, where I do research in Mathematical Logic and Theoretical Computer Science.

The main aim of my work has been to modernize proof theory and the foundations of constructive mathematics using distilled computing abstractions from the theory of programming languages such as delimited control operators, partial evaluators and type isomorphisms. One can see this as working on extensions of the Curry-Howard correspondence relevant to applications of proof theory in mathematics and in proof assistant systems such as Coq. In particular, I contribute to structural proof theory as participant to the ProofCert project in the team Parsifal.

Publications | Formal Proofs and Software | Teaching | CV | Contact

Latest News RSS