Talks
Home
-
On defining McCarthy f91 in CIC (TYPES'2008, Torino, mar. 2008)
pdf,
with a coq development (to come).
-
Apero-reflexion (JFLA, Aix-les-Bains, jan. 2007)
pdf (in french),
with a coq demo.
-
Proving termination using dependent types: the case of xor-terms (common session TFP+TYPES, Nottingham, april 2006).
pdf.
-
Defending the Bank with a Proof Assistant (WITS, Vienna, march 2006).
pdf.
-
Proof pearl: From concrete to functional unparsing (TPHOLs, sept 2004).
advi.
-
A formalisation of the join-calculus in type theory (IWFMS'04, Nanjing).
pdf, advi.
Home