| 2013 | A Constructive Theory of Regular Languages in Coq. Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka |
| 2013 | A Formal Model and Correctness Proof for an Access Control Policy Framework. Chunhan Wu, Xingyuan Zhang, Christian Urban |
| 2013 | A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem. Andrea Asperti |
| 2013 | Aliasing Restrictions of C11 Formalized in Coq. Robbert Krebbers |
| 2013 | Certifiably Sound Parallelizing Transformations. Christian J. Bell |
| 2013 | Certified Kruskal's Tree Theorem. Christian Sternagel |
| 2013 | Certified Parsing of Regular Languages. Denis Firsov, Tarmo Uustalu |
| 2013 | Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings Georges Gonthier, Michael Norrish |
| 2013 | Computational Verification of Network Programs in Coq. Gordon Stewart |
| 2013 | Extracting Proofs from Tabled Proof Search. Dale Miller, Alwen Tiu |
| 2013 | Formalizing Probabilistic Noninterference. Andrei Popescu, Johannes Hölzl, Tobias Nipkow |
| 2013 | Formalizing the SAFECode Type System. Daniel Huang, Greg Morrisett |
| 2013 | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. Brian Huffman, Ondrej Kuncar |
| 2013 | Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties. Narges Khakpour, Oliver Schwarz, Mads Dam |
| 2013 | Mostly Sound Type System Improves a Foundational Program Verifier. Josiah Dodds, Andrew W. Appel |
| 2013 | Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. Andreas Schropp, Andrei Popescu |
| 2013 | Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka |
| 2013 | Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. Magnus O. Myreen, Gregorio Curello |
| 2013 | Refinements for Free! Cyril Cohen, Maxime Dénès, Anders Mörtberg |
| 2013 | π n (S n ) in Homotopy Type Theory. Daniel R. Licata, Guillaume Brunerie |