Museum A - POPL 2018

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 AndronickData61,CSIRO (formerly NICTA) and UNSW

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čarTechnische Universität München, Germany, René ThiemannUniversity of Innsbruck, Akihisa Yamada

DOI

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

10:30 - 11:00
Talk

Total Haskell is Reasonable Coq

Antal Spector-Zabusky, Joachim BreitnerUniversity of Pennsylvania, Christine RizkallahUniversity of Pennsylvania, USA, Stephanie WeirichUniversity of Pennsylvania, USA

DOI

11:00 - 11:30
Talk

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

Damien RouhlingUniversity of Côte d'Azur, France

DOI

11:30 - 12:00
Talk

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

Christian DoczkalCNRS, France, Joachim BardSaarland University, Germany

DOI

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

13:30 - 14:00
Talk

Mechanising and Verifying the WebAssembly Specification

Conrad WattUniversity of Cambridge, UK

DOI

14:00 - 14:30
Talk

Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL

Sidney AmaniUNSW, Australia, Myriam BégelENS Paris-Saclay, France, Maksym Bortin, Mark StaplesCSIRO, Australia

DOI

14:30 - 15:00
Talk

Mechanising Blockchain Consensus

George PîrleaUniversity College London, Ilya SergeyUniversity College London

DOI Pre-print

15:00 - 15:30
Talk

Formal Microeconomic Foundations and the First Welfare Theorem

Cezary KaliszykUniversity of Innsbruck, Julian ParsertUniversity of Innsbruck, Austria

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

16:00 - 16:30
Talk

Triangulating Context Lemmas

Craig McLaughlinThe University of Edinburgh, James McKinna, Ian StarkThe University of Edinburgh

DOI

16:30 - 17:00
Talk

Adapting Proof Automation to Adapt Proofs

Talia RingerUniversity of Washington, Nathaniel YazdaniUniversity of Washington, Seattle, John LeoHalfaya Research, Dan GrossmanUniversity of Washington

DOI

17:00 - 17:30
Talk

A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations

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 - 18:00
Talk

Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations

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 2018 - CPP Reception at Museum A

18:15 - 20:15
Social Event

CPP Reception

Tue 9 Jan

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

09:00 - 10:00
Talk

POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)

Brigitte PientkaMcGill University

DOI

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

10:30 - 11:00
Talk

A Verified SAT Solver with Watched Literals Using Imperative HOL

Mathias FleuryMPI-INF, Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Peter LammichTechnische Universität München

DOI

11:00 - 11:30
Talk

Œuf: Minimizing the Coq Extraction TCB

Eric MullenUniversity of Washington, Stuart PernsteinerUniversity of Washington, USA, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Dan GrossmanUniversity of Washington

DOI

11:30 - 12:00
Talk

Proofs in Conflict-Driven Theory Combination

Maria Paola BonacinaUniversity of Verona, Italy, Stéphane Graham-LengrandCNRS, France, Natarajan ShankarSRI International, USA

DOI

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

13:30 - 14:00
Talk

Finite Sets in Homotopy Type Theory

Dan FruminRadboud University, Herman GeuversRadboud University Nijmegen, Netherlands, Léon GondelmanLRI, Université Paris-Sud, Niels van der WeideRadboud University Nijmegen, Netherlands

DOI

14:00 - 14:30
Talk

Generic Derivation of Induction for Impredicative Encodings in Cedille

Denis FirsovUniversity of Iowa, USA, Aaron StumpUniversity of Iowa, USA

DOI

14:30 - 15:00
Talk

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

Dominik KirstSaarland University, Gert SmolkaSaarland University

DOI

15:00 - 15:30
Talk

A Constructive Formalisation of Semi-algebraic Sets and Functions

Boris DjalalINRIA

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

16:00 - 16:30
Talk

HOpi in Coq

Sergueï LengletUniversity of Lorraine, France, Alan SchmittInria

DOI

16:30 - 17:00
Talk

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

Paweł WieczorekUniversity of Wrocław, Dariusz BiernackiUniversity of Wrocław

DOI

17:00 - 17:30
Talk

A Two-Level Logic Perspective on (Simultaneous) Substitutions

Kaustuv ChaudhuriInria, France

DOI

17:30 - 18:00
Talk

Binder Aware Recursion over Well-Scoped de Bruijn Syntax

Jonas Kaiser, Steven Schäfer, Kathrin StarkSaarland University, Germany

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 Invited Talk by René Thiemann 09:00 - 10:00																		CPP Verifying Programs and Systems 10:30 - 12:00																																				CPP Verified Applications 13:30 - 15:30																														CPP Proof Methods and Libraries 16:00 - 18:00																											CPP 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 Invited Talk by Brigitte Pientka 09:00 - 10:00																		CPP Trusted Verification Frameworks and Systems 10:30 - 12:00																																				CPP Type Theory, Set Theory, and Formalized Mathematics 13:30 - 15:30																														CPP 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 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 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 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

Room information: Museum A

Mon 8 Jan

Tue 9 Jan

Mon 8 Jan 2018

CPP

CPP

CPP

CPP

CPP

Tue 9 Jan 2018

CPP

CPP

CPP

CPP

Mon 8 Jan 2018

Tue 9 Jan 2018

Tracks

Co-hosted Conferences

Co-hosted Workshops

Co-hosted Symposiums