Auditorium - POPL 2017

VenueParis Jussieu

Room nameAuditorium

Floor0

Room numberAAA

Capacity500

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect 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 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00	Invited TalkCPP at Auditorium

09:00 60m Talk		Porting the HOL Light Analysis Library: Some Lessons CPP Lawrence Paulson University of Cambridge File Attached

10:30 - 12:00	Algorithm and library verificationCPP at Auditorium

10:30 30m Talk		Verifying a hash table and its iterators in higher-order separation logic CPP François Pottier
11:00 30m Talk		A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm CPP Jose Divasón , Sebastiaan Joosten , René Thiemann University of Innsbruck, Akihisa Yamada
11:30 30m Talk		Formal foundations of 3D geometry for modeling robot manipulators CPP Reynald Affeldt AIST, Japan, Cyril Cohen

14:00 - 15:30	Automated proof and its verificationCPP at Auditorium

14:00 30m Talk		BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP Jan Jakubuv , Josef Urban
14:30 30m Talk		Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP Reuben Rowe University College London, James Brotherston
15:00 30m Talk		Formalization of Karp-Miller Tree Construction on Petri Nets CPP Mitsuharu Yamamoto , Shogo Sekine , Saki Matsumoto

16:00 - 18:00	Formalized mathematics with numerical computationsCPP at Auditorium

16:00 30m Talk		A Coq Formal Proof of the Lax–Milgram theorem CPP Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero
16:30 30m Talk		A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations CPP Erik Martin-Dorel IRIT, Université Paul Sabatier, Pierre Roux
17:00 30m Talk		Markov Processes in Isabelle/HOL CPP Johannes Hölzl Technische Universität München DOI Pre-print File Attached
17:30 30m Talk		Formalising Real Numbers in Homotopy Type Theory CPP Gaetan Gilbert

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00	Invited TalkCPP at Auditorium

09:00 60m Talk		Mechanized verification of preemptive OS kernels CPP Xinyu Feng University of Science and Technology of China File Attached

10:30 - 12:00	Verified programming toolsCPP at Auditorium

10:30 30m Talk		Verified compilation of CakeML to multiple machine-code targets CPP Anthony Fox University of Cambridge, UK, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan IHPC at A*STAR, Singapore, Ramana Kumar
11:00 30m Talk		COMPLX: a verification framework for concurrent imperative programs CPP Sidney Amani UNSW, Australia, June Andronick Data61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin , Corey Lewis , Christine Rizkallah University of Pennsylvania, USA, Joseph Tuong
11:30 30m Talk		Verifying dynamic race detection CPP William Mansky University of Pennsylvania, Yuanfeng Peng University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Joseph Devietti University of Pennsylvania

14:00 - 15:30	Homotopy type theoryCPP at Auditorium

14:00 30m Talk		The HoTT library: a formalization of homotopy type theory in Coq CPP Andrej Bauer University of Ljubljana, Jason Gross MIT CSAIL, Peter Lefanu Lumsdaine , Michael Shulman , Matthieu Sozeau Inria, Bas Spitters Pre-print
14:30 30m Talk		Lifting proof-relevant unification to higher dimensions CPP Jesper Cockx iMinds, Belgium, Dominique Devriese iMinds - Distrinet, KU Leuven
15:00 30m Talk		The Next 700 Syntactical models of type theory CPP Simon Boulier , Pierre-Marie Pédrot , Nicolas Tabareau Inria, France

16:00 - 17:30	Formal verification of programming language foundationsCPP at Auditorium

16:00 30m Talk		Type-and-scope safe programs and their proofs CPP Guillaume Allais Radboud University Nijmegen, James Chapman , Conor McBride , James McKinna University of Edinburgh
16:30 30m Talk		Formally verified differential dynamic logic CPP Brandon Bohrer , Vincent Rahli SnT, Ivana Vukotic , Marcus Voelp , André Platzer
17:00 30m Talk		Equivalence of System F and λ2 in Coq based on context morphism lemmas CPP Jonas Kaiser , Tobias Tebbi , Gert Smolka Saarland University

Wed 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05	OpeningPOPL at Auditorium Chair(s): Giuseppe Castagna Paris Diderot University & CNRS, Andrew D. Gordon Microsoft Research and University of Edinburgh

09:00 5m Day opening		Opening POPL

09:05 - 10:00	Invited speakerPOPL at Auditorium Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh

09:05 55m Talk		The Influence of Dependent Types POPL Stephanie Weirich University of Pennsylvania

10:30 - 12:10	Type Systems 1POPL at Auditorium Chair(s): Avik Chaudhuri Facebook

10:30 25m Talk		Polymorphism, subtyping and type inference in MLsub POPL Stephen Dolan , Alan Mycroft University of Cambridge
10:55 25m Talk		Java generics are Turing complete POPL Radu Grigore University of Kent
11:20 25m Talk		Hazelnut: A Bidirectionally Typed Structure Editor Calculus POPL Cyrus Omar Carnegie Mellon University, Ian Voysey Carnegie Mellon University, Michael Hilton Oregon State University, USA, Jonathan Aldrich Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
11:45 25m Talk		Modules, Abstraction, and Parametric Polymorphism POPL Karl Crary Carnegie Mellon University

14:20 - 16:00	Concurrency 1POPL at Auditorium Chair(s): Ilya Sergey University College London

14:20 25m Talk		A Promising Semantics for Relaxed-Memory Concurrency POPL Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS Link to publication Pre-print Media Attached
14:45 25m Talk		Automatically Comparing Memory Consistency Models POPL John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UK Pre-print Media Attached File Attached
15:10 25m Talk		Interactive Proofs in Higher-Order Concurrent Separation Logic POPL Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus University DOI Pre-print Media Attached
15:35 25m Talk		A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic POPL Morten Krogh-Jespersen Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University

16:30 - 17:45	Compiler OptimisationPOPL at Auditorium Chair(s): Andrew Myers Cornell University

16:30 25m Talk		A Program Optimization for Automatic Database Result Caching POPL Ziv Scully Carnegie Mellon University, Adam Chlipala MIT
16:55 25m Talk		Stream Fusion, to Completeness POPL Oleg Kiselyov , Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens Pre-print Media Attached
17:20 25m Talk		Rigorous Floating-point Mixed Precision Tuning POPL Wei-Fan Chiang School of Computing, University of Utah, Ganesh Gopalakrishnan University of Utah, Zvonimir Rakamaric University of Utah, Ian Briggs School of Computing, University of Utah, Marek S. Baranowski University of Utah, Alexey Solovyev School of Computing, University of Utah Pre-print

Thu 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:15	ACM and SIGPLAN AwardsPOPL at Auditorium Chair(s): Satnam Singh Facebook

09:00 5m Awards		Turing Award Video POPL
09:05 5m Awards		Most Influential Paper Award POPL
09:10 5m Awards		Reynolds Doctoral Dissertation Award POPL

09:15 - 10:00	Invited speakerPOPL at Auditorium Chair(s): Roberto Giacobazzi University of Verona, Italy

09:15 45m Talk		40 Years of Abstract Interpretation — An Interview with Patrick Cousot POPL Patrick Cousot New York University, Roberto Giacobazzi University of Verona, Italy

10:30 - 12:10	Type Systems 2POPL at Auditorium Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh

10:30 25m Talk		Deciding equivalence with sums and the empty type POPL Gabriel Scherer Northeastern University
10:55 25m Talk		The exp-log normal form of types: Decomposing extensional equality and representing terms compactly POPL Danko Ilik Trusted Labs
11:20 25m Talk		Contextual isomorphisms POPL Paul Blain Levy
11:45 25m Talk		Typed Self-Evaluation via Intensional Type Functions POPL Matt Brown UCLA, Jens Palsberg University of California, Los Angeles

14:20 - 16:00	Functional Programming with EffectsPOPL at Auditorium Chair(s): Kathleen Fisher Tufts University

14:20 25m Talk		Type Directed Compilation of Row-Typed Algebraic Effects POPL Daan Leijen Microsoft Research
14:45 25m Talk		Do be do be do POPL Sam Lindley University of Edinburgh, Conor McBride , Craig McLaughlin The University of Edinburgh
15:10 25m Talk		Dijkstra Monads for Free POPL Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin , Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research Pre-print
15:35 25m Talk		Stateful Manifest Contracts POPL Taro Sekiyama , Atsushi Igarashi Kyoto University

16:30 - 17:20	Logic and ProgrammingPOPL at Auditorium Chair(s): Nada Amin EPFL

16:30 25m Talk		Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks POPL Kausik Subramanian University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison, Aditya Akella University of Wisconsin-Madison
16:55 25m Talk		LOIS: syntax and semantics POPL Eryk Kopczynski , Szymon Toruńczyk

17:20 - 18:20	Business meetingPOPL at Auditorium Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh

17:20 20m Talk		PC Chair report POPL Andrew D. Gordon Microsoft Research and University of Edinburgh
17:40 10m Talk		POPL 2018 presentation POPL Andrew Myers Cornell University, Ranjit Jhala University of California, San Diego
17:50 30m Meeting		SIGPLAN business meeting POPL C: Andrew D. Gordon Microsoft Research and University of Edinburgh

Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05	Student Competition AwardStudent Research Competition at Auditorium Chair(s): Kim Nguyễn LRI, Université Paris-Sud

09:00 5m Awards		Student Competition Award Student Research Competition

09:05 - 10:00	Invited speakerPOPL at Auditorium Chair(s): Giuseppe Castagna Paris Diderot University & CNRS

09:05 55m Talk		Rust: from POPL to practice POPL Aaron Turon MPI-SWS

10:30 - 12:10	Type Systems 3POPL at Auditorium Chair(s): Derek Dreyer MPI-SWS

10:30 25m Talk		Intersection Type Calculi of Bounded Dimension POPL Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
10:55 25m Talk		Type Soundness Proofs with Definitional Interpreters POPL Nada Amin EPFL, Tiark Rompf Purdue University
11:20 25m Talk		Computational Higher-Dimensional Type Theory POPL Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno
11:45 25m Talk		Type Systems as Macros POPL Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University

14:20 - 16:00	Gradual Typing and ContractsPOPL at Auditorium Chair(s): Ronald Garcia University of British Columbia

14:20 25m Talk		Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL Michael Vitousek , Cameron Swords Indiana University, Jeremy G. Siek Indiana University Bloomington
14:45 25m Talk		Gradual Refinement Types POPL Nicolás Lehmann , Éric Tanter University of Chile, Chile Link to publication DOI Pre-print
15:10 25m Talk		Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL Matteo Cimini Indiana University, USA, Jeremy G. Siek Indiana University Bloomington
15:35 25m Talk		Sums of Uncertainty: Refinements go gradual POPL Khurram A. Jafery University of British Columbia, Jana Dunfield University of British Columbia

16:30 - 17:45	Security and PrivacyPOPL at Auditorium Chair(s): Cătălin Hriţcu Inria Paris

16:30 25m Talk		LMS-Verify: Abstraction Without Regret for Verified Systems Programming POPL Nada Amin EPFL, Tiark Rompf Purdue University
16:55 25m Talk		Hypercollecting Semantics and its Application to Static Analysis of Information Flow POPL Mounir Assaf Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Julien Signoles CEA LIST, Éric Totel CentraleSupélec, Frédéric Tronel CentraleSupélec
17:20 25m Talk		LightDP: Towards Automating Differential Privacy Proofs POPL Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00	Opening SessionCoqPL at Auditorium Chair(s): Emilio Jesús Gallego Arias MINES ParisTech

09:00 60m Talk		Invited Talk -- Demonstration of the Iris separation logic in Coq CoqPL I: Robbert Krebbers Delft University of Technology, Netherlands

10:30 - 12:10	Morning SessionCoqPL at Auditorium Chair(s): Alan Schmitt Inria

10:30 25m Talk		IxFree: Step-Indexed Logical Relations in Coq CoqPL Piotr Polesiuk File Attached
10:55 25m Talk		Logical Relations in Iris CoqPL Amin Timany imec - Distrinet, KU Leuven, Robbert Krebbers Delft University of Technology, Netherlands, Lars Birkedal Aarhus University File Attached
11:20 25m Talk		Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting CoqPL Edwin Westbrook Galois, Inc., Gregory Malecha UCSD File Attached
11:45 25m Talk		ppsimpl: a reflexive Coq tactic for canonising goals CoqPL Frédéric Besson File Attached

14:00 - 15:30	Midday SessionCoqPL at Auditorium Chair(s): Sandrine Blazy University of Rennes 1, France

14:00 60m Talk		Invited Talk -- Managing Logical and Computational Complexity using Program Transformations CoqPL I: Nicolas Tabareau Inria, France
15:00 30m Demonstration		Session with the Coq Development Team CoqPL Matthieu Sozeau Inria

16:00 - 18:05	Afternoon SessionCoqPL at Auditorium Chair(s): Matthieu Sozeau Inria

16:00 25m Talk		Synthetic topology in HoTT for probabilistic programming CoqPL Florian Faissole , Bas Spitters File Attached
16:25 25m Talk		CertiCoq: A verified compiler for Coq CoqPL Abhishek Anand , Andrew W. Appel Princeton, Greg Morrisett Cornell University, Zoe Paraskevopoulou Princeton University, USA, Randy Pollack Harvard University, Olivier Savary Belanger Princeton University, Matthieu Sozeau Inria, Matthew Weaver Princeton University File Attached
16:50 25m Talk		CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL CoqPL Izumi Asakura Tokyo Institute of Technology, Japan, Hidehiko Masuhara Tokyo Institute of Technology, Tomoyuki Aotani Tokyo Institute of Technology File Attached
17:15 25m Talk		Verification of Implementations of Distributed Systems Under Churn CoqPL Ryan Doenges University of Washington, James R. Wilcox University of Washington, Doug Woos University of Washington, Zachary Tatlock University of Washington, Seattle, Karl Palmskog File Attached
17:40 25m Talk		Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations CoqPL Nicolas Magaud File Attached

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	CPP Invited Talk																		CPP Algorithm and library verification																																										CPP Automated proof and its verification																								CPP Formalized mathematics with numerical computations

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	CPP Invited Talk																		CPP Verified programming tools																																										CPP Homotopy type theory																								CPP Formal verification of programming language foundations

Wed 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	POPL Opening	POPL Invited speaker																	POPL Type Systems 1																																														POPL Concurrency 1																										POPL Compiler Optimisation

Thu 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	POPL ACM and SIGPLAN Awards			POPL Invited speaker															POPL Type Systems 2																																														POPL Functional Programming with Effects																										POPL Logic and Programming										POPL Business meeting

Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	Student Research Competition Student Competition Award	POPL Invited speaker																	POPL Type Systems 3																																														POPL Gradual Typing and Contracts																										POPL Security and Privacy

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	CoqPL Opening Session																		CoqPL Morning Session																																										CoqPL Midday Session																								CoqPL Afternoon Session

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	CPP Porting the HOL Light Analysis Library: Some Lessons 09:00 - 10:00																		CPP Verifying a hash table and its iterators in higher-order separation logic 10:30 - 11:00						CPP A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm 11:00 - 11:30						CPP Formal foundations of 3D geometry for modeling robot manipulators 11:30 - 12:00																														CPP BliStrTune: Hierarchical Invention of Theorem Proving Strategies 14:00 - 14:30						CPP Automatic Cyclic Termination Proofs for Recursive Procedures in Separat ... 14:30 - 15:00						CPP Formalization of Karp-Miller Tree Construction on Petri Nets 15:00 - 15:30												CPP A Coq Formal Proof of the Lax–Milgram theorem 16:00 - 16:30						CPP A Reflexive Tactic for Polynomial Positivity using Numerical Solvers an ... 16:30 - 17:00						CPP Markov Processes in Isabelle/HOL 17:00 - 17:30						CPP Formalising Real Numbers in Homotopy Type Theory 17:30 - 18:00

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	CPP Mechanized verification of preemptive OS kernels 09:00 - 10:00																		CPP Verified compilation of CakeML to multiple machine-code targets 10:30 - 11:00						CPP COMPLX: a verification framework for concurrent imperative programs 11:00 - 11:30						CPP Verifying dynamic race detection 11:30 - 12:00																														CPP The HoTT library: a formalization of homotopy type theory in Coq 14:00 - 14:30						CPP Lifting proof-relevant unification to higher dimensions 14:30 - 15:00						CPP The Next 700 Syntactical models of type theory 15:00 - 15:30												CPP Type-and-scope safe programs and their proofs 16:00 - 16:30						CPP Formally verified differential dynamic logic 16:30 - 17:00						CPP Equivalence of System F and λ2 in Coq based on context morphism lemmas 17:00 - 17:30

Wed 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	POPL Opening 09:00 - 09:05	POPL The Influence of Dependent Types 09:05 - 10:00																	POPL Polymorphism, subtyping and type inference in MLsub 10:30 - 10:55					POPL Java generics are Turing complete 10:55 - 11:20					POPL Hazelnut: A Bidirectionally Typed Structure Editor Calculus 11:20 - 11:45					POPL Modules, Abstraction, and Parametric Polymorphism 11:45 - 12:10																															POPL A Promising Semantics for Relaxed-Memory Concurrency 14:20 - 14:45					POPL Automatically Comparing Memory Consistency Models 14:45 - 15:10					POPL Interactive Proofs in Higher-Order Concurrent Separation Logic 15:10 - 15:35					POPL A Relational Model of Types-and-Effects in Higher-Order Concurrent Sepa ... 15:35 - 16:00											POPL A Program Optimization for Automatic Database Result Caching 16:30 - 16:55					POPL Stream Fusion, to Completeness 16:55 - 17:20					POPL Rigorous Floating-point Mixed Precision Tuning 17:20 - 17:45

Thu 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	POPL Turing Award Video 09:00 - 09:05	POPL Most Influential Paper Award 09:05 - 09:10	POPL Reynolds Doctoral Dissertation Award 09:10 - 09:15	POPL 40 Years of Abstract Interpretation — An Interview with Patrick Cousot 09:15 - 10:00															POPL Deciding equivalence with sums and the empty type 10:30 - 10:55					POPL The exp-log normal form of types: Decomposing extensional equality and ... 10:55 - 11:20					POPL Contextual isomorphisms 11:20 - 11:45					POPL Typed Self-Evaluation via Intensional Type Functions 11:45 - 12:10																															POPL Type Directed Compilation of Row-Typed Algebraic Effects 14:20 - 14:45					POPL Do be do be do 14:45 - 15:10					POPL Dijkstra Monads for Free 15:10 - 15:35					POPL Stateful Manifest Contracts 15:35 - 16:00											POPL Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks 16:30 - 16:55					POPL LOIS: syntax and semantics 16:55 - 17:20					POPL PC Chair report 17:20 - 17:40				POPL POPL 2018 presentation 17:40 - 17:50		POPL SIGPLAN business meeting 17:50 - 18:20

Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	POPL Student Research Competition Student Competition Award 09:00 - 09:05	POPL Rust: from POPL to practice 09:05 - 10:00																	POPL Intersection Type Calculi of Bounded Dimension 10:30 - 10:55					POPL Type Soundness Proofs with Definitional Interpreters 10:55 - 11:20					POPL Computational Higher-Dimensional Type Theory 11:20 - 11:45					POPL Type Systems as Macros 11:45 - 12:10																															POPL Big Types in Little Runtime: Open World Soundness and Collaborative Bla ... 14:20 - 14:45					POPL Gradual Refinement Types 14:45 - 15:10					POPL Automatically Generating the Dynamic Semantics of Gradually Typed Languages 15:10 - 15:35					POPL Sums of Uncertainty: Refinements go gradual 15:35 - 16:00											POPL LMS-Verify: Abstraction Without Regret for Verified Systems Programming 16:30 - 16:55					POPL Hypercollecting Semantics and its Application to Static Analysis of Inf ... 16:55 - 17:20					POPL LightDP: Towards Automating Differential Privacy Proofs 17:20 - 17:45

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Auditorium	CoqPL Invited Talk -- Demonstration of the Iris separation logic in Coq 09:00 - 10:00																		CoqPL IxFree: Step-Indexed Logical Relations in Coq 10:30 - 10:55					CoqPL Logical Relations in Iris 10:55 - 11:20					CoqPL Predicate Monads: A Framework for Proving Generic Properties of Monadic ... 11:20 - 11:45					CoqPL ppsimpl: a reflexive Coq tactic for canonising goals 11:45 - 12:10																											CoqPL Invited Talk -- Managing Logical and Computational Complexity using Pro ... 14:00 - 15:00												CoqPL Session with the Coq Development Team 15:00 - 15:30												CoqPL Synthetic topology in HoTT for probabilistic programming 16:00 - 16:25					CoqPL CertiCoq: A verified compiler for Coq 16:25 - 16:50					CoqPL CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL 16:50 - 17:15					CoqPL Verification of Implementations of Distributed Systems Under Churn 17:15 - 17:40					CoqPL Transferring Arithmetic Decision Procedures (on Z) to Alternative Repre ... 17:40 - 18:05

Room information: Auditorium

Program Display Configuration

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

POPL

POPL

POPL

POPL

POPL

Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

POPL

POPL

POPL

POPL

POPL

POPL

Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Student Research Competition

POPL

POPL

POPL

POPL

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CoqPL

CoqPL

CoqPL

CoqPL

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change