POPL 2019 (series) / CPP 2019 (series) /
CPP 2019 Program
This is the CPP 2019 program - see the full program for POPL 2019 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 14 JanDisplayed time zone: Belfast change
Mon 14 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | Keynote 1 and Research PaperCPP at Sala XII Chair(s): Magnus O. Myreen Chalmers University of Technology, Sweden | ||
09:00 60mTalk | A Linear Logical Framework in Hybrid CPP Amy Felty University of Ottawa DOI | ||
10:00 30mResearch paper | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines CPP DOI |
11:00 - 12:30 | Research Papers: Proof Theory, Theory of Programming LanguagesCPP at Sala XII Chair(s): Assia Mahboubi INRIA | ||
11:00 30mResearch paper | A Proof-Theoretic Approach to Certifying Skolemization CPP Kaustuv Chaudhuri Inria, France, Matteo Manighetti Inria & École Polytechnique, Dale Miller INRIA Saclay and LIX DOI | ||
11:30 30mResearch paper | Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory CPP Yannick Forster Saarland University, Steven Schäfer Saarland University, Simon Spies Saarland University, Kathrin Stark Saarland University, Germany DOI | ||
12:00 30mResearch paper | Eliminating Reflection from Type Theory CPP DOI |
14:00 - 15:30 | |||
14:00 30mResearch paper | Formally Verified Big Step Semantics out of x86-64 Binaries CPP Ian Roessle Virginia Tech, USA, Freek Verbeek Open University of the Netherlands, The Netherlands, Binoy Ravindran Virginia Tech DOI | ||
14:30 30mResearch paper | Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions CPP DOI | ||
15:00 30mResearch paper | From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server CPP Nicolas Koh , Yao Li University of Pennsylvania, Yishuai Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Lennart Beringer Princeton University, Wolf Honore , William Mansky University of Illinois at Chicago, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI |
16:00 - 17:30 | Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII Chair(s): Georges Gonthier Inria | ||
16:00 30mResearch paper | A Formal Proof of Hensel's Lemma over the p-adic Integers CPP Robert Y. Lewis Vrije Universiteit Amsterdam DOI | ||
16:30 30mResearch paper | Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem CPP DOI | ||
17:00 30mResearch paper | Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL CPP DOI |
Tue 15 JanDisplayed time zone: Belfast change
Tue 15 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | |||
09:00 60mTalk | Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL CPP Jasmin Blanchette Vrije Universiteit Amsterdam DOI | ||
10:00 30mResearch paper | A Verified Prover Based on Ordered Resolution CPP Anders Schlichtkrull Technical University of Denmark, Jasmin Blanchette Vrije Universiteit Amsterdam, Dmitriy Traytel ETH Zurich DOI |
11:00 - 12:30 | Research Papers: Rewriting, Automated ReasoningCPP at Sala XII Chair(s): Andrei Popescu Middlesex University, London | ||
11:00 30mResearch paper | Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions CPP DOI | ||
11:30 30mResearch paper | Certified ACKBO CPP DOI | ||
12:00 30mResearch paper | A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL CPP DOI |
14:00 - 15:30 | |||
14:00 30mResearch paper | A Verified Protocol Buffer Compiler CPP DOI | ||
14:30 30mResearch paper | A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra CPP DOI | ||
15:00 30mResearch paper | Dynamic Class Initialization Semantics: a Jinja Extension CPP DOI |
16:00 - 17:30 | Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII Chair(s): Zhong Shao Yale University | ||
16:00 30mResearch paper | On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem CPP Yannick Forster Saarland University, Dominik Kirst Saarland University, Gert Smolka Saarland University DOI | ||
16:30 30mResearch paper | Verified Solving and Asymptotics of Linear Recurrences CPP Manuel Eberl Technische Universität München DOI | ||
17:00 30mMeeting | Business Meeting CPP |