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
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by René ThiemannCPP at Museum A
Chair(s): June AndronickData61,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čarTechnische Universität München, Germany, René ThiemannUniversity of Innsbruck, Akihisa Yamada
DOI
10:30 - 12:00
Verifying Programs and SystemsCPP at Museum A
Chair(s): Natarajan ShankarSRI International, USA
10:30
30m
Talk
Total Haskell is Reasonable Coq
CPP
Antal Spector-Zabusky, Joachim BreitnerUniversity of Pennsylvania, Christine RizkallahUniversity of Pennsylvania, USA, Stephanie WeirichUniversity of Pennsylvania, USA
DOI
11:00
30m
Talk
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
CPP
Damien RouhlingUniversity 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 DoczkalCNRS, France, Joachim BardSaarland University, Germany
DOI
13:30 - 15:30
Verified ApplicationsCPP at Museum A
Chair(s): K. Rustan M. LeinoAmazon
13:30
30m
Talk
Mechanising and Verifying the WebAssembly Specification
CPP
Conrad WattUniversity of Cambridge, UK
DOI
14:00
30m
Talk
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
CPP
Sidney AmaniUNSW, Australia, Myriam BégelENS Paris-Saclay, France, Maksym Bortin, Mark StaplesCSIRO, Australia
DOI
14:30
30m
Talk
Mechanising Blockchain Consensus
CPP
George PîrleaUniversity College London, Ilya SergeyUniversity College London
DOI Pre-print
15:00
30m
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
CPP
Cezary KaliszykUniversity of Innsbruck, Julian ParsertUniversity of Innsbruck, Austria
16:00 - 18:00
Proof Methods and LibrariesCPP at Museum A
Chair(s): René ThiemannUniversity of Innsbruck
16:00
30m
Talk
Triangulating Context Lemmas
CPP
Craig McLaughlinThe University of Edinburgh, James McKinna, Ian StarkThe University of Edinburgh
DOI
16:30
30m
Talk
Adapting Proof Automation to Adapt Proofs
CPP
Talia RingerUniversity of Washington, Nathaniel YazdaniUniversity of Washington, Seattle, John LeoHalfaya Research, Dan GrossmanUniversity of Washington
DOI
17:00
30m
Talk
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
CPP
Niklas GrimmVienna University of Technology, Austria, Kenji MaillardInria Paris and ENS Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Matteo MaffeiSaarland University, Jonathan ProtzenkoMicrosoft Research, n.n., Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, Santiago Zanella-BéguelinMicrosoft Research, n.n.
DOI
17:30
30m
Talk
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
CPP
Hugo FéréeUniversity of Kent, UK, Samuel HymUniversity of Lille, France, Micaela Mayero, Jean-Yves MoyenUniversity of Copenhagen, Denmark, David NowakCNRS, France
DOI
18:15 - 20:15
CPP ReceptionCPP at Museum A
18:15
2h
Social Event
CPP Reception
CPP

Tue 9 Jan
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by Brigitte PientkaCPP at Museum A
Chair(s): Amy FeltyUniversity of Ottawa
09:00
60m
Talk
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
CPP
Brigitte PientkaMcGill University
DOI
10:30 - 12:00
Trusted Verification Frameworks and SystemsCPP at Museum A
Chair(s): Zhong ShaoYale University
10:30
30m
Talk
A Verified SAT Solver with Watched Literals Using Imperative HOL
CPP
Mathias FleuryMPI-INF, Jasmin BlanchetteVrije Universiteit Amsterdam, Peter LammichTechnische Universität München
DOI
11:00
30m
Talk
Œuf: Minimizing the Coq Extraction TCB
CPP
Eric MullenUniversity of Washington, Stuart PernsteinerUniversity of Washington, USA, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Dan GrossmanUniversity of Washington
DOI
11:30
30m
Talk
Proofs in Conflict-Driven Theory Combination
CPP
Maria Paola BonacinaUniversity of Verona, Italy, Stéphane Graham-LengrandCNRS, France, Natarajan ShankarSRI International, USA
DOI
13:30 - 15:30
Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A
Chair(s): Thorsten AltenkirchUniversity of Nottingham
13:30
30m
Talk
Finite Sets in Homotopy Type Theory
CPP
Dan FruminRadboud University, Herman GeuversRadboud University Nijmegen, Netherlands, Léon GondelmanLRI, Université Paris-Sud, Niels van der WeideRadboud University Nijmegen, Netherlands
DOI
14:00
30m
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
CPP
Denis FirsovUniversity of Iowa, USA, Aaron StumpUniversity of Iowa, USA
DOI
14:30
30m
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
CPP
Dominik KirstSaarland University, Gert SmolkaSaarland University
DOI
15:00
30m
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
CPP
Boris DjalalINRIA
16:00 - 18:00
Formalizing Meta-TheoryCPP at Museum A
Chair(s): Brigitte PientkaMcGill University
16:00
30m
Talk
HOpi in Coq
CPP
Sergueï LengletUniversity of Lorraine, France, Alan SchmittInria
DOI
16:30
30m
Talk
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
CPP
Paweł WieczorekUniversity of Wrocław, Dariusz BiernackiUniversity of Wrocław
DOI
17:00
30m
Talk
A Two-Level Logic Perspective on (Simultaneous) Substitutions
CPP
Kaustuv ChaudhuriInria, France
DOI
17:30
30m
Talk
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
CPP
Jonas Kaiser, Steven Schäfer, Kathrin StarkSaarland University, Germany
DOI

Mon 8 Jan
Times are displayed in 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
Times are displayed in 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
Times are displayed in 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
Times are displayed in 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