Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019
Cascais, Portugal
Toggle navigation
Attending
Venue: Hotel Cascais Miragem
Online Participation
Registration
Visa
Information for Students
Code of Conduct
Supporting POPL
Program
POPL Program
Your Program
Filter by Day
Sun 13 Jan
Mon 14 Jan
Tue 15 Jan
Wed 16 Jan
Thu 17 Jan
Fri 18 Jan
Sat 19 Jan
Tracks
POPL 2019
Research Papers
Artifact Evaluation
TutorialFest
Student Research Competition
Workshops
Co-hosted Conferences
CPP
VMCAI
Workshops
BEAT
CoqPL
LAFI
(né PPS)
OPCT
Off the Beaten Track
PEPM
PLMW
@POPL
PriSC
Co-hosted Symposia
PADL
Organization
POPL 2019 Committees
Organizing Committee
Steering Committee
Track Committees
Research Papers
Artifact Evaluation
TutorialFest
Student Research Competition
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Invited Speakers
Organizing Committee
Program Committee
Workshops
BEAT
Organizing Committee
Program Committee
CoqPL
Organizing Committee
Program Committee
LAFI
Program Committee
Steering Committee
OPCT
Organizing Committee
Program Committee
Off the Beaten Track
Organizing Committee
Program Committee
PEPM
Program Committee
Steering Committee
PLMW
Organizing Committee
Speakers
Panelists
PriSC
Program Committee
Organizing Committee
Co-hosted Symposia
PADL
Organizing Committee
Program Committee
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2019
(
series
) /
Hotel Cascais Miragem
/
Room information: Sala XII
Venue
Hotel Cascais Miragem
Room name
Sala XII
Floor
0
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT) Belfast
.
Use conference time zone: (GMT) Belfast
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-03:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-02:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
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 Paper
CPP
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 Languages
CPP
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 Verification
CPP
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 Algebra
CPP
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
Fabian Immler
,
Bohua Zhan
DOI
Tue 15 Jan
Displayed time zone:
Belfast
change
09:00 - 10:30
Keynote 2 and Research Paper
CPP
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 Reasoning
CPP
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
Bertram Felgenhauer
,
Aart Middeldorp
,
Turaga Prathamesh
,
Franziska Rapp
DOI
14:00 - 15:30
Research Papers: Program Verification
CPP
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 Algebra
CPP
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
Mon 14 Jan
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Sala XII
CPP
Keynote 1 and Research Paper
CPP
Research Papers: Proof Theory, Theory of Programming Languages
CPP
Research Papers: Program Verification
CPP
Research Papers: Formalization of Mathematics and Computer Algebra
Tue 15 Jan
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Sala XII
CPP
Keynote 2 and Research Paper
CPP
Research Papers: Rewriting, Automated Reasoning
CPP
Research Papers: Program Verification
CPP
Research Papers: Formalization of Mathematics and Computer Algebra
Mon 14 Jan
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Sala XII
CPP
A Linear Logical Framework in Hybrid
09:00 - 10:00
CPP
Certified Undecidability of Intuitionistic Linear Logic via Binary Stac ...
10:00 - 10:30
CPP
A Proof-Theoretic Approach to Certifying Skolemization
11:00 - 11:30
CPP
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
11:30 - 12:00
CPP
Eliminating Reflection from Type Theory
12:00 - 12:30
CPP
Formally Verified Big Step Semantics out of x86-64 Binaries
14:00 - 14:30
CPP
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Ari ...
14:30 - 15:00
CPP
From C to Interaction Trees: Specifying, Verifying, and Testing a Netwo ...
15:00 - 15:30
CPP
A Formal Proof of Hensel's Lemma over the p-adic Integers
16:00 - 16:30
CPP
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan- ...
16:30 - 17:00
CPP
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
17:00 - 17:30
Tue 15 Jan
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Sala XII
CPP
Formalizing the Metatheory of Logical Calculi and Automatic Provers in ...
09:00 - 10:00
CPP
A Verified Prover Based on Ordered Resolution
10:00 - 10:30
CPP
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Sub ...
11:00 - 11:30
CPP
Certified ACKBO
11:30 - 12:00
CPP
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite ...
12:00 - 12:30
CPP
A Verified Protocol Buffer Compiler
14:00 - 14:30
CPP
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally ...
14:30 - 15:00
CPP
Dynamic Class Initialization Semantics: a Jinja Extension
15:00 - 15:30
CPP
On Synthetic Undecidability in Coq, with an Application to the Entschei ...
16:00 - 16:30
CPP
Verified Solving and Asymptotics of Linear Recurrences
16:30 - 17:00
CPP
Business Meeting
17:00 - 17:30
x
Sat 21 Dec 15:25