Museum A - POPL 2018

Sun 7 - Sat 13 January 2018 Los Angeles, California, United States

VenueOmni Hotel

Room nameMuseum A

Floor0

Room number

Capacity0

Additional informationThere is no additional information of this room available.

Program

Mon 8 Jan

09:00 - 10:00: CPP 2018 - Invited Talk by René Thiemann at Museum A
Chair(s): June Andronick

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

10:30 - 12:00: CPP 2018 - Verifying Programs and Systems at Museum A
Chair(s): Natarajan Shankar

10:30 - 11:00
Talk

Total Haskell is Reasonable Coq

Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich

11:00 - 11:30
Talk

A Formal Proof in Coq of a Control Function for the Inverted Pendulum

Damien Rouhling

11:30 - 12:00
Talk

Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq

Christian Doczkal, Joachim Bard

13:30 - 15:30: CPP 2018 - Verified Applications at Museum A
Chair(s): K. Rustan M. Leino

13:30 - 14:00
Talk

Mechanising and Verifying the WebAssembly Specification

14:00 - 14:30
Talk

Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL

Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples

14:30 - 15:00
Talk

Mechanising Blockchain Consensus

George Pîrlea, Ilya Sergey

15:00 - 15:30
Talk

Formal Microeconomic Foundations and the First Welfare Theorem

Cezary Kaliszyk, Julian Parsert

16:00 - 18:00: CPP 2018 - Proof Methods and Libraries at Museum A
Chair(s): René Thiemann

16:00 - 16:30
Talk

Triangulating Context Lemmas

Craig McLaughlin, James McKinna, Ian Stark

16:30 - 17:00
Talk

Adapting Proof Automation to Adapt Proofs

Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman

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

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

18:15 - 20:15: CPP 2018 - CPP Reception at Museum A

18:15 - 20:15
Social Event

Tue 9 Jan

09:00 - 10:00: CPP 2018 - Invited Talk by Brigitte Pientka at Museum A
Chair(s): Amy Felty

09:00 - 10:00
Talk

POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)

Brigitte Pientka

10:30 - 12:00: CPP 2018 - Trusted Verification Frameworks and Systems at Museum A
Chair(s): Zhong Shao

10:30 - 11:00
Talk

A Verified SAT Solver with Watched Literals Using Imperative HOL

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich

11:00 - 11:30
Talk

Œuf: Minimizing the Coq Extraction TCB

Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman

11:30 - 12:00
Talk

Proofs in Conflict-Driven Theory Combination

Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar

13:30 - 15:30: CPP 2018 - Type Theory, Set Theory, and Formalized Mathematics at Museum A
Chair(s): Thorsten Altenkirch

13:30 - 14:00
Talk

Finite Sets in Homotopy Type Theory

Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide

14:00 - 14:30
Talk

Generic Derivation of Induction for Impredicative Encodings in Cedille

Denis Firsov, Aaron Stump

14:30 - 15:00
Talk

Large Model Constructions for Second-Order ZF in Dependent Type Theory

Dominik Kirst, Gert Smolka

15:00 - 15:30
Talk

A Constructive Formalisation of Semi-algebraic Sets and Functions

16:00 - 18:00: CPP 2018 - Formalizing Meta-Theory at Museum A
Chair(s): Brigitte Pientka

16:00 - 16:30
Talk

Sergueï Lenglet, Alan Schmitt

16:30 - 17:00
Talk

A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory

Paweł Wieczorek, Dariusz Biernacki

17:00 - 17:30
Talk

A Two-Level Logic Perspective on (Simultaneous) Substitutions

Kaustuv Chaudhuri

17:30 - 18:00
Talk

Binder Aware Recursion over Well-Scoped de Bruijn Syntax

Jonas Kaiser, Steven Schäfer, Kathrin Stark

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