Powered by
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018),
January 8–9, 2018,
Los Angeles, CA, USA
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018)
Frontmatter
Invited Talks
Verifing Programs and Systems
Verified Applications
Proof Methods and Libraries
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm,
Kenji Maillard,
Cédric Fournet, Cătălin Hriţcu, Matteo Maffei,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem Rastogi,
Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
Trusted Verification Frameworks and Systems
Proofs in Conflict-Driven Theory Combination
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar
(University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA)
Type Theory, Set Theory, and Formalized Mathematics
Formalizing Meta-Theory
HOπ in Coq
Sergueï Lenglet and Alan Schmitt
(University of Lorraine, France; Inria, France)
proc time: 0.7