POPL 2018 (series) / CPP 2018 (series) /
CPP 2018 Program
This is the CPP 2018 program - see the full program for POPL 2018 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 8 JanDisplayed time zone: Tijuana, Baja California change
Mon 8 Jan
Displayed time zone: Tijuana, Baja California change
09:00 - 10:00 | Invited Talk by René ThiemannCPP at Museum A Chair(s): June Andronick Data61,CSIRO (formerly NICTA) and UNSW | ||
09:00 60mTalk | Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper) CPP Jose Divasón , Sebastiaan Joosten , Ondřej Kunčar Technische Universität München, Germany, René Thiemann University of Innsbruck, Akihisa Yamada DOI |
10:30 - 12:00 | |||
10:30 30mTalk | Total Haskell is Reasonable Coq CPP Antal Spector-Zabusky , Joachim Breitner University of Pennsylvania, Christine Rizkallah University of Pennsylvania, USA, Stephanie Weirich University of Pennsylvania, USA DOI | ||
11:00 30mTalk | A Formal Proof in Coq of a Control Function for the Inverted Pendulum CPP Damien Rouhling University of Côte d'Azur, France DOI | ||
11:30 30mTalk | Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq CPP DOI |
13:30 - 15:30 | |||
13:30 30mTalk | Mechanising and Verifying the WebAssembly Specification CPP Conrad Watt University of Cambridge, UK DOI | ||
14:00 30mTalk | Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL CPP Sidney Amani UNSW, Australia, Myriam Bégel ENS Paris-Saclay, France, Maksym Bortin , Mark Staples CSIRO, Australia DOI | ||
14:30 30mTalk | Mechanising Blockchain Consensus CPP DOI Pre-print | ||
15:00 30mTalk | Formal Microeconomic Foundations and the First Welfare Theorem CPP |
16:00 - 18:00 | |||
16:00 30mTalk | Triangulating Context Lemmas CPP DOI | ||
16:30 30mTalk | Adapting Proof Automation to Adapt Proofs CPP Talia Ringer University of Washington, Nathaniel Yazdani University of Washington, Seattle, John Leo Halfaya Research, Dan Grossman University of Washington DOI | ||
17:00 30mTalk | A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations CPP Niklas Grimm Vienna University of Technology, Austria, Kenji Maillard Inria Paris and ENS Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Matteo Maffei Saarland University, Jonathan Protzenko Microsoft Research, n.n., Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Santiago Zanella-Béguelin Microsoft Research, n.n. DOI | ||
17:30 30mTalk | Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations CPP Hugo Férée University of Kent, UK, Samuel Hym University of Lille, France, Micaela Mayero , Jean-Yves Moyen University of Copenhagen, Denmark, David Nowak CNRS, France DOI |
18:15 - 20:15 | |||
18:15 2hSocial Event | CPP Reception CPP |
Tue 9 JanDisplayed time zone: Tijuana, Baja California change
Tue 9 Jan
Displayed time zone: Tijuana, Baja California change
09:00 - 10:00 | |||
09:00 60mTalk | POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk) CPP Brigitte Pientka McGill University DOI |
10:30 - 12:00 | |||
10:30 30mTalk | A Verified SAT Solver with Watched Literals Using Imperative HOL CPP Mathias Fleury MPI-INF, Jasmin Blanchette Vrije Universiteit Amsterdam, Peter Lammich Technische Universität München DOI | ||
11:00 30mTalk | Œuf: Minimizing the Coq Extraction TCB CPP Eric Mullen University of Washington, Stuart Pernsteiner University of Washington, USA, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle, Dan Grossman University of Washington DOI | ||
11:30 30mTalk | Proofs in Conflict-Driven Theory Combination CPP Maria Paola Bonacina University of Verona, Italy, Stéphane Graham-Lengrand CNRS, France, Natarajan Shankar SRI International, USA DOI |
13:30 - 15:30 | Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A Chair(s): Thorsten Altenkirch University of Nottingham | ||
13:30 30mTalk | Finite Sets in Homotopy Type Theory CPP Dan Frumin Radboud University, Herman Geuvers Radboud University Nijmegen, Netherlands, Léon Gondelman LRI, Université Paris-Sud, Niels van der Weide Radboud University Nijmegen, Netherlands DOI | ||
14:00 30mTalk | Generic Derivation of Induction for Impredicative Encodings in Cedille CPP DOI | ||
14:30 30mTalk | Large Model Constructions for Second-Order ZF in Dependent Type Theory CPP DOI | ||
15:00 30mTalk | A Constructive Formalisation of Semi-algebraic Sets and Functions CPP Boris Djalal INRIA |
16:00 - 18:00 | |||
16:00 30mTalk | HOpi in Coq CPP DOI | ||
16:30 30mTalk | A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory CPP DOI | ||
17:00 30mTalk | A Two-Level Logic Perspective on (Simultaneous) Substitutions CPP Kaustuv Chaudhuri Inria, France DOI | ||
17:30 30mTalk | Binder Aware Recursion over Well-Scoped de Bruijn Syntax CPP DOI |