Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
VenueHotel Cascais Miragem
Room nameSala XII
Floor0
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

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
60m
Talk
A Linear Logical Framework in Hybrid
CPP
Amy Felty University of Ottawa
DOI
10:00
30m
Research paper
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
CPP
Yannick Forster Saarland University, Dominique Larchey-Wendling CNRS, LORIA
DOI
11:00 - 12:30
Research Papers: Proof Theory, Theory of Programming LanguagesCPP at Sala XII
Chair(s): Assia Mahboubi INRIA
11:00
30m
Research 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
30m
Research 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
30m
Research paper
Eliminating Reflection from Type Theory
CPP
Théo Winterhalter Gallinette / Inria / LS2N, Nicolas Tabareau Inria, Matthieu Sozeau Inria
DOI
14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Chris Hawblitzel Microsoft Research
14:00
30m
Research 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
30m
Research paper
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
CPP
Sandrine Blazy Univ Rennes- IRISA, Rémi Hutin IRISA / ENS Rennes
DOI
15:00
30m
Research 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
30m
Research paper
A Formal Proof of Hensel's Lemma over the p-adic Integers
CPP
Robert Y. Lewis Vrije Universiteit Amsterdam
DOI
16:30
30m
Research paper
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
CPP
Wenda Li University of Cambridge, Lawrence Paulson University of Cambridge
DOI
17:00
30m
Research paper
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
CPP
DOI

Tue 15 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Keynote 2 and Research PaperCPP at Sala XII
Chair(s): Assia Mahboubi INRIA
09:00
60m
Talk
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
CPP
Jasmin Blanchette Vrije Universiteit Amsterdam
DOI
10:00
30m
Research 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
30m
Research paper
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
CPP
Kathrin Stark Saarland University, Germany, Steven Schäfer Saarland University, Jonas Kaiser
DOI
11:30
30m
Research paper
Certified ACKBO
CPP
Alexander Lochmann , Christian Sternagel University of Innsbruck, Austria
DOI
12:00
30m
Research paper
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
CPP
DOI
14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Nicolas Tabareau Inria
14:00
30m
Research paper
A Verified Protocol Buffer Compiler
CPP
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
DOI
14:30
30m
Research paper
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
CPP
Véronique Benzaken LRI, Université Paris-Sud, Evelyne Contejean
DOI
15:00
30m
Research paper
Dynamic Class Initialization Semantics: a Jinja Extension
CPP
Susannah Mansky , Elsa Gunter University of Illinois
DOI
16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Zhong Shao Yale University
16:00
30m
Research 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
30m
Research paper
Verified Solving and Asymptotics of Linear Recurrences
CPP
Manuel Eberl Technische Universität München
DOI
17:00
30m
Meeting
Business Meeting
CPP
Assia Mahboubi INRIA, Magnus O. Myreen Chalmers University of Technology, Sweden