Program - POPL 2023

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select 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 15 Jan
Displayed time zone: Eastern Time (US & Canada) 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
Kenmore	ProLaLa Opening comments 09:00 - 09:10		ProLaLa Academic keynote : A Logician and Lawyer walk into a Classroom 09:10 - 09:55				ProLaLa Formal Modeling and Analysis of Legal Contracts using ContractCheck 09:55 - 10:20				ProLaLa What do Relational Properties Have to Say About Legal Expert Systems ? 10:20 - 10:30			ProLaLaVirtual Building Information Modeling Using Constraint Logic Programming (Exten ... 11:00 - 11:25			ProLaLa Exploring Consequences of Privacy Policies with Narrative Generation vi ... 11:25 - 11:50			ProLaLaVirtual The Structure and Legal Interpretation of Computer Programs 11:50 - 12:15				ProLaLa Deontic Paradoxes in Library Lending Regulations: A Case Study in Flint 12:15 - 12:25		ProLaLaVirtual Defeasible Semantics for L4 12:25 - 12:35							ProLaLa Experience report: implementing a real-world, medium-sized program deri ... 14:00 - 14:25			ProLaLaVirtual Legal Contracts Amending in Stipula 14:25 - 14:50			ProLaLaVirtual Towards an Automatic Consolidation of French Law 14:50 - 15:15				ProLaLa DCR Graphs as Co-created Executable Models of the Law 15:15 - 15:25		ProLaLaVirtual Visual Propositional Logic With yscript 15:25 - 15:35			ProLaLa Research keynote 16:00 - 16:45			ProLaLa Designing an experiment for comparing user interfaces for legal formali ... 16:45 - 17:10		ProLaLaVirtual Blawx: User-friendly Goal-Directed Answer Set Programming for Rules as Code 17:10 - 17:20		ProLaLaVirtual Formalising Criminal Law in Catala 17:20 - 17:30
Scollay	LAFI Opening Comments 09:00 - 09:05	LAFIBoston Introduction to the tensor-programs framework, a PL approach that helps ... 09:05 - 10:05							LAFIParis Exact Inference for Discrete Probabilistic Programs via Generating Func ... 10:10 - 10:20		LAFIBoston Exact Probabilistic Inference Using Generating Functions 10:20 - 10:30			LAFIBoston What do posterior distributions of probabilistic programs look like? 11:00 - 11:20		LAFIBoston Semantics of Probabilistic Program Traces 11:20 - 11:30		LAFIBoston A convenient category of tracing measure kernels 11:30 - 11:40	LAFIParis Random probability distributions as natural transformations 11:45 - 11:50	LAFIParis Static Delayed Sampling for Probabilistic Programming Languages 11:50 - 11:55	LAFIOnline Denotational semantics of languages for inference: semirings, monads, a ... 11:55 - 12:00		LAFIBoston Separated and Shared Effects in Higher-Order Languages 12:10 - 12:15	LAFIBoston On Iteration in Discrete Probabilistic Programming 12:15 - 12:20	LAFIBoston Bit-Blasting Probabilistic Programs 12:20 - 12:25	LAFIBoston πMPC: Automatic Security Proofs for MPC Protocols 12:25 - 12:30							LAFIParis The Variable Elimination Algorithm as a Let-Term Rewriting 14:00 - 14:20		LAFIOnline Contextual source code AD transformations for sum types 14:20 - 14:40			LAFIOnline Pitfalls of Full Bayesian Inference in Universal Probabilistic Programming 14:45 - 14:50	LAFIOnline ∂ is for Dialectica: typing differentiable programming 14:50 - 14:55	LAFIBoston On the Reparameterisation Gradient for Non-Differentiable but Continuou ... 15:00 - 15:05	LAFIBoston Partial Evaluation of Forward-Mode Automatic Differentiation 15:05 - 15:10	LAFIBoston Distribution Theoretic Semantics for Non-Smooth Differentiable Programming 15:10 - 15:15	LAFIBoston New foundations for probabilistic separation logic 15:15 - 15:20	LAFIBoston Verified Reversible Programming for Verified Lossless Compression 15:20 - 15:25	LAFI Towards type-driven data-science in Idris 15:25 - 15:30

Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada) 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
Arlington	VMCAI Towards a Theoretical Understanding of Property-Directed Reachability 09:00 - 10:00				VMCAI Distributing and Parallelizing Non-canonical Loops 10:00 - 10:30					VMCAI Efficient Interprocedural Data-Flow Analysis using Treedepth and Treewidth 11:00 - 11:30			VMCAI Result Invalidation for Incremental Modular Analyses 11:30 - 12:00		VMCAI Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference 12:00 - 12:30									VMCAI What Can Program Analysis Say About Data Bias? 14:00 - 15:00					VMCAI Bayesian parameter estimation with guarantees via interval analysis and ... 15:00 - 15:30					VMCAI Solving Constrained Horn Clauses over Algebraic Data Types 16:00 - 16:30			VMCAI Satisfiability Modulo Custom Theories in Z3 (Tool Paper) 16:30 - 17:00		VMCAI CosySEL: Improving SAT Solving Using Local Symmetries 17:00 - 17:30
Copley	POPL TutorialFest Deductive Verification of Probabilistic Programs 09:00 - 10:30									POPL TutorialFest Deductive Verification of Probabilistic Programs 11:00 - 12:30														POPL TutorialFest Neurosymbolic Programming 14:00 - 15:30										POPL TutorialFest Neurosymbolic Programming 16:00 - 17:30
Kenmore	POPL TutorialFest QuickChick: Combining Random Testing and Verification in Coq 09:00 - 10:30									POPL TutorialFest QuickChick: Combining Random Testing and Verification in Coq 11:00 - 12:30														POPL TutorialFest RUST: Regions, Uniqueness, Ownership & Types 14:00 - 15:30										POPL TutorialFest RUST: Regions, Uniqueness, Ownership & Types 16:00 - 17:30
Park	POPL TutorialFest Isabelle/HOL: Foundations, Induction, and Coinduction 09:00 - 10:30									POPL TutorialFest Isabelle/HOL: Foundations, Induction, and Coinduction 11:00 - 12:30														POPL TutorialFest Using a Proof Assistant to Teach PL Theory, Without the Overhead 14:00 - 15:30										POPL TutorialFest Using a Proof Assistant to Teach PL Theory, Without the Overhead 16:00 - 17:30
Scollay	POPL TutorialFest Z3 Internals – A guide to principles, art and empirics of programming S ... 09:00 - 10:30									POPL TutorialFest Z3 Internals – A guide to principles, art and empirics of programming S ... 11:00 - 12:30														POPL TutorialFest Incorrectness Logic and Under-approximation: Foundations of Bug Catching 14:00 - 15:30										POPL TutorialFest Incorrectness Logic and Under-approximation: Foundations of Bug Catching 16:00 - 17:30
Studio 1	CPP CompCert: a journey through the landscape of mechanized semantics for v ... 09:00 - 10:00					CPP Mechanised Semantics for Gated Static Single Assignment 10:08 - 10:30				CPPdistinguished paper A Formalization of the Development Closedness Criterion for Left-Linear ... 11:00 - 11:22		CPPremote presentation Formalizing and computing propositional quantifiers 11:22 - 11:45		CPPremote presentation Encoding Dependently-Typed Constructions into Simple Type Theory 11:45 - 12:07		CPP A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Co ... 12:07 - 12:30								CPP A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL 14:00 - 14:22		CPP P4Cub: A Little Language for Big Routers 14:22 - 14:45		CPP ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER 14:45 - 15:07		CPP Verifying term graph optimizations using Isabelle/HOL 15:07 - 15:30				CPPremote presentation Formalising the h-principle and sphere eversion 16:00 - 16:22		CPP A Formalized Reduction of Keller's Conjecture 16:22 - 16:44		CPPdistinguished paper Computing Cohomology Rings in Cubical Agda 16:45 - 17:07		CPP short break 17:07 - 17:15	CPP CPP Business Meeting 17:15 - 18:00
The Loft	PADL Towards Declarative Content Generation for Creativity Support Tools 09:00 - 10:00				PADL Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL 10:00 - 10:30					PADL Fluo: A Domain-Specific Language for Experiments in Fluorescence Micros ... 11:00 - 11:30			PADL SwitchLog: A Logic Programming Language for Network Switches 11:30 - 12:00		PADL Formalizing and Reasoning about Contracts between Agents 12:00 - 12:30									PADL Jury-trial Story Construction and Analysis using Goal-directed Answer S ... 14:00 - 14:30			PADL Solving Vehicle Equipment Specification Problems with Answer Set Progra ... 14:30 - 15:00		PADL Pruning Redundancy in Answer Set Optimization Applied to Preventive Mai ... 15:00 - 15:30					PADL Integrating ASP-based incremental reasoning in the videogame developmen ... 16:00 - 16:30			PADL UAV Compliance Checking using Answer Set Programming and Minimal Explan ... 16:30 - 17:00		PADL Flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybri ... 17:00 - 17:30

Tue 17 Jan
Displayed time zone: Eastern Time (US & Canada) 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
Arlington	VMCAI Differential Verification of Deep Neural Networks 09:00 - 10:00				VMCAI ARENA: Enhancing Abstract Refinement for Neural Network Verification 10:00 - 10:30					VMCAIRecorded Maximal Robust Neural Network Specifications via Oracle-guided Numerica ... 11:00 - 11:15	VMCAIRecorded SMT-Based Modeling and Verification of Spiking Neural Networks: A Case ... 11:15 - 11:30		VMCAI A generic framework to coarse-grain stochastic reaction networks by Abs ... 11:30 - 12:00		VMCAI Sound Symbolic Execution via Abstract Interpretation and its Applicatio ... 12:00 - 12:30									VMCAI Verifying, Inferring and Exploiting Code Commutativity 14:00 - 15:00										VMCAIRecorded A Pragmatic Approach to Stateful Partial Order Reduction 16:00 - 16:15	VMCAIRecorded StaticPersist : Compiler Support for PMEM Programming 16:15 - 16:30		VMCAI Compositional Verification of Stigmergic Collective Systems 16:30 - 17:00		VMCAI Synthesizing History and Prophecy Variables for Symbolic Model Checking 17:00 - 17:30
Scollay	PEPM Fast Cryptographic Code via Partial Evaluation 09:00 - 10:00				PEPM Towards Type Debugging using Partial Evaluation 10:00 - 10:30					PEPM Semantic Transformation Framework for Rewriting Rules 11:00 - 11:30			PEPM Symbolic Execution of Hadamard-Toffoli Quantum Circuits 11:30 - 12:00		PEPM Generating Programs for Polynomial Multiplication with Correctness Assu ... 12:00 - 12:30									PEPM MATLAB Coder: Partial Evaluation in Practice 14:00 - 15:00					PEPM Modular Construction of Multi-sorted Free Extensions 15:00 - 15:30					PEPMRemote Efficient Embedding of Strategic Attribute Grammars via Memoization 16:00 - 16:30			PEPMRecorded Towards a Reflection for Effect Handlers 16:30 - 17:00		PEPM Wrap up 17:00 - 17:30
Studio 1	CPP (canceled invited talk) 09:00 - 10:00					CPPdistinguished paper Aesop: White-Box Best-First Proof Search for Lean 10:08 - 10:30				CPPRecorded Presentation Terms for Efficient Proof Checking and Parsing 11:00 - 11:22		CPPremote presentation Compositional pre-processing for automated reasoning in dependent type ... 11:22 - 11:45		CPP Practical and sound equality tests, automatically 11:45 - 12:07		CPPremote presentation Compiling higher-order specifications to SMT solvers: how to deal with ... 12:07 - 12:30								CPPremote presentation FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores 14:00 - 14:22		CPP Formalising Decentralised Exchanges in Coq 14:22 - 14:45		CPP Semantics of Probabilistic Programs using S-Finite Kernels in Coq 14:45 - 15:07		CPP Formalising Sharkovsky's Theorem (Proof Pearl) 15:07 - 15:30				CPPremote presentation A formalization of Doob's martingale convergence theorems in mathlib 16:00 - 16:22		CPP A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL 16:22 - 16:45		CPP A Formal Disproof of Hirsch Conjecture 16:45 - 17:07		CPP Formalized Class Group Computations and Integral Points on Mordell Elli ... 17:07 - 17:30
Studio 2	PLMW @ POPL Introduction 09:00 - 09:15	PLMW @ POPL Imagining the Reader 09:15 - 10:00			PLMW @ POPL Icebreaker Activity 10:00 - 10:30					PLMW @ POPL Session Types Meet Polymorphism and Dependent Types 11:00 - 11:45				PLMW @ POPL Career Trajectories in PL 11:45 - 12:30										PLMW @ POPLremote presentation Anti-disciplinary: doing academic research when you like too many things 14:00 - 14:45				PLMW @ POPL How (not) to give a great research talk 14:45 - 15:30						PLMW @ POPL Big Ideas in Program Synthesis 16:00 - 16:45				PLMW @ POPL Care and Feeding of Advisors 16:45 - 17:30
The Loft	PADL Modern Macros 09:00 - 10:00				PADL Automatic Rollback Suggestions for Incremental Datalog Evaluation 10:00 - 10:30					PADL RICE: An Optimizing Curry Compiler 11:00 - 11:30			PADL Embedding Functional Logic Programming in Haskell via a Compiler Plugin 11:30 - 12:00		PADL Program Synthesis Using Example Propagation 12:00 - 12:30									PADL Execution Time Program Verification With Tight Bounds 14:00 - 14:30			PADL From Starvation Freedom to All-Path Reachability Problems in Constraine ... 14:30 - 15:00		PADL Multiple Query Satisfiability of Constrained Horn Clauses 15:00 - 15:30					PADL Dynamic slicing of Reaction Systems based on assertions and monitors 16:00 - 16:30			PADL Linear Algebraic Abduction with Partial Evaluation 16:30 - 17:00

Wed 18 Jan
Displayed time zone: Eastern Time (US & Canada) 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	18:00		15		30	45	19:00	15	30	45	20:00	15	30	45
Avenue34															POPL Distinguished Paper Higher-Order Leak and Deadlock Free Locks 10:45 - 11:10		POPL Temporal Verification with Answer-Effect Modification: Dependent Tempor ... 11:10 - 11:35			POPL Recursive Subtyping for All 11:35 - 12:00												POPL A High-Level Separation Logic for Heap Space under Garbage Collection 13:30 - 13:55		POPL CN: Verifying Systems C Code with Separation-Logic Refinement Types 13:55 - 14:20			POPL Conditional Contextual Refinement 14:20 - 14:45				POPL MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code 15:10 - 15:35			POPL Reconciling Shannon and Scott with a Lattice of Computable Information 15:35 - 16:00		POPL A Core Calculus for Equational Proofs of Cryptographic Protocols 16:00 - 16:25			POPL Distinguished Paper DimSum: A Decentralized Approach to Multi-language Semantics and Verifi ... 16:45 - 17:10		POPL Formally Verified Native Code Generation in an Effectful JIT: Turning t ... 17:10 - 17:35			POPL Dargent: A Silver Bullet for Verified Data Layout Refinement 17:35 - 18:00
Foyer																															POPL Reception 18:00 - 21:00
Grand Ballroom A							POPL Principles of Persistent Programming 09:10 - 10:15								POPL Kater: Automating Weak Memory Model Metatheory and Consistency Checking 10:45 - 11:10		POPL Virtual Stratified Commutativity in Verification Algorithms for Concurrent Programs 11:10 - 11:35			POPL A Partial Order View of Message-Passing Communication Models 11:35 - 12:00												POPL Witnessability of Undecidable Problems 13:30 - 13:55		POPL On the Expressive Power of String Constraints 13:55 - 14:20			POPL A Robust Theory of Series Parallel Graphs 14:20 - 14:45				POPL Inductive Synthesis of Structurally Recursive Functional Programs from ... 15:10 - 15:35			POPL FlashFill++: Scaling Programming by Example by Cutting to the Chase 15:35 - 16:00		POPL Unrealizability Logic 16:00 - 16:25			POPL Affine Monads and Lazy Structures for Bayesian Programming 16:45 - 17:10		POPL Virtual Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective ... 17:10 - 17:35			POPL Smoothness Analysis for Probabilistic Programs with Application to Opti ... 17:35 - 18:00		POPL Student Research Competition Zydeco: A Stack-Based Call-By-Push-Value Language 18:00 - 19:30 HasChor: Choreographic Programming in Haskell 18:00 - 19:30 Towards Synthesis in Superposition 18:00 - 19:30 A Formalization of Observational Equivalence in Message Passing Protocols 18:00 - 19:30 On the metatheory of IRs and the CPS-calculus 18:00 - 19:30 Scalable Synthesis of Regular Expressions From Only Positive Examples 18:00 - 19:30 Evaluating Soundness of a Gradual Verifier with Property Based Testing 18:00 - 19:30 A mechanized model for logical clocks 18:00 - 19:30 Wisening Assertions: A live Bayesian reasoning system for probabilistic ... 18:00 - 19:30 Synthesizing Vectorized Code via Verified Lifting 18:00 - 19:30 Citrus: A Dependently Typed Framework for Pulse-Based Logic 18:00 - 19:30 Neko: A quantum map-filter-reduce programming language 18:00 - 19:30 Compiling and Running High-level Quantum Programs 18:00 - 19:30 Trace-Guided Inductive Synthesis of Recursive Functional Programs 18:00 - 19:30
White Hill			POPL Session Previews Automated Verification: Session Preview 08:30 - 08:40	POPL Session Previews Types I: Session Preview 08:40 - 08:50									POPL Session Previews Security: Session Preview 10:20 - 10:30	POPL Session Previews Synthesis I: Session Preview 10:30 - 10:40											POPL Session Previews Logic & Decidability I: Session Preview 12:40 - 12:50		POPL Session Previews Program Logics & Resources: Session Preview 12:50 - 13:00	POPL Session Previews Verified Compilation: Session Preview 13:00 - 13:10	POPL Session Previews Probabilistic Inference: Session Preview 13:10 - 13:20																												POPL Session Previews Synthesis II: Session Preview 18:10 - 18:20		POPL Session Previews Semantics I: Session Preview 18:20 - 18:30

Thu 19 Jan
Displayed time zone: Eastern Time (US & Canada) 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	18:00		15		30	45
Avenue34														POPL A Type-Based Approach to Divide-and-Conquer Recursion in Coq 10:20 - 10:45		POPL Virtual Elements of Quantitative Rewriting 10:45 - 11:10		POPL The Geometry of Causality: Multi-token Geometry of Interaction and Its ... 11:10 - 11:35			POPL Deconstructing the Calculus of Relations with Tape Diagrams 11:35 - 12:00									POPL Probabilistic Resource-Aware Session Types 13:30 - 13:55		POPL A Calculus for Amortized Expected Runtimes 13:55 - 14:20			POPL A General Noninterference Policy for Polynomial Time 14:20 - 14:45				POPL Distinguished Paper Admissible Types-to-PERs Relativization in Higher-Order Logic 15:10 - 15:35			POPL An Order-Theoretic Analysis of Universe Polymorphism 15:35 - 16:00		POPL Impredicative Observational Equality 16:00 - 16:25
Grand Ballroom A							POPL Panel: Next 50 Years of POPL 09:00 - 10:00							POPL babble: Learning Better Abstractions with E-Graphs and Anti-unification 10:20 - 10:45		POPL Combining Functional and Automata Synthesis to Discover Causal Reactive ... 10:45 - 11:10		POPL Comparative Synthesis: Learning Near-Optimal Network Designs by Query 11:10 - 11:35			POPL Top-Down Synthesis for Library Learning 11:35 - 12:00									POPL Distinguished Paper SSA Translation Is an Abstract Interpretation 13:30 - 13:55		POPL Distinguished Paper Dynamic Race Detection with O(1) Samples 13:55 - 14:20			POPL Statically Resolvable Ambiguity 14:20 - 14:45				POPL You Only Linearize Once: Tangents Transpose to Gradients 15:10 - 15:35			POPL Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations 15:35 - 16:00		POPL Distinguished Paper ADEV: Sound Automatic Differentiation of Expected Values of Probabilist ... 16:00 - 16:25
White Hill			POPL Session Previews Program Analysis & Parsing: Session Preview 08:20 - 08:30	POPL Session Previews Resource Analysis: Session Preview 08:30 - 08:40	POPL Session Previews Automatic Differentiation: Session Preview 08:40 - 08:50							POPL Session Previews Type Theory: Session Preview 10:05 - 10:15															POPL Session Previews Logic & Decidability II: Session Preview 13:00 - 13:10	POPL Session Previews Types II: Session Preview 13:10 - 13:20		POPL Student Research Competition Scalable Synthesis of Regular Expressions From Only Positive Examples 13:30 - 13:45	POPL Student Research Competition Synthesizing Vectorized Code via Verified Lifting 13:45 - 14:00		POPL Student Research Competition Evaluating Soundness of a Gradual Verifier with Property Based Testing 14:00 - 14:15	POPL Student Research Competition On the metatheory of IRs and the CPS-calculus 14:15 - 14:30		POPL Student Research Competition Wisening Assertions: A live Bayesian reasoning system for probabilistic ... 14:30 - 14:45	POPL Student Research Competition Compiling and Running High-level Quantum Programs 14:45 - 15:00																POPL Session Previews Semantics & Effects: Session Preview 18:10 - 18:20		POPL Session Previews Logic Programming: Session Preview 18:20 - 18:30

Fri 20 Jan
Displayed time zone: Eastern Time (US & Canada) 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
Avenue34						POPL A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data T ... 09:00 - 09:25		POPL Making a Type Difference: Subtraction on Intersection Types as Generali ... 09:25 - 09:50			POPL Quantitative Inhabitation for Different Lambda Calculi in a Unifying Fr ... 09:50 - 10:15					POPL Step-Indexed Logical Relations for Countable Nondeterminism and Probabi ... 10:45 - 11:10		POPL Choice Trees: Representing Nondeterministic, Recursive, and Impure Prog ... 11:10 - 11:35			POPL Recorded Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects 11:35 - 12:00									POPL Tail Recursion Modulo Context: An Equational Approach 13:30 - 13:55		POPL Taking Back Control in an Intermediate Representation for GPU Computing 13:55 - 14:20			POPL Executing Microservice Applications on Serverless, Correctly 14:20 - 14:45				POPL An Operational Approach to Library Abstraction under Relaxed Memory Con ... 15:10 - 15:35			POPL The Path to Durable Linearizability 15:35 - 16:00		POPL A Compositional Theory of Linearizability 16:00 - 16:25			POPL Locally Nameless Sets 16:45 - 17:10		POPL Why Are Proofs Relevant in Proof-Relevant Models? 17:10 - 17:35			POPL Towards a Higher-Order Mathematical Operational Semantics 17:35 - 18:00
Square						POPL When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic 09:00 - 09:25		POPL Higher-Order MSL Horn Constraints 09:25 - 09:50			POPL Fast Coalgebraic Bisimilarity Minimization 09:50 - 10:15					POPL Qunity: A Unified Language for Quantum and Classical Computing 10:45 - 11:10		POPL Virtual Proto-Quipper with Dynamic Lifting 11:10 - 11:35			POPL Virtual CoqQ: Foundational Verification of Quantum Programs 11:35 - 12:00									POPL Distinguished Paper Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification 13:30 - 13:55		POPL Optimal CHC Solving via Termination Proofs 13:55 - 14:20			POPL From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-a ... 14:20 - 14:45				POPL The Fine-Grained Complexity of CFL Reachability 15:10 - 15:35			POPL Single-Source-Single-Target Interleaved-Dyck Reachability via Integer L ... 15:35 - 16:00		POPL Context-Bounded Verification of Context-Free Specifications 16:00 - 16:25			POPL An Algebra of Alignment for Relational Verification 16:45 - 17:10		POPL Grisette: Symbolic Compilation as a Functional Programming Library 17:10 - 17:35			POPL HFL(Z) Validity Checking for Automated Program Verification 17:35 - 18:00
White Hill			POPL Session Previews Formal Methods in Compilation & Implementation: Session Preview 08:30 - 08:40	POPL Session Previews Quantum Computing: Session Preview 08:40 - 08:50										POPL Session Previews Concurrency & Linearizability: Session Preview 10:20 - 10:30	POPL Session Previews Algorithmic Verification 10:30 - 10:40												POPL Session Previews Relational & Automated Verification: Session Preview 13:00 - 13:10	POPL Session Previews Semantics II: Session Preview 13:10 - 13:20

Sat 21 Jan
Displayed time zone: Eastern Time (US & Canada) 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
Park	PriSC Introduction 09:00 - 09:05	PriSC Semantic Intermediate Representations for Sound Language Interoperability 09:05 - 10:05					PriSC Towards End-to-End Verified TEEs via Verified Interface Conformance and ... 10:05 - 10:30				PriSC Automated Learning and Verification of Embedded Security Architectures 11:00 - 11:25		PriSC pi_RA: A pi-calculus for verifying protocols that use remote attestation 11:25 - 11:50			PriSC Robust Constant-Time Cryptography 11:50 - 12:15		PriSC Short Talk: Generalising secure compilation criteria 12:15 - 12:30							PriSC Blame-Preserving Secure Compilation 14:00 - 14:25		PriSCRecorded Securely Compiling F* Programs With IO and Then Linking Them Against We ... 14:25 - 14:50			PriSC SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capa ... 14:50 - 15:15					PriSC Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers 16:00 - 16:25		PriSC FaJITa: Verifying Optimizations on Just-In-Time Programs 16:25 - 16:50			PriSC Universally Composable Security for Program Partitioning 16:50 - 17:15
Scollay	CoqPL Omnisemantics: Smooth Handling of Nondeterminism (Invited talk) 09:00 - 10:00					CoqPL Interactive Theorem Proving in Logic Education：A Coq Formalization of Z ... 10:00 - 10:30					CoqPL Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving C ... 11:00 - 11:30			CoqPL Integrating graphical proofs in Coq 11:30 - 12:00			CoqPL Towards Formally Verified Path ORAM in Coq 12:00 - 12:30								CoqPL Verified Differential Privacy for Finite Computers 14:00 - 14:30			CoqPL Formalizing Monoidal Categories and Actions for Syntax with Binders 14:30 - 15:00			CoqPL Certifying Complexity Analysis 15:00 - 15:30				CoqPL Session with the Coq Development Team 16:00 - 16:45

POPL 2023 Program

Sun 15 Jan
Displayed time zone: Eastern Time (US & Canada) change

Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada) change

Tue 17 Jan
Displayed time zone: Eastern Time (US & Canada) change

Wed 18 Jan
Displayed time zone: Eastern Time (US & Canada) change

Thu 19 Jan
Displayed time zone: Eastern Time (US & Canada) change

Fri 20 Jan
Displayed time zone: Eastern Time (US & Canada) change

Sat 21 Jan
Displayed time zone: Eastern Time (US & Canada) change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

POPL 2023 Program

Switch Program View

Program Display Configuration

Sun 15 JanDisplayed time zone: Eastern Time (US & Canada) change

Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change

Tue 17 JanDisplayed time zone: Eastern Time (US & Canada) change

Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change

Thu 19 JanDisplayed time zone: Eastern Time (US & Canada) change

Fri 20 JanDisplayed time zone: Eastern Time (US & Canada) change

Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change

Get Calendar (iCal)

Sun 15 Jan
Displayed time zone: Eastern Time (US & Canada) change

Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada) change

Tue 17 Jan
Displayed time zone: Eastern Time (US & Canada) change

Wed 18 Jan
Displayed time zone: Eastern Time (US & Canada) change

Thu 19 Jan
Displayed time zone: Eastern Time (US & Canada) change

Fri 20 Jan
Displayed time zone: Eastern Time (US & Canada) change

Sat 21 Jan
Displayed time zone: Eastern Time (US & Canada) change