CPP 2013

19 papers

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