POPL 2016 (series) / CPP 2016 (series) /
CPP 2016 Program
This is the CPP 2016 program - see the full program for POPL 2016 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 60mTalk | Perspectives on Formal Verfication CPP Harvey Friedman Ohio State University | ||
10:30 - 12:00 | |||
10:30 30mTalk | Higher-order Representation Predicates in Separation Logic CPP | ||
11:00 30mTalk | A Unified Coq Framework for Verifying C Programs with Floating-Point Computations CPP | ||
11:30 30mTalk | Refinement Based Verification of Imperative Data Structures CPP Peter Lammich Technische Universität München | ||
14:00 - 15:30 | |||
14:00 30mTalk | The Vampire and the FOOL CPP Evgenii Kotelnikov Chalmers University of Technology, Laura Kovacs Chalmers University of Technology, Giles Reger University of Manchester, Andrei Voronkov University of Manchester | ||
14:30 30mTalk | Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP Lukasz Czajka University of Innsbruck | ||
15:00 30mTalk | Mizar Environment for Isabelle CPP Cezary Kaliszyk University of Innsbruck, Karol Pąk University of Bialystok, Institute of Computer Science, Josef Urban | ||
16:00 - 18:00 | |||
16:00 30mTalk | A Modular, Efficient Formalisation of Real Algebraic Numbers CPP | ||
16:30 30mTalk | Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials CPP Sophie Bernard INRIA, Yves Bertot INRIA, Laurence Rideau INRIA, Pierre-Yves Strub IMDEA Software Institute | ||
17:00 30mTalk | Formalizing Jordan Normal Forms in Isabelle/HOL CPP | ||
17:30 30mTalk | Formalization of a Newton series representation of polynomials CPP | ||
Tue 19 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 60mTalk | Dependent Type Practice CPP Leonardo de Moura Microsoft Research, Redmond | ||
10:30 - 12:00 | |||
10:30 30mTalk | A Logic of Proofs for Differential Dynamic Logic CPP | ||
11:00 30mTalk | Constructing the Propositional Truncation using Non-recursive HITs CPP Floris van Doorn Carnegie Mellon University | ||
11:30 30mTalk | A Nominal Exploration of Intuitionism CPP | ||
14:00 - 15:30 | |||
14:00 30mTalk | Bisimulation Up-to Techniques for Psi-calculi CPP | ||
14:30 30mTalk | Planning for Change in a Formal Verification of the Raft Consensus Protocol CPP Doug Woos University of Washington, James R. Wilcox University of Washington, Steve Anton University of Washington, Zachary Tatlock University of Washington, Seattle, Michael D. Ernst University of Washington, Thomas Anderson University of Washington Pre-print | ||
15:00 30mTalk | A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules CPP | ||
16:00 - 17:00 | |||
16:00 30mTalk | Formal Verification of Control-flow Graph Flattening CPP | ||
16:30 30mTalk | Axiomatic Semantics for Compiler Verification CPP | ||
18:00 - 21:00 | |||
18:00 3hSocial Event | CPP Reception, sponsored by the DeepSpec project CPP | ||