I am a PhD student in the research group πr² based at the laboratory PPS. My advisor is Hugo Herbelin. I am financed by Ecole Polytechnique, Palaiseau, France. I spent the first year of my studies within the group TypiCal based at LIX.
My research 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; Blog: speleologic
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 meaning of the new notion and its applications to call-by-name proof normalisation.
Links to the draft, talk on the πr² seminar and talk on Padova's Logic seminar..In preparation...
Link to a talk on the TypiCal seminar and Ljubljana's Foundations seminar.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.
Springer link, link to a preprint, my old web page.