POPL 2018
Sun 7 - Sat 13 January 2018
Los Angeles, California, United States
Toggle navigation
Attending
Venue: Omni Hotel
Registration
Code of Conduct
Supporting POPL
Childcare
Students
Visa Support Letter
Accessibility
Remote Participation
Program
Complete Program
Your Program
Proceedings
Filter by Day
Sun 7 Jan
Mon 8 Jan
Tue 9 Jan
Wed 10 Jan
Thu 11 Jan
Fri 12 Jan
Sat 13 Jan
Tracks
POPL 2018
Research Papers
TutorialFest
Student Research Competition
Workshops
Artifact Evaluation
Student Volunteers
Co-hosted Conferences
CPP
CPP
CPP
VMCAI
Workshops
PPS
CoqPL
NetPL
Off the Beaten Track
PEPM
PLMW
PriSC
Co-hosted Symposia
PADL
Organization
POPL 2018 Committees
Organizing Committee
Steering Committee
Track Committees
Research Papers
TutorialFest
Student Research Competition
Workshops
Artifact Evaluation
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Invited Speakers
Invited Tutorial
Organizing Committee
Travel Grants
Program Committee
Workshops
PPS
Program Committee
CoqPL
Organizing Committee
Program Committee
NetPL
Organizing Committee
Off the Beaten Track
Organizing Committee
Program Committee
PEPM
Programme Committee
Steering Committee
PLMW
Speakers
Panelists
Organizers
PriSC
Program Committee
Organizing Committee
Co-hosted Symposia
PADL
Publicity Chair
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 2018
(
series
) /
Omni Hotel
/
Room information: Museum A
Venue
Omni Hotel
Room name
Museum A
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-08:00) Tijuana, Baja California
.
Use conference time zone: (GMT-08:00) Tijuana, Baja California
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 8 Jan
Displayed time zone:
Tijuana, Baja California
change
09:00 - 10:00
Invited Talk by René Thiemann
CPP
at
Museum A
Chair(s):
June Andronick
Data61,CSIRO (formerly NICTA) and UNSW
09:00
60m
Talk
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
Verifying Programs and Systems
CPP
at
Museum A
Chair(s):
Natarajan Shankar
SRI International, USA
10:30
30m
Talk
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
30m
Talk
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
30m
Talk
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
CPP
Christian Doczkal
CNRS, France
,
Joachim Bard
Saarland University, Germany
DOI
13:30 - 15:30
Verified Applications
CPP
at
Museum A
Chair(s):
K. Rustan M. Leino
Amazon
13:30
30m
Talk
Mechanising and Verifying the WebAssembly Specification
CPP
Conrad Watt
University of Cambridge, UK
DOI
14:00
30m
Talk
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
30m
Talk
Mechanising Blockchain Consensus
CPP
George Pîrlea
University College London
,
Ilya Sergey
University College London
DOI
Pre-print
15:00
30m
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
CPP
Cezary Kaliszyk
University of Innsbruck
,
Julian Parsert
University of Innsbruck, Austria
16:00 - 18:00
Proof Methods and Libraries
CPP
at
Museum A
Chair(s):
René Thiemann
University of Innsbruck
16:00
30m
Talk
Triangulating Context Lemmas
CPP
Craig McLaughlin
The University of Edinburgh
,
James McKinna
,
Ian Stark
The University of Edinburgh
DOI
16:30
30m
Talk
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
30m
Talk
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
30m
Talk
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
CPP Reception
CPP
at
Museum A
18:15
2h
Social Event
CPP Reception
CPP
Tue 9 Jan
Displayed time zone:
Tijuana, Baja California
change
09:00 - 10:00
Invited Talk by Brigitte Pientka
CPP
at
Museum A
Chair(s):
Amy Felty
University of Ottawa
09:00
60m
Talk
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
CPP
Brigitte Pientka
McGill University
DOI
10:30 - 12:00
Trusted Verification Frameworks and Systems
CPP
at
Museum A
Chair(s):
Zhong Shao
Yale University
10:30
30m
Talk
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
30m
Talk
Œ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
30m
Talk
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 Mathematics
CPP
at
Museum A
Chair(s):
Thorsten Altenkirch
University of Nottingham
13:30
30m
Talk
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
30m
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
CPP
Denis Firsov
University of Iowa, USA
,
Aaron Stump
University of Iowa, USA
DOI
14:30
30m
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
CPP
Dominik Kirst
Saarland University
,
Gert Smolka
Saarland University
DOI
15:00
30m
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
CPP
Boris Djalal
INRIA
16:00 - 18:00
Formalizing Meta-Theory
CPP
at
Museum A
Chair(s):
Brigitte Pientka
McGill University
16:00
30m
Talk
HOpi in Coq
CPP
Sergueï Lenglet
University of Lorraine, France
,
Alan Schmitt
Inria
DOI
16:30
30m
Talk
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
CPP
Paweł Wieczorek
University of Wrocław
,
Dariusz Biernacki
University of Wrocław
DOI
17:00
30m
Talk
A Two-Level Logic Perspective on (Simultaneous) Substitutions
CPP
Kaustuv Chaudhuri
Inria, France
DOI
17:30
30m
Talk
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
CPP
Jonas Kaiser
,
Steven Schäfer
,
Kathrin Stark
Saarland University, Germany
DOI
Mon 8 Jan
Displayed time zone:
Tijuana, Baja California
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
18:00
30
19:00
30
20:00
30
Museum A
CPP
Invited Talk by René Thiemann
CPP
Verifying Programs and Systems
CPP
Verified Applications
CPP
Proof Methods and Libraries
CPP
CPP Reception
Tue 9 Jan
Displayed time zone:
Tijuana, Baja California
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
Museum A
CPP
Invited Talk by Brigitte Pientka
CPP
Trusted Verification Frameworks and Systems
CPP
Type Theory, Set Theory, and Formalized Mathematics
CPP
Formalizing Meta-Theory
Mon 8 Jan
Displayed time zone:
Tijuana, Baja California
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
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
Museum A
CPP
Efficient Certification of Complexity Proofs: Formalizing the Perron–Fr ...
09:00 - 10:00
CPP
Total Haskell is Reasonable Coq
10:30 - 11:00
CPP
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
11:00 - 11:30
CPP
Completeness and Decidability of Converse PDL in the Constructive Type ...
11:30 - 12:00
CPP
Mechanising and Verifying the WebAssembly Specification
13:30 - 14:00
CPP
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
14:00 - 14:30
CPP
Mechanising Blockchain Consensus
14:30 - 15:00
CPP
Formal Microeconomic Foundations and the First Welfare Theorem
15:00 - 15:30
CPP
Triangulating Context Lemmas
16:00 - 16:30
CPP
Adapting Proof Automation to Adapt Proofs
16:30 - 17:00
CPP
A Monadic Framework for Relational Verification: Applied to Information ...
17:00 - 17:30
CPP
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
17:30 - 18:00
CPP
CPP Reception
18:15 - 20:15
Tue 9 Jan
Displayed time zone:
Tijuana, Baja California
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
Museum A
CPP
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
09:00 - 10:00
CPP
A Verified SAT Solver with Watched Literals Using Imperative HOL
10:30 - 11:00
CPP
Œuf: Minimizing the Coq Extraction TCB
11:00 - 11:30
CPP
Proofs in Conflict-Driven Theory Combination
11:30 - 12:00
CPP
Finite Sets in Homotopy Type Theory
13:30 - 14:00
CPP
Generic Derivation of Induction for Impredicative Encodings in Cedille
14:00 - 14:30
CPP
Large Model Constructions for Second-Order ZF in Dependent Type Theory
14:30 - 15:00
CPP
A Constructive Formalisation of Semi-algebraic Sets and Functions
15:00 - 15:30
CPP
HOpi in Coq
16:00 - 16:30
CPP
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type ...
16:30 - 17:00
CPP
A Two-Level Logic Perspective on (Simultaneous) Substitutions
17:00 - 17:30
CPP
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
17:30 - 18:00
x
Mon 4 Nov 05:13