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 2018
VMCAI 2018
Co-hosted Workshops
PPS 2018
CoqPL 2018
NetPL 2018
Off the Beaten Track 2018
PEPM 2018
PLMW 2018
PriSC 2018
Co-hosted Symposiums
PADL 2018
Committees
POPL 2018
Organizing Committee
Steering Committee
Tracks
Research Papers
Program Committee
TutorialFest
Organizers
Student Research Competition
Selection Committee
Workshops
Selection Committee
Artifact Evaluation
Artifact Evaluation Committee
Student Volunteers
Organizers
Co-hosted Conferences
CPP 2018
CPP 2018
Program Committee
VMCAI 2018
VMCAI 2018
Invited Speakers
VMCAI 2018
Invited Tutorial
VMCAI 2018
Organizing Committee
VMCAI 2018
Travel Grants
VMCAI 2018
Program Committee
Co-hosted Workshops
PPS 2018
PPS 2018
Program Committee
CoqPL 2018
Organizing Committee
Program Committee
NetPL 2018
NetPL 2018
Organizing Committee
Off the Beaten Track 2018
Off the Beaten Track 2018
Organizing Committee
Off the Beaten Track 2018
Program Committee
PEPM 2018
PEPM 2018
Programme Committee
PEPM 2018
Steering Committee
PLMW 2018
PLMW
Speakers
PLMW
Panelists
PLMW
Organizers
PriSC 2018
PriSC 2018
Program Committee
PriSC 2018
Organizing Committee
Co-hosted Symposiums
PADL 2018
PADL 2018
Organizing Committee
Search
Other Editions
Series
POPL 2019
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 number
Capacity
0
Additional information
There is no additional information of this room available.
Program
Detailed Table
Session Timeline
Detailed Timeline
Mon 8 Jan
CPP-2018
09:00 - 10:00:
CPP 2018
- Invited Talk by René Thiemann at
Museum A
Chair(s):
June Andronick
CPP-2018
1515398400000
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
,
René Thiemann
,
Akihisa Yamada
DOI
CPP-2018
10:30 - 12:00:
CPP 2018
- Verifying Programs and Systems at
Museum A
Chair(s):
Natarajan Shankar
CPP-2018
1515403800000
10:30 - 11:00
Talk
Total Haskell is Reasonable Coq
Antal Spector-Zabusky
,
Joachim Breitner
,
Christine Rizkallah
,
Stephanie Weirich
DOI
CPP-2018
1515405600000
11:00 - 11:30
Talk
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Damien Rouhling
DOI
CPP-2018
1515407400000
11:30 - 12:00
Talk
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Christian Doczkal
,
Joachim Bard
DOI
CPP-2018
13:30 - 15:30:
CPP 2018
- Verified Applications at
Museum A
Chair(s):
K. Rustan M. Leino
CPP-2018
1515414600000
13:30 - 14:00
Talk
Mechanising and Verifying the WebAssembly Specification
Conrad Watt
DOI
CPP-2018
1515416400000
14:00 - 14:30
Talk
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani
,
Myriam Bégel
,
Maksym Bortin
,
Mark Staples
DOI
CPP-2018
1515418200000
14:30 - 15:00
Talk
Mechanising Blockchain Consensus
George Pîrlea
,
Ilya Sergey
DOI
Pre-print
CPP-2018
1515420000000
15:00 - 15:30
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk
,
Julian Parsert
CPP-2018
16:00 - 18:00:
CPP 2018
- Proof Methods and Libraries at
Museum A
Chair(s):
René Thiemann
CPP-2018
1515423600000
16:00 - 16:30
Talk
Triangulating Context Lemmas
Craig McLaughlin
,
James McKinna
,
Ian Stark
DOI
CPP-2018
1515425400000
16:30 - 17:00
Talk
Adapting Proof Automation to Adapt Proofs
Talia Ringer
,
Nathaniel Yazdani
,
John Leo
,
Dan Grossman
DOI
CPP-2018
1515427200000
17:00 - 17:30
Talk
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm
,
Kenji Maillard
,
Cédric Fournet
,
Cătălin Hriţcu
,
Matteo Maffei
,
Jonathan Protzenko
,
Tahina Ramananandro
,
Aseem Rastogi
,
Nikhil Swamy
,
Santiago Zanella-Béguelin
DOI
CPP-2018
1515429000000
17:30 - 18:00
Talk
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée
,
Samuel Hym
,
Micaela Mayero
,
Jean-Yves Moyen
,
David Nowak
DOI
CPP-2018
18:15 - 20:15:
CPP 2018
- CPP Reception at
Museum A
CPP-2018
1515431700000
18:15 - 20:15
Social Event
CPP Reception
Tue 9 Jan
CPP-2018
09:00 - 10:00:
CPP 2018
- Invited Talk by Brigitte Pientka at
Museum A
Chair(s):
Amy Felty
CPP-2018
1515484800000
09:00 - 10:00
Talk
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
Brigitte Pientka
DOI
CPP-2018
10:30 - 12:00:
CPP 2018
- Trusted Verification Frameworks and Systems at
Museum A
Chair(s):
Zhong Shao
CPP-2018
1515490200000
10:30 - 11:00
Talk
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury
,
Jasmin Christian Blanchette
,
Peter Lammich
DOI
CPP-2018
1515492000000
11:00 - 11:30
Talk
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen
,
Stuart Pernsteiner
,
James R. Wilcox
,
Zachary Tatlock
,
Dan Grossman
DOI
CPP-2018
1515493800000
11:30 - 12:00
Talk
Proofs in Conflict-Driven Theory Combination
Maria Paola Bonacina
,
Stéphane Graham-Lengrand
,
Natarajan Shankar
DOI
CPP-2018
13:30 - 15:30:
CPP 2018
- Type Theory, Set Theory, and Formalized Mathematics at
Museum A
Chair(s):
Thorsten Altenkirch
CPP-2018
1515501000000
13:30 - 14:00
Talk
Finite Sets in Homotopy Type Theory
Dan Frumin
,
Herman Geuvers
,
Léon Gondelman
,
Niels van der Weide
DOI
CPP-2018
1515502800000
14:00 - 14:30
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov
,
Aaron Stump
DOI
CPP-2018
1515504600000
14:30 - 15:00
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik Kirst
,
Gert Smolka
DOI
CPP-2018
1515506400000
15:00 - 15:30
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
Boris Djalal
CPP-2018
16:00 - 18:00:
CPP 2018
- Formalizing Meta-Theory at
Museum A
Chair(s):
Brigitte Pientka
CPP-2018
1515510000000
16:00 - 16:30
Talk
HOpi in Coq
Sergueï Lenglet
,
Alan Schmitt
DOI
CPP-2018
1515511800000
16:30 - 17:00
Talk
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Paweł Wieczorek
,
Dariusz Biernacki
DOI
CPP-2018
1515513600000
17:00 - 17:30
Talk
A Two-Level Logic Perspective on (Simultaneous) Substitutions
Kaustuv Chaudhuri
DOI
CPP-2018
1515515400000
17:30 - 18:00
Talk
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Jonas Kaiser
,
Steven Schäfer
,
Kathrin Stark
DOI
Mon 8 Jan 2018
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 2018
Invited Talk by René Thiemann
09:00 - 10:00
CPP 2018
Verifying Programs and Systems
10:30 - 12:00
CPP 2018
Verified Applications
13:30 - 15:30
CPP 2018
Proof Methods and Libraries
16:00 - 18:00
CPP 2018
CPP Reception
18:15 - 20:15
Tue 9 Jan 2018
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 2018
Invited Talk by Brigitte Pientka
09:00 - 10:00
CPP 2018
Trusted Verification Frameworks and Systems
10:30 - 12:00
CPP 2018
Type Theory, Set Theory, and Formalized Mathematics
13:30 - 15:30
CPP 2018
Formalizing Meta-Theory
16:00 - 18:00
Mon 8 Jan 2018
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 2018
Efficient Certification of Complexity Proofs: Formalizing the Perron–Fr ...
09:00 - 10:00
CPP 2018
Total Haskell is Reasonable Coq
10:30 - 11:00
CPP 2018
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
11:00 - 11:30
CPP 2018
Completeness and Decidability of Converse PDL in the Constructive Type ...
11:30 - 12:00
CPP 2018
Mechanising and Verifying the WebAssembly Specification
13:30 - 14:00
CPP 2018
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
14:00 - 14:30
CPP 2018
Mechanising Blockchain Consensus
14:30 - 15:00
CPP 2018
Formal Microeconomic Foundations and the First Welfare Theorem
15:00 - 15:30
CPP 2018
Triangulating Context Lemmas
16:00 - 16:30
CPP 2018
Adapting Proof Automation to Adapt Proofs
16:30 - 17:00
CPP 2018
A Monadic Framework for Relational Verification: Applied to Information ...
17:00 - 17:30
CPP 2018
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
17:30 - 18:00
CPP 2018
CPP Reception
18:15 - 20:15
Tue 9 Jan 2018
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 2018
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
09:00 - 10:00
CPP 2018
A Verified SAT Solver with Watched Literals Using Imperative HOL
10:30 - 11:00
CPP 2018
Œuf: Minimizing the Coq Extraction TCB
11:00 - 11:30
CPP 2018
Proofs in Conflict-Driven Theory Combination
11:30 - 12:00
CPP 2018
Finite Sets in Homotopy Type Theory
13:30 - 14:00
CPP 2018
Generic Derivation of Induction for Impredicative Encodings in Cedille
14:00 - 14:30
CPP 2018
Large Model Constructions for Second-Order ZF in Dependent Type Theory
14:30 - 15:00
CPP 2018
A Constructive Formalisation of Semi-algebraic Sets and Functions
15:00 - 15:30
CPP 2018
HOpi in Coq
16:00 - 16:30
CPP 2018
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type ...
16:30 - 17:00
CPP 2018
A Two-Level Logic Perspective on (Simultaneous) Substitutions
17:00 - 17:30
CPP 2018
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
17:30 - 18:00
x
Wed 25 Apr 20:15