Arthur Charguéraud
Research
Binders
Capabilities
Verification
Fixed points
Granularity
Pretty-big-step
JavaScript
Publications
by venue
by project
by date
Talks
by venue
by project
by date
Software
LN
CFML
TLC
PASL
Teaching
France-IOI
Coq proofs
Verification
Home – Contact
International journals
The Locally Nameless Representation
Journal of Automated Reasoning (JAR), May 2011
paper - abstract - bib
International conferences
Engineering Formal Metatheory
with B. Aydemir, B. C. Pierce, R. Pollack and S. Weirich
Symposium on Principles of Programming Languages (POPL), January 2008
paper - abstract - bib
Functional Translation of a Calculus of Capabilities
with F. Pottier
International Conference on Functional Programming (ICFP), September 2008
paper - abstract - bib - appendix
The Optimal Fixed Point Combinator
International Conference on Interactive Theorem Proving (ITP), July 2010
paper - abstract - bib - long version
Program Verification Through Characteristic Formulae
International Conference on Functional Programming (ICFP), September 2010
paper - abstract - bib
Characteristic Formulae for the Verification of Imperative Programs
International Conference on Functional Programming (ICFP), September 2011
paper - abstract - bib
Oracle Scheduling: Controlling Granularity in Implicitly Parallel Languages
with U. Acar and M. Rainey
OOPSLA, October 2011
paper - abstract - bib
Pretty-Big-Step Semantics
To appear at the European Symposium on Programming (ESOP), March 2013
paper - abstract - bib - scripts
Scheduling Parallel Programs by Work Stealing with Private Deques
with U. Acar and M. Rainey
Symposium on Principles and Practice of Parallel Programming (PPOPP), Febuary 2013
paper - abstract - bib
International workshops
Efficient Primitives for Creating and Scheduling Parallel Computations
with U. Acar and M. Rainey
Declarative Aspects and Applications of Multicore Programming (DAMP), January 2012
paper - abstract - bib
Drafts
Characteristic Formulae for the Verification of Imperative Programs
(Journal version of ICFP'11). Submitted, October 2012
paper - abstract - bib
Reports
Interactive Verification of Call-by-Value Functional Programs Through a Deep Embedding
Report, March 2009
paper - abstract - bib
Proof Pearl: A Constructive Fixed Point Combinator for Recursive Functions
Report, March 2009
paper - abstract - bib
Characteristic Formulae for Mechanized Program Verification
PhD thesis, December 2010
paper - abstract - bib