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
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 Symposiums
PADL
Organization
POPL 2018
Organizing Committee
Steering Committee
Research Papers
Program Committee
TutorialFest
Organizers
Student Research Competition
Selection Committee
Workshops
Selection Committee
Artifact Evaluation
Artifact Evaluation Committee
Student Volunteers
Organizers
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 Symposiums
PADL
Publicity Chair
Search
Series
Series
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
Additional information
There is no additional information of this room available.
Display in different time zone
The program is currently displayed in
(GMT-07:00) Tijuana, Baja California
.
Use conference time zone: (GMT-07:00) Tijuana, Baja California
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06: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-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04: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-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Greenwich Mean Time : Belfast
(GMT+01:00) Greenwich Mean Time : Dublin
(GMT+01:00) Greenwich Mean Time : Lisbon
(GMT+01:00) Greenwich Mean Time : London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+04: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+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) 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+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
Apply
Program
Detailed Table
Session Timeline
Detailed Timeline
×
You're viewing the program in a time zone which is different from your device's time zone -
change time zone
Mon 8 Jan
Times are displayed in time zone:
(GMT-07:00) Tijuana, Baja California
change
CPP-2018
09:00 - 10:00:
CPP 2018
- Invited Talk by René Thiemann at
Museum A
Chair(s):
June Andronick
Data61,CSIRO (formerly NICTA) and UNSW
CPP-2018
09:00 - 10:00
Talk
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón
,
Sebastiaan Joosten
,
Ondřej Kunčar
Technische Universität München, Germany
,
René Thiemann
University of Innsbruck
,
Akihisa Yamada
DOI
CPP-2018
10:30 - 12:00:
CPP 2018
- Verifying Programs and Systems at
Museum A
Chair(s):
Natarajan Shankar
SRI International, USA
CPP-2018
10:30 - 11:00
Talk
Total Haskell is Reasonable Coq
Antal Spector-Zabusky
,
Joachim Breitner
University of Pennsylvania
,
Christine Rizkallah
University of Pennsylvania, USA
,
Stephanie Weirich
University of Pennsylvania, USA
DOI
CPP-2018
11:00 - 11:30
Talk
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Damien Rouhling
University of Côte d'Azur, France
DOI
CPP-2018
11:30 - 12:00
Talk
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Christian Doczkal
CNRS, France
,
Joachim Bard
Saarland University, Germany
DOI
CPP-2018
13:30 - 15:30:
CPP 2018
- Verified Applications at
Museum A
Chair(s):
K. Rustan M. Leino
Amazon
CPP-2018
13:30 - 14:00
Talk
Mechanising and Verifying the WebAssembly Specification
Conrad Watt
University of Cambridge, UK
DOI
CPP-2018
14:00 - 14:30
Talk
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani
UNSW, Australia
,
Myriam Bégel
ENS Paris-Saclay, France
,
Maksym Bortin
,
Mark Staples
CSIRO, Australia
DOI
CPP-2018
14:30 - 15:00
Talk
Mechanising Blockchain Consensus
George Pîrlea
University College London
,
Ilya Sergey
University College London
DOI
Pre-print
CPP-2018
15:00 - 15:30
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk
University of Innsbruck
,
Julian Parsert
University of Innsbruck, Austria
CPP-2018
16:00 - 18:00:
CPP 2018
- Proof Methods and Libraries at
Museum A
Chair(s):
René Thiemann
University of Innsbruck
CPP-2018
16:00 - 16:30
Talk
Triangulating Context Lemmas
Craig McLaughlin
The University of Edinburgh
,
James McKinna
,
Ian Stark
The University of Edinburgh
DOI
CPP-2018
16:30 - 17:00
Talk
Adapting Proof Automation to Adapt Proofs
Talia Ringer
University of Washington
,
Nathaniel Yazdani
University of Washington, Seattle
,
John Leo
Halfaya Research
,
Dan Grossman
University of Washington
DOI
CPP-2018
17:00 - 17:30
Talk
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
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
CPP-2018
17:30 - 18:00
Talk
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
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
CPP-2018
18:15 - 20:15:
CPP 2018
- CPP Reception at
Museum A
CPP-2018
18:15 - 20:15
Social Event
CPP Reception
Tue 9 Jan
Times are displayed in time zone:
(GMT-07:00) Tijuana, Baja California
change
CPP-2018
09:00 - 10:00:
CPP 2018
- Invited Talk by Brigitte Pientka at
Museum A
Chair(s):
Amy Felty
University of Ottawa
CPP-2018
09:00 - 10:00
Talk
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
Brigitte Pientka
McGill University
DOI
CPP-2018
10:30 - 12:00:
CPP 2018
- Trusted Verification Frameworks and Systems at
Museum A
Chair(s):
Zhong Shao
Yale University
CPP-2018
10:30 - 11:00
Talk
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury
MPI-INF
,
Jasmin Blanchette
Vrije Universiteit Amsterdam
,
Peter Lammich
Technische Universität München
DOI
CPP-2018
11:00 - 11:30
Talk
Œuf: Minimizing the Coq Extraction TCB
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
CPP-2018
11:30 - 12:00
Talk
Proofs in Conflict-Driven Theory Combination
Maria Paola Bonacina
University of Verona, Italy
,
Stéphane Graham-Lengrand
CNRS, France
,
Natarajan Shankar
SRI International, USA
DOI
CPP-2018
13:30 - 15:30:
CPP 2018
- Type Theory, Set Theory, and Formalized Mathematics at
Museum A
Chair(s):
Thorsten Altenkirch
University of Nottingham
CPP-2018
13:30 - 14:00
Talk
Finite Sets in Homotopy Type Theory
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
CPP-2018
14:00 - 14:30
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov
University of Iowa, USA
,
Aaron Stump
University of Iowa, USA
DOI
CPP-2018
14:30 - 15:00
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik Kirst
Saarland University
,
Gert Smolka
Saarland University
DOI
CPP-2018
15:00 - 15:30
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
Boris Djalal
INRIA
CPP-2018
16:00 - 18:00:
CPP 2018
- Formalizing Meta-Theory at
Museum A
Chair(s):
Brigitte Pientka
McGill University
CPP-2018
16:00 - 16:30
Talk
HOpi in Coq
Sergueï Lenglet
University of Lorraine, France
,
Alan Schmitt
Inria
DOI
CPP-2018
16:30 - 17:00
Talk
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Paweł Wieczorek
University of Wrocław
,
Dariusz Biernacki
University of Wrocław
DOI
CPP-2018
17:00 - 17:30
Talk
A Two-Level Logic Perspective on (Simultaneous) Substitutions
Kaustuv Chaudhuri
Inria, France
DOI
CPP-2018
17:30 - 18:00
Talk
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Jonas Kaiser
,
Steven Schäfer
,
Kathrin Stark
Saarland University, Germany
DOI
Mon 8 Jan
Times are displayed in time zone:
(GMT-07:00) 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
Times are displayed in time zone:
(GMT-07:00) 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
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
Times are displayed in time zone:
(GMT-07:00) 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
Times are displayed in time zone:
(GMT-07:00) 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
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
Fri 18 Sep 18:50