Arthur Charguéraud
Research
Metatheory
Capabilities
Verification
Fixed points
Parallelism
Publications
by project
by venue
by date
Talks
by project
by venue
by date
Software
LN
CFML
TLC
Teaching
France-IOI
Coq proofs
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.