I am a PhD student in the research group πr², advised by Hugo Herbelin, and financed by Ecole Polytechnique. I spent the first year of my studies within the research group TypiCal.
My interests are constructive type theory, proof theory, functional programming and semantics of programming languages. In my daily work I use the proof assistant Coq.
Contact: danko AT lix DOT polytechnique DOT fr; IRC: #coq on
irc.freenode.net; Research blog
PGP key id EBF590A2 fingerprint F86F 7446 5D70 AD02 93A9 AB6D 286E
F71E EBF5 90A2
Abstract: 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 potential applications.
Author's version; to appear in Annals of Pure and Applied Logic, special issue on "Classical Logic and Computation".Abstract: We experiment with implementing exact real arithmetic in the Coq proof assistant, following a constructive mathematics approach of Gabriel Stolzenberg, which does not need the axiom of countable choice.
Masterclass report; coq code.Abstract: Taking a `set' to be a type together with an equivalence relation and adding an extensional choice axiom to the logical framework (a restricted version of constructive type theory) it is shown that any `set' can be well-ordered. Zermelo's first proof from 1904 is followed, with a simplification to avoid using comparability of well-orderings. The proof has been formalised in the system AgdaLight.
Author's version; published in Lecture Notes in Computer Science, Volume 4502/2007, "Types for Proofs and Programs".