Arthur Charguéraud
Publications
by date
by topic
by venue
Software
OptiTrust
CFML
TLC
PASL
FormalMetaCoq
Teaching
Separation Logic
Coq tutorials
Concours Castor
France-ioi
Misc
The RE command
Home
–
Contact
This work is now distributed as part of
the Locally Nameless Library (LN)
.
A snapshot of the files taken at the time of publication of the paper at POPL'08 is available from
here
. Note, however, that it compiles only with Coq v8.1.