POPL 2018
Sun 7 - Sat 13 January 2018 Los Angeles, California, United States
POPL 2018 (series) / Omni Hotel /

Room information: Museum A

VenueOmni Hotel
Room nameMuseum A
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

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by René ThiemannCPP 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 SystemsCPP 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 ApplicationsCPP 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 LibrariesCPP 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 ReceptionCPP 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 PientkaCPP 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 SystemsCPP 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 MathematicsCPP 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-TheoryCPP 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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:0030
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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:00153045
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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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