Museum A - POPL 2018

VenueOmni Hotel

Room nameMuseum A

Floor0

Additional informationThere is no additional information of this room available.

Program

Time Zone

The program is currently displayed in (GMT-08:00) Tijuana, Baja California.

Use conference time zone: (GMT-08:00) Tijuana, Baja CaliforniaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

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 - 10:00 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 - 11:00 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 - 11:30 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 - 12:00 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 - 14:00 Talk		Mechanising and Verifying the WebAssembly Specification CPP Conrad WattUniversity of Cambridge, UK DOI
	14:00 - 14:30 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 - 15:00 Talk		Mechanising Blockchain Consensus CPP 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 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 - 16:30 Talk		Triangulating Context Lemmas CPP Craig McLaughlinThe University of Edinburgh, James McKinna, Ian StarkThe University of Edinburgh DOI
	16:30 - 17:00 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 - 17:30 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 - 18:00 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 - 20:15 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 - 10:00 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 - 11:00 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 - 11:30 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 - 12:00 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 - 14:00 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 - 14:30 Talk		Generic Derivation of Induction for Impredicative Encodings in Cedille CPP 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 CPP Dominik KirstSaarland University, Gert SmolkaSaarland University DOI
	15:00 - 15:30 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 - 16:30 Talk		HOpi in Coq CPP 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 CPP Paweł WieczorekUniversity of Wrocław, Dariusz BiernackiUniversity of Wrocław DOI
	17:00 - 17:30 Talk		A Two-Level Logic Perspective on (Simultaneous) Substitutions CPP Kaustuv ChaudhuriInria, France DOI
	17:30 - 18:00 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


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																		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


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
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


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


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

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

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

CPP

CPP

CPP

CPP

CPP

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

CPP

CPP

CPP

CPP

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

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

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposiums

Room information: Museum A

Program Display Configuration

Mon 8 Jan Times are displayed in time zone: Tijuana, Baja California change

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

Mon 8 Jan Times are displayed in time zone: Tijuana, Baja California change

CPP

CPP

CPP

CPP

CPP

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

CPP

CPP

CPP

CPP

Mon 8 Jan Times are displayed in time zone: Tijuana, Baja California change

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

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

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

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

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

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

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