Program - POPL 2020

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT-06:00) Saskatchewan, Central America.

Use conference time zone: (GMT-06:00) Saskatchewan, Central AmericaSelect 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

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America 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
Break					POPL Catering Break 10:00 - 10:30
Lunch Room																	POPL Catering Lunch 12:30 - 14:00
Maurepas	PLanQC Invited Talk: Quantum Computing for Programming Languages Researchers 09:00 - 09:30		PLanQC Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper 09:30 - 10:00				PLanQC Invited Talk: Q# - Going Beyond Quantum Circuits 10:30 - 11:00		PLanQC Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions 11:00 - 11:30		PLanQC Tuning up entanglement through the cloud using Qiskit-OpenPulse 11:30 - 11:50		PLanQC Tracking Errors through Types in Quantum Programs 11:50 - 12:10		PLanQC Quantum CPOs 12:10 - 12:30								PLanQC Runtime Analysis of Quantum Programs: A Formal Approach 14:00 - 14:20		PLanQC Qbricks: formal verification in quantum computing 14:20 - 14:40		PLanQC Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Trans ... 14:40 - 15:05					PLanQC Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation 15:35 - 15:55		PLanQC Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices 15:55 - 16:15			PLanQC Quingo: A Domain Specific Language for Quantum Computing with NISQ Features 16:15 - 16:35				PLanQC Extending Modern C++ for Heterogeneous Quantum-Classical Computing 16:50 - 17:10		PLanQC Formalization of a Programming Language for Quantum Circuits with Measu ... 17:10 - 17:30		PLanQC Automated distribution of quantum circuits via hypergraph partitioning 17:30 - 17:50
St Jerome	VMCAI The Siren Song of Temporal Synthesis 09:00 - 10:00						VMCAI Witnessing Secure Compilation 10:30 - 11:00		VMCAI BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analy ... 11:00 - 11:30		VMCAI Mini Break 11:30 - 12:00			VMCAI Fixing Code That Explodes Under Symbolic Evaluation 12:00 - 12:30									VMCAI Safety and Robustness for Deep Learning with Provable Guarantees 14:00 - 15:05									VMCAI The Correctness of a Code Generator for a Functional Language 15:35 - 16:07				VMCAI Leveraging Compiler Intermediate Representation for Multi- and Cross-La ... 16:07 - 16:40			VMCAI Mini Break 16:40 - 17:12				VMCAI Putting the Squeeze on Array Programs: Loop Verification via Inductive ... 17:12 - 17:45

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change


Room	8:00	15	30	45	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
Babylon					POPL TutorialFest [T6] Verifying Probabilistic Properties with Couplings 09:00 - 10:00								POPL TutorialFest [T6] Verifying Probabilistic Properties with Couplings 10:30 - 12:30
Bacchus			PADL Opening 08:30 - 08:45	PADL Invited Talk: Logical Engines for Cloud Configurations 08:45 - 09:35					PADL Interactive Text Graph Mining with a Prolog-based Dialog Engine 09:35 - 10:00				PADL AQuA: ASP-based Visual Question Answering 10:30 - 10:55			PADL Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report 10:55 - 11:10			PADL VRASP: A Virtual Reality Environment for Learning Answer Set Programming 11:10 - 11:25		PADL Panel: Programming with logic for the masses 11:25 - 12:00											PADL On the Effects of Integrating Region-based Memory Managemen and Generat ... 13:30 - 13:55		PADL RTMLton: An SML Runtime for Real-Time Systems 13:55 - 14:20			PADL A Timed IO Monad 14:20 - 14:45		PADL Panel: Memory and real-time programming in practice 14:45 - 15:00			PADL Flexible Graph Matching and Graph Edit Distance Using Answer Set Progra ... 15:30 - 15:55			PADL On Repairing Web Services Workflows 15:55 - 16:20					PADL Competitive Programming with PiCat 16:20 - 17:00
Conde					ADSL Relational reasoning using concurrent separation logic 09:00 - 10:00								ADSL Extending the Profile Abstraction for Complete Entailment Checking of S ... 10:30 - 11:00				ADSL Steel: scaling up memory reasoning for F* 11:00 - 11:30					ADSL Strong-Separation Logic 11:30 - 12:00		ADSL The Lower Bound of Decidable Entailments in Separation Logic with Induc ... 12:00 - 12:30											ADSL SLEdge: Bounded Model Checking in Separation Logic 14:00 - 15:05								ADSL Programs Synthesis with Separation Logic 15:35 - 16:40										ADSL Local Reasoning for Global Graph Properties 16:40 - 17:45
Endymion					POPL TutorialFest [T2] Verified Quantum Computing 09:00 - 10:00								POPL TutorialFest [T2] Verified Quantum Computing 10:30 - 12:30																						POPL TutorialFest [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak ... 14:00 - 15:05								POPL TutorialFest [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak ... 15:35 - 17:35
Frontenac					PEPM Opening 09:00 - 09:05	PEPM Network Verification: Past, Present, and Future 09:05 - 10:00							PEPM Dependently-Typed Multi-Stage Programming Revisited (invited talk) 10:30 - 11:05					PEPM High-Fidelity Metaprogramming with Separator Syntax Trees 11:05 - 11:30				PEPM Mini Break 1 11:30 - 11:45	PEPM Module Generation without Regret 11:45 - 12:10			PEPM GOOL: A Generic Object-Oriented Language 12:10 - 12:30									PEPM Reasoning about Progress of Concurrent Objects 14:00 - 15:00								PEPM Frex: Free extensions for normalisation by evaluation (invited talk) 15:35 - 16:10					PEPM Symbolic Bisimulation for Open and Parameterized System 16:10 - 16:35				PEPM Mini Break 2 16:35 - 16:50			PEPM Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited ... 16:50 - 17:25				PEPM An approach to generating text-based IDEs with syntax completion from s ... 17:25 - 17:45
Lunch Room																												POPL Catering Lunch 12:30 - 14:00
Maurepas					CPP Invited talk: Matching Logic: The Foundation of the K Framework 09:00 - 10:00								CPP A Verified Packrat Parser Interpreter for Parsing Expression Grammars 10:30 - 10:51		CPP Proof Pearl: Braun Trees 10:51 - 11:13					CPP FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq 11:13 - 11:35			CPP Verifying x86 Instruction Implementations 11:45 - 12:07		CPP Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs 12:07 - 12:30										CPP An Equational Theory for Weak Bisimulation via Generalized Parameterize ... 14:00 - 14:21		CPP Exploration of Neural Machine Translation in Autoformalization of Mathe ... 14:21 - 14:43		CPP REPLICA: REPL Instrumentation for Coq Analysis 14:43 - 15:05				CPP Verified Programming of Turing Machines in Coq 15:35 - 15:56		CPP A Functional Proof Pearl: Inverting the Ackermann Hierarchy 15:56 - 16:18					CPP Undecidability of Higher-Order Unification Formalised in Coq 16:18 - 16:40					CPP Cubical Synthetic Homotopy Theory 16:50 - 17:12		CPP Three equivalent ordinal notation systems in Cubical Agda 17:12 - 17:34				CPP PC Chairs' report 17:34 - 17:56
Muses					POPL TutorialFest [T1] Building Program Reasoning Tools using LLVM and Z3 09:00 - 10:00								POPL TutorialFest [T1] Building Program Reasoning Tools using LLVM and Z3 10:30 - 12:30																						POPL TutorialFest [T4] Proving Semantic Type Soundness in Iris 14:00 - 15:05								POPL TutorialFest [T4] Proving Semantic Type Soundness in Iris 15:35 - 17:35
SHANGRI-LA					POPL TutorialFest [T3] Synthesizing Programs from Types 09:00 - 10:00								POPL TutorialFest [T3] Synthesizing Programs from Types 10:30 - 12:30																						POPL TutorialFest [T7] Programming and Reasoning with Kleene Algebra with Tests 14:00 - 15:05								POPL TutorialFest [T7] Programming and Reasoning with Kleene Algebra with Tests 15:35 - 17:35
St Jerome					VMCAI Model Checking for Safe Autonomy 09:00 - 10:00								VMCAI A Systematic Approach to Abstract Interpretation of Program Transformations 10:30 - 11:00				VMCAI Sharing Ghost Variables in a Collection of Abstract Domains 11:00 - 11:30					VMCAI Mini Break 11:30 - 12:00		VMCAI Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Mani ... 12:00 - 12:30											VMCAI Synthesizing Environment Invariants for Modular Hardware Verification 14:00 - 14:32			VMCAI Systematic Classification of Attackers via Bounded Model Checking 14:32 - 15:05					VMCAI Cheap CTL Compassion in NuSMV 15:35 - 16:07				VMCAI A Cooperative Parallelization Approach for Property-Directed k-Induction 16:07 - 16:40						VMCAI Mini Break 16:40 - 17:12				VMCAI Generalized Property-Directed Reachability for Hybrid Systems 17:12 - 17:45

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change


Room	8:00	15	30	45	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
Bacchus			PADL Invited Talk: Symbolic Reasoning About Machine Learning Systems 08:30 - 09:20					PADL Exploiting Database Systems and Treewidth for Counting 09:20 - 09:45		PADL Whitebox Induction of Default Rules Using High-Utility Itemset Mining 09:45 - 10:00			PADL Explanations for Dynamic Programming 10:30 - 10:55			PADL A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams 10:55 - 11:20				PADL Variability-aware Datalog 11:20 - 11:35		PADL Panel: Reasoning for machine learning at large 11:35 - 12:00										PADL Invited Talk: Relational Artificial Intelligence 13:30 - 14:00		PADL Invited Talk: Learning Interpretable Rules from Structured Data 14:00 - 14:30			PADL Invited Talk: An Introduction to the Imandra Automated Reasoning System 14:30 - 15:00					PADL Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types 15:30 - 16:00					PADL Panel: Experience and Direction 16:00 - 16:45							PADL Closing 16:45 - 17:00
Frontenac													POPL Ally Skills SessionMentoring Event Ally Skills Session 10:30 - 12:30																														POPL mark 15 Year Retrospective Panel POPLmark 15 Year Retrospective Panel 15:35 - 17:35
Ile de France III (IDF III)					PLMW Opening 09:00 - 09:10	PLMWMentoring Event How to Write Papers So People Can Read Them 09:10 - 10:00							PLMWMentoring Event Making Progress Under Uncertainty in SMT Solving, Research, and Life 10:30 - 11:10					PLMWMentoring Event Research as a collaborative effort 11:10 - 11:50						PLMWMentoring Event Theorem provers are a P.L. researcher's best friend 11:50 - 12:30										PLMWMentoring Event Panel 14:00 - 15:05										PLMWMentoring Event How Can I Academia When My Brain Can't Even? Mental Health in Grad Scho ... 15:40 - 16:40									PLMW Mini break 16:40 - 16:50		PLMWMentoring Event Automated Program Verification using Abductive Reasoning 16:50 - 17:35
Lunch Room																												POPL Catering Lunch 12:30 - 14:00
Maurepas					CPP Invited talk: Proof Assistants at the Hardware-Software Interface 09:00 - 10:00								CPP Coq à la Carte - A Practical Approach to Modular Syntax with Binders 10:30 - 10:51		CPP A Mechanized Formalization of GraphQL 10:51 - 11:13				CPP ConCert: A Smart Contract Certification Framework in Coq 11:13 - 11:35				CPP Formalising Oblivious Transfer in the Semi-Honest and Malicious Model i ... 11:45 - 12:07			CPP Verified Security of BLT Signature Scheme 12:07 - 12:30								CPP Formalizing Determinacy of Concurrent Revisions 14:00 - 14:21		CPP Formalizing π-calculus in Guarded Cubical Agda 14:21 - 14:43		CPP Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed ... 14:43 - 15:05					CPP Formalising perfectoid spaces 15:35 - 15:56			CPP A Constructive Formalization of the Weak Perfect Graph Theorem 15:56 - 16:18				CPP Completeness of an Axiomatization of Graph Isomorphism via Graph Rewrit ... 16:18 - 16:40					CPP The Poincaré-Bendixson Theorem in Isabelle/HOL 16:50 - 17:12			CPP A Formal Proof of the Independence of the Continuum Hypothesis 17:12 - 17:34			CPP The Lean mathematical library 17:34 - 17:56
Orpheus					HASE Opening Plenary 09:00 - 09:10	HASE Interactive Knowledge Shares 09:10 - 10:10							HASE Working Sessions I 10:30 - 12:30																			HASE Peer Skillshare 13:30 - 14:15					HASE Working Sessions II 14:30 - 16:30														HASE Closing Plenary 16:30 - 17:45
St Claude					LAFI Invited talk: Nonstandard Interpretation in Pyro 09:00 - 10:00								LAFI A Differential-form Pullback Programming Language for Higher-order Reve ... 10:30 - 11:00				LAFI A Monad for Point Processes 11:00 - 11:30				LAFI Denotational Semantics for Differentiable Programming with Manifolds 11:30 - 12:00				LAFI Backpropagation in the Simply Typed Lambda-calculus with Linear Negation 12:00 - 12:30									LAFI Divide, Conquer, and Combine: a New Inference Strategy for Probabilisti ... 14:00 - 14:30			LAFI MetaPPL: Inference Algorithms as First-Class Generative Models 14:32 - 14:47		LAFI Monte Carlo Semantic Differencing of Probabilistic Programs 14:49 - 15:05				LAFI Coinductive Trees for Exact Inference of Probabilistic Programs 15:35 - 16:05					LAFI Name generation and Higher-order Probabilistic Programming (Or is new=rnd?) 16:05 - 16:35				LAFI Density Functions of Statistical Probabilistic Programs 16:35 - 17:05					LAFI Probabilistic Programming around Gaussian Processes 17:05 - 17:35				LAFI Closing 17:35 - 17:45
St Jerome					VMCAI How to Win First-Order Safety Games 09:00 - 09:30				VMCAI Improving Parity Game Solvers with Justifications 09:30 - 10:00				VMCAI Language Inclusion for Finite Prime Event Structures 10:30 - 11:00				VMCAI Promptness and Bounded Fairness in Concurrent and Parameterized Systems 11:00 - 11:30				VMCAI Mini Break 11:30 - 12:00				VMCAI Solving LIA* Using Approximations 12:00 - 12:30									VMCAI Formalizing and Checking Multilevel Consistency 14:00 - 14:32			VMCAI Practical Abstractions for Automated Verification of Shared-Memory Conc ... 14:32 - 15:05						VMCAI Panel "The Future of Software Verification" at VMCAI 15:35 - 17:45

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change


Room	7:00	15	30	45	8:00	15	30	45	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
Breakfast Room				POPL Mentoring BreakfastsMentoring Event Mentoring Breakfast 07:45 - 08:45
Endymion																									POPL LGBTQ LunchMentoring Event LGBTQ Lunch 12:30 - 14:00
Ile de France II (IDF II)								POPL Research Papers Welcome + SIGPLAN Award Ceremony 08:45 - 09:00	POPL Research PapersInvited Talk Can Programming Languages Research impact Deep Learning 2.0? 09:00 - 10:00						POPL Research Papers Towards Verified Stochastic Variational Inference for Probabilistic Pro ... 10:30 - 10:51		POPL Research Papers Trace Types and Denotational Semantics for Sound Programmable Inference ... 10:51 - 11:13		POPL Research Papers Semantics of Higher-Order Probabilistic Programs with Conditioning 11:13 - 11:35		POPL Research Papers Recurrence Extraction for Functional Programs through Call-by-Push-Value 11:45 - 12:07		POPL Research Papers Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell 12:07 - 12:30									POPL Research Papers The Future is Ours: Prophecy Variables in Separation Logic 14:00 - 14:21		POPL Research Papers Spy Game: Verifying a Local Generic Solver in Iris 14:21 - 14:43		POPL Research Papers Actris: Session-Type Based Reasoning in Separation Logic 14:43 - 15:05				POPL Research Papers A Simple Differentiable Programming Language 15:35 - 15:56		POPL Research Papers Backpropagation in the Simply Typed Lambda-calculus with Linear Negation 15:56 - 16:18			POPL Research PapersDistinguished Paper Guarded Kleene Algebra with Tests: Verification of Uninterpreted Progra ... 16:18 - 16:40			POPL Research Papers Visualization by Example 16:50 - 17:12		POPL Research Papers Deciding Memory Safety for Single-Pass Heap-Manipulating Programs 17:12 - 17:35
Ile de France III (IDF III)															POPL Research Papers The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space 10:30 - 10:51		POPL Research Papers Complexity and Information in Invariant Inference 10:51 - 11:13		POPL Research Papers Parameterized Verification under TSO is PSPACE-Complete 11:13 - 11:35		POPL Research Papers Program Synthesis by Type-Guided Abstraction Refinement 11:45 - 12:07		POPL Research Papers Synthesizing Replacement Classes 12:07 - 12:30									POPL Research Papers What is Decidable about Gradual Types? 14:00 - 14:21		POPL Research Papers Graduality and Parametricity: Together Again for the First Time 14:21 - 14:43		POPL Research Papers Does Blame Shifting Work? 14:43 - 15:05				POPL Research Papers Persistency Semantics of the Intel-x86 Architecture 15:35 - 15:56		POPL Research Papers Reductions for Safety Proofs 15:56 - 16:18			POPL Research Papers RustBelt Meets Relaxed Memory 16:18 - 16:40
Lunch Room																									POPL Catering Lunch 12:30 - 14:00
SRC																									POPL Student Research Competition SRC Poster Session 16:50 - 19:00
Social Hour																									POPL Research Papers Social Hour (Supported by Facebook) 17:35 - 18:35

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change


Room	7:00	15	30	45	8:00	15	30	45	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
Breakfast Room				POPL Mentoring BreakfastsMentoring Event Mentoring Breakfast 07:45 - 09:00
Ile de France II (IDF II)									POPL Research PapersInvited Talk What is a Secure Programming Language? 09:00 - 10:00						POPL Research Papers Binders by Day, Labels by Night: Effect Instances via Lexically Scoped ... 10:30 - 10:51		POPL Research Papers The Fire Triangle: How to Mix Substitution, Dependent Elimination, and ... 10:51 - 11:13		POPL Research Papers SyTeCi: Automating Contextual Equivalence for Higher-Order Programs wit ... 11:13 - 11:35		POPL Research Papers Fast, Sound, and Effectively Complete Dynamic Race Prediction 11:45 - 12:07		POPL Research Papers Detecting Floating-Point Errors via Atomic Conditions 12:07 - 12:30									POPL Research PapersDistinguished Paper Undecidability of D<: and Its Decidable Fragments 14:00 - 14:21		POPL Research Papers Decidable Subtyping for Path Dependent Types 14:21 - 14:43		POPL Research Papers Dependent Type Systems as Macros 14:43 - 15:05				POPL Research Papers Deductive Verification with Ghost Monitors 15:35 - 15:56		POPL Research Papers The Next 700 Relational Program Logics 15:56 - 16:18			POPL Research Papers Incorrectness Logic 16:18 - 16:40			POPL Research Papers Business Meeting & SRC Awards 16:50 - 18:00
Ile de France III (IDF III)															POPL Research Papers Synthesis of Coordination Programs from Linear Temporal Specifications 10:30 - 10:51		POPL Research Papers Augmented Example-based Synthesis using Relational Perturbation Properties 10:51 - 11:13		POPL Research Papers Provenance-Guided Synthesis of Datalog Programs 11:13 - 11:35		POPL Research PapersDistinguished Paper Seminaïve Evaluation for a Higher-Order Functional Language 11:45 - 12:07		POPL Research Papers Decomposition Diversity with Symmetric Data and Codata 12:07 - 12:30									POPL Research Papers Abstract Extensionality: On the Properties of Incomplete Abstract Inter ... 14:00 - 14:21		POPL Research Papers Abstract Interpretation of Distributed Network Control Planes 14:21 - 14:43		POPL Research Papers Deterministic Parallel Fixpoint Computation 14:43 - 15:05				POPL Research Papers A Language for Probabilistically Oblivious Computation 15:35 - 15:56		POPL Research Papers PλωNK: Functional Probabilistic NetKAT 15:56 - 16:18			POPL Research Papers Optimal Approximate Sampling From Discrete Probability Distributions 16:18 - 16:40
Lunch Room																									POPL Catering Lunch 12:30 - 14:00
Palace Cafe																									POPL W@POPL DinnerMentoring Event W@POPL Dinner 19:00 - 21:00
Social Hour																									POPL Research Papers Social Hour (Supported by Microsoft) 18:00 - 19:00
St Jerome																									POPL Student Research Competition SRC Finalists Presentations 14:00 - 15:30

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change


Room	7:00	15	30	45	8:00	15	30	45	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
Breakfast Room				POPL Mentoring BreakfastsMentoring Event Mentoring Breakfast 07:45 - 09:00
Ile de France II (IDF II)									POPL Research PapersInvited Talk Probabilistic Programming 09:00 - 10:00						POPL Research PapersDistinguished Paper Kind Inference for Datatypes 10:30 - 10:51		POPL Research Papers Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc 10:51 - 11:13		POPL Research Papers Pointer Life Cycle Types for Lock-Free Data Structures with Memory Recl ... 11:13 - 11:35		POPL Research Papers Label-Dependent Session Types 11:45 - 12:07		POPL Research Papers Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Fu ... 12:07 - 12:30									POPL Research Papers Full Abstraction for the Quantum Lambda-Calculus 14:00 - 14:21		POPL Research Papers Relational Proofs for Quantum Programs 14:21 - 14:43		POPL Research Papers A Probabilistic Separation Logic 14:43 - 15:05				POPL Research PapersDistinguished Paper Taylor Subsumes Scott, Berry, Kahn and Plotkin 15:35 - 15:56		POPL Research Papers Reduction Monads and Their Signatures 15:56 - 16:18			POPL Research Papers Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq 16:18 - 16:40
Ile de France III (IDF III)															POPL Research Papers Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedul ... 10:30 - 10:51		POPL Research Papers The High-Level Benefits of Low-Level Sandboxing 10:51 - 11:13		POPL Research PapersDistinguished Paper Interaction Trees: Representing Recursive and Impure Programs in Coq 11:13 - 11:35		POPL Research Papers Proving Expected Sensitivity of Probabilistic Programs with Randomized ... 11:45 - 12:07		POPL Research Papers Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Progr ... 12:07 - 12:30									POPL Research Papers Stacked Borrows: An Aliasing Model for Rust 14:00 - 14:21		POPL Research Papers Executable Formal Semantics for the POSIX Shell 14:21 - 14:43		POPL Research Papers Disentanglement in Nested-Parallel Programs 14:43 - 15:05				POPL Research Papers Formal Verification of a Constant-Time Preserving C Compiler 15:35 - 15:56		POPL Research Papers CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Ver ... 15:56 - 16:18			POPL Research Papers Mechanized Semantics and Verified Compilation for a Dataflow Synchronou ... 16:18 - 16:40
Lunch Room																									POPL Catering Lunch 12:30 - 14:00
Social Hour																									POPL Research Papers Social Hour (Supported by Tezos) 16:40 - 17:40

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America 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
Lunch Room																				POPL Catering Lunch 12:30 - 14:00
Maurepas	CoqPL SMTCoq: Safe and efficient automation in Coq (Keynote) 09:00 - 10:00							CoqPL Deriving Instances with Dependent Types 10:30 - 11:00			CoqPL The use of Coq for Common Criteria Evaluations 11:00 - 11:30			CoqPL Verifying concurrent Go code in Coq with Goose 11:30 - 12:00			CoqPL A Tutorial on Equations 12:00 - 12:30									CoqPL Autosubst 2: Mechanising binders in Coq (Keynote) 14:00 - 15:00										CoqPL Towards Formally Verified Just-in-Time compilation 15:35 - 16:05			CoqPL A Coq Library of Undecidable Problems 16:05 - 16:35				CoqPL Short break 16:35 - 16:50			CoqPL Session with the Coq Development Team 16:50 - 17:35
Orleans	WGT Gradual Typing as if Types Mattered 09:00 - 09:30			WGT Fully Abstract from Static to Gradual 09:30 - 10:00				WGT Gradual Algebraic Data Types 10:30 - 11:00			WGT Gradual Typing for Extensibility by Rows 11:00 - 11:30			WGT Foreign Function Typing: Semantic Type Soundness for FFIs 11:30 - 12:00			WGT Space-Efficient Monotonic References 12:00 - 12:30									WGT Hypercoercions and a Framework for Equivalence of Cast Calculi 14:00 - 14:32			WGT Space-Efficient Gradual Typing in Coercion-Passing Style 14:32 - 15:05							WGT Gradual Verification of Recursive Heap Data Structures 15:35 - 16:07			WGT Gradual Program Analysis 16:07 - 16:40					WGT Minibreak 16:40 - 16:50		WGT Blame tracking at higher fidelity 16:50 - 17:20				WGT Discussion on gradual typing and WGT21 17:20 - 17:45
Rosalie	PriSC PriSC Introduction 09:00 - 09:05	PriSC Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing 09:05 - 10:00						PriSC Exorcising Spectres with Secure Compilers 10:30 - 10:54		PriSC Trace-Relating Compiler Correctness and Secure Compilation 10:54 - 11:18			PriSC Reconciling progress-insensitive noninterference and declassification 11:18 - 11:42		PriSC Hermes: Implementing Cryptography without Side-channels 11:42 - 12:06			PriSC A CompCert Compiler that Preserves Cryptographic Constant-time 12:06 - 12:30								PriSC Exploits as Insecure Compilation 14:00 - 14:24		PriSC Universal Composability is Secure Compilation 14:24 - 14:48			PriSC Short Talk: Automatically Eliminating Speculative Leaks With Blade 14:48 - 14:56	PriSC Short Talk: Everparse 14:56 - 15:04				PriSC Flexible Tag-based Policies for Compartmentalized C 15:35 - 15:59		PriSC Mechanized Reasoning about a Capability Machine 15:59 - 16:23			PriSC Securing Interruptible Enclaves 16:23 - 16:47				PriSC Mini-break 16:47 - 16:57		PriSC WebAssembly as an Intermediate Language for Provably-Safe Software Sand ... 16:57 - 17:21			PriSC Memory Safety Preservation for WebAssembly 17:21 - 17:45

POPL 2020 Program

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

POPL 2020 Program

Switch Program View

Program Display Configuration

Sun 19 JanDisplayed time zone: Saskatchewan, Central America change

Mon 20 JanDisplayed time zone: Saskatchewan, Central America change

Tue 21 JanDisplayed time zone: Saskatchewan, Central America change

Wed 22 JanDisplayed time zone: Saskatchewan, Central America change

Thu 23 JanDisplayed time zone: Saskatchewan, Central America change

Fri 24 JanDisplayed time zone: Saskatchewan, Central America change

Sat 25 JanDisplayed time zone: Saskatchewan, Central America change

Get Calendar (iCal)

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change