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

Conference Day
Mon 14 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Keynote 1 and Research PaperCPP at Sala XII
Chair(s): Magnus O. MyreenChalmers University of Technology, Sweden
09:00
60m
Talk
A Linear Logical Framework in Hybrid
CPP
Amy FeltyUniversity of Ottawa
DOI
10:00
30m
Research paper
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
CPP
Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA
DOI
11:00 - 12:30
Research Papers: Proof Theory, Theory of Programming LanguagesCPP at Sala XII
Chair(s): Assia MahboubiINRIA
11:00
30m
Research paper
A Proof-Theoretic Approach to Certifying Skolemization
CPP
Kaustuv ChaudhuriInria, France, Matteo ManighettiInria & École Polytechnique, Dale MillerINRIA Saclay and LIX
DOI
11:30
30m
Research paper
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
CPP
Yannick ForsterSaarland University, Steven SchäferSaarland University, Simon SpiesSaarland University, Kathrin StarkSaarland University, Germany
DOI
12:00
30m
Research paper
Eliminating Reflection from Type Theory
CPP
Theo WinterhalterGallinette / Inria / LS2N, Nicolas TabareauInria, Matthieu SozeauInria
DOI
14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Chris HawblitzelMicrosoft Research
14:00
30m
Research paper
Formally Verified Big Step Semantics out of x86-64 Binaries
CPP
Ian RoessleVirginia Tech, USA, Freek VerbeekOpen University of the Netherlands, The Netherlands, Binoy RavindranVirginia Tech
DOI
14:30
30m
Research paper
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
CPP
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes
DOI
15:00
30m
Research paper
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
CPP
Nicolas Koh, Yao LiUniversity of Pennsylvania, Yishuai LiUniversity of Pennsylvania, Li-yao XiaUniversity of Pennsylvania, Lennart BeringerPrinceton University, Wolf Honore, William ManskyUniversity of Illinois at Chicago, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
DOI
16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Georges GonthierInria
16:00
30m
Research paper
A Formal Proof of Hensel's Lemma over the p-adic Integers
CPP
Robert Y. LewisVrije Universiteit Amsterdam
DOI
16:30
30m
Research paper
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
CPP
Wenda LiUniversity of Cambridge, Lawrence PaulsonUniversity of Cambridge
DOI
17:00
30m
Research paper
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
CPP
DOI

Conference Day
Tue 15 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Keynote 2 and Research PaperCPP at Sala XII
Chair(s): Assia MahboubiINRIA
09:00
60m
Talk
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
CPP
Jasmin BlanchetteVrije Universiteit Amsterdam
DOI
10:00
30m
Research paper
A Verified Prover Based on Ordered Resolution
CPP
Anders SchlichtkrullTechnical University of Denmark, Jasmin BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich
DOI
11:00 - 12:30
Research Papers: Rewriting, Automated ReasoningCPP at Sala XII
Chair(s): Andrei PopescuMiddlesex University, London
11:00
30m
Research paper
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
CPP
Kathrin StarkSaarland University, Germany, Steven SchäferSaarland University, Jonas Kaiser
DOI
11:30
30m
Research paper
Certified ACKBO
CPP
Alexander Lochmann, Christian SternagelUniversity 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 TabareauInria
14:00
30m
Research paper
A Verified Protocol Buffer Compiler
CPP
Qianchuan YePurdue University, Benjamin DelawarePurdue 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 BenzakenLRI, Université Paris-Sud, Evelyne Contejean
DOI
15:00
30m
Research paper
Dynamic Class Initialization Semantics: a Jinja Extension
CPP
Susannah Mansky, Elsa GunterUniversity of Illinois
DOI
16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Zhong ShaoYale University
16:00
30m
Research paper
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
CPP
Yannick ForsterSaarland University, Dominik KirstSaarland University, Gert SmolkaSaarland University
DOI
16:30
30m
Research paper
Verified Solving and Asymptotics of Linear Recurrences
CPP
Manuel EberlTechnische Universität München
DOI
17:00
30m
Meeting
Business Meeting
CPP
Assia MahboubiINRIA, Magnus O. MyreenChalmers University of Technology, Sweden