CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 18 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Session 1: Invited talk by Harvey FriedmanCPP at Room St Petersburg II
09:00
60m
Talk
Perspectives on Formal Verfication
CPP
Harvey Friedman Ohio State University
14:00 - 15:30
Session 3: Design and Implementation of Theorem ProversCPP at Room St Petersburg II
14:00
30m
Talk
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
30m
Talk
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
CPP
Lukasz Czajka University of Innsbruck
15:00
30m
Talk
Mizar Environment for Isabelle
CPP
Cezary Kaliszyk University of Innsbruck, Karol Pąk University of Bialystok, Institute of Computer Science, Josef Urban

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Session 5: Invited talk by Leonardo de MouraCPP at Room St Petersburg II
09:00
60m
Talk
Dependent Type Practice
CPP
Leonardo de Moura Microsoft Research, Redmond
10:30 - 12:00
Session 6: FoundationsCPP at Room St Petersburg II
10:30
30m
Talk
A Logic of Proofs for Differential Dynamic Logic
CPP
Nathan Fulton Carnegie Mellon University, André Platzer
11:00
30m
Talk
Constructing the Propositional Truncation using Non-recursive HITs
CPP
Floris van Doorn Carnegie Mellon University
11:30
30m
Talk
A Nominal Exploration of Intuitionism
CPP
Vincent Rahli SnT, Mark Bickford Cornell University
14:00 - 15:30
Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II
14:00
30m
Talk
Bisimulation Up-to Techniques for Psi-calculi
CPP
Johannes Å. Pohjola Uppsala University, Joachim Parrow Uppsala University
14:30
30m
Talk
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
30m
Talk
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Michel St-Martin University of Ottawa, Amy Felty University of Ottawa
16:00 - 17:00
Session 8: Compiler VerificationCPP at Room St Petersburg II
16:00
30m
Talk
Formal Verification of Control-flow Graph Flattening
CPP
Sandrine Blazy IRISA / University of Rennes 1, Alix Trieu ENS Rennes
16:30
30m
Talk
Axiomatic Semantics for Compiler Verification
CPP
Steven Schäfer , Sigurd Schneider Saarland University, Gert Smolka Saarland University
18:00 - 21:00
CPP Reception, sponsored by the DeepSpec projectCPP at Room St Petersburg I
18:00
3h
Social Event
CPP Reception, sponsored by the DeepSpec project
CPP