Marco Polo - WITS 2025

VenueCurtis Hotel Denver

Room nameMarco Polo

Floor3

Capacity450

Room InformationNo extra information available

Program

This program is tentative and subject to change.

Time Zone

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

Use conference time zone: (GMT-07:00) Mountain 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

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30	Session 1CPP at Marco Polo Chair(s): Nicolas Tabareau Inria

09:00 60m Keynote		Prospects for Computer Formalization of Infinite-Dimensional Category Theory CPP Emily Riehl Johns Hopkins University
10:00 30m Talk		Certifying rings of integers in number fieldsdistinguished paper CPP Anne Baanen Vrije Universiteit Amsterdam, Alain Chavarri Villarello Vrije Universiteit Amsterdam, Sander R. Dahmen Vrije Universiteit Amsterdam

11:00 - 12:30	Session 2CPP at Marco Polo Chair(s): Jennifer Paykin Intel

11:00 30m Talk		Split Decisions: Explicit Contexts for Substructural Languagesdistinguished paper CPP Daniel Zackon McGill University, Chuta Sano McGill University, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University
11:30 30m Talk		Machine Checked Proofs and Programs in Algebraic Combinatorics CPP Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA
12:00 30m Talk		Monadic interpreters for concurrent memory models: Executable semantics of a concurrent subset of LLVM IRremote presentation CPP Nicolas Chappe Inria Lyon, LIP, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski Inria

14:00 - 15:30	Session 3CPP at Marco Polo Chair(s): Yasuhiko Minamide Tokyo Institute of Technology

14:00 30m Talk		An Isabelle formalization of co-rewrite pairs for non-reachability in conditional rewriting CPP Dohan Kim University of Innsbruck, Teppei Saito Japan Advanced Institute of Science and Technology, Japan, René Thiemann University of Innsbruck, Akihisa Yamada National Institute of Informatics
14:30 30m Talk		Intrinsically Correct Sorting in Cubical Agda CPP Cass Alexandru RPTU Kaiserslautern-Landau, Vikraman Choudhury Università di Bologna & Inria OLAS, Jurriaan Rot Radboud University Nijmegen, Niels van der Weide Radboud University
15:00 30m Talk		Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems CPP Christina Kirk University of Innsbruck, Aart Middeldorp University of Innsbruck

16:00 - 17:30	Session 4CPP at Marco Polo

16:00 30m Talk		Formalized Burrows-Wheeler Transform CPP Louis Cheung University of Melbourne, Alistair Moffat The University of Melbourne, Christine Rizkallah University of Melbourne
16:30 30m Talk		Verified and Efficient Matching of Regular Expressions with Lookaroundremote presentation CPP Agnishom Chattopadhyay Rice University, Wu Angela Li Rice University, Konstantinos Mamouras Rice University
17:00 30m Talk		Further Tackling Post Correspondence Problem and Proof Generation CPP Akihiro Omori Department of Mathematical and Computing Science, Tokyo Institute of Technology, Yasuhiko Minamide Tokyo Institute of Technology

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30	Session 5CPP at Marco Polo Chair(s): Sandrine Blazy University of Rennes

09:00 60m Keynote		CRIS: The power of imagination in specification and verification CPP A: Chung-Kil Hur Seoul National University
10:00 30m Talk		The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logicdistinguished paper CPP Simon Friis Vindum Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Lars Birkedal Aarhus University

11:00 - 12:30	Session 6CPP at Marco Polo

11:00 30m Talk		Leakage-Free Probabilistic Jasmin Programs CPP Denis Firsov Tallinn University of Technology, Tiago Oliveira SandboxAQ, José Bacelar Almeira University of Minho & INESC TEC, Dominique Unruh RWTH Aachen
11:30 30m Talk		Formally verified hardening of C programs against hardware fault injection CPP Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC), Sylvain Boulmé Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, David Monniaux CNRS, Marie-Laure Potet Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG Pre-print
12:00 30m Talk		CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq CPP Wolfgang Meier Aarhus University, Martin Jensen Aarhus University, Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University

14:00 - 15:30	Session 7CPP at Marco Polo

14:00 30m Talk		Nominal Matching Logic With Fixpoints CPP James Cheney University of Edinburgh, Maribel Fernandez King's College London, Mircea Sebe UIUC
14:30 30m Talk		Tactic Script Optimisation for Aesop CPP Jannis Limperg University of Munich (LMU)
15:00 30m Talk		An Isabelle/HOL Framework for Synthetic Completeness Proofs CPP Asta Halkjær From University of Copenhagen

16:00 - 17:30	Session 8CPP at Marco Polo

16:00 30m Talk		Formalization of Differential Privacy in Isabelle/HOL CPP Tetsuya Sato Tokyo Institute of Technology, Yasuhiko Minamide Tokyo Institute of Technology
16:30 30m Talk		A CHERI C Memory Model for Verified Temporal Safety CPP Vadim Zaliva University of Cambridge, UK, Kayvan Memarian University of Cambridge, Brian Campbell University of Edinburgh, Ricardo Almeida University of Edinburgh, Nathaniel Filardo University of Cambridge, Ian Stark The University of Edinburgh, Peter Sewell University of Cambridge
17:00 30m Talk		Formalizing the One-way to Hiding Theorem CPP Katharina Heidler Technical University Munich, Dominique Unruh RWTH Aachen

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00	Automata and Temporal PropertiesPOPL at Marco Polo

10:40 20m Talk		Coinductive Proofs for Temporal Hyperliveness POPL Arthur Correnson CISPA Helmholtz Center for Information Security, Bernd Finkbeiner CISPA Helmholtz Center for Information Security
11:00 20m Talk		Derivative-Guided Symbolic Execution POPL Yongwei Yuan Purdue University, Zhe Zhou Purdue University, Julia Belyakova Purdue University, Suresh Jagannathan Purdue University
11:20 20m Talk		Symbolic Automata: omega-Regularity Modulo Theories POPL Margus Veanes Microsoft Research, Thomas Ball Microsoft Research, Gabriel Ebner Microsoft Research, Ekaterina Zhuchko Tallinn University of Technology
11:40 20m Talk		Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis POPL Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security Pre-print

13:20 - 14:20	Quantum Computing 1POPL at Marco Polo

13:20 20m Talk		Linear and non-linear relational analyses for Quantum Program Optimization POPL Matthew Amy Simon Fraser University, Joseph Lunderville Simon Fraser University
13:40 20m Talk		Automating equational proofs in Dirac notation POPL Yingte Xu MPI-SP and Institute of Software, Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Li Zhou Institute of Software, Chinese Academy of Sciences
14:00 20m Talk		Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages POPL Andrea Colledan University of Bologna & INRIA Sophia Antipolis, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis

15:00 - 16:20	Probabilistic Programming 1POPL at Marco Polo

15:00 20m Talk		A quantitative probabilistic relational Hoare logic POPL Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Benjamin Gregoire INRIA, Davide Davoli Université Côte d’Azur, Inria
15:20 20m Talk		Approximate Relational Reasoning for Higher-Order Probabilistic Programs POPL Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University Pre-print
15:40 20m Talk		Compositional imprecise probability: a solution from graded monads and Markov categories POPL Jack Liell-Cock University of Oxford, Sam Staton University of Oxford
16:00 20m Talk		Sound and Complete Proof Rules for Probabilistic Termination POPL Rupak Majumdar MPI-SWS, V.R. Sathiyanarayana MPI-SWS

	17:00 - 18:00	TOPLASPOPL at Marco Polo

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00	Probabilistic Programming 2POPL at Marco Polo

10:40 20m Talk		Inference Plans for Hybrid Particle Filtering POPL Ellie Y. Cheng MIT, Eric Atkinson , Guillaume Baudart Inria, Louis Mandel IBM Research, USA, Michael Carbin Massachusetts Institute of Technology
11:00 20m Talk		Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops POPL Fabian Zaiser University of Oxford, Andrzej Murawski University of Oxford, C.-H. Luke Ong NTU Pre-print
11:20 20m Talk		Modelling Recursion and Probabilistic Choice in Guarded Type Theory POPL Philipp Stassen Aarhus University, Rasmus Ejlers Møgelberg IT University of Copenhagen, Maaike Annebet Zwart IT University of Copenhagen, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University
11:40 20m Talk		Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning POPL Jialu Bao Cornell University, Emanuele D'Osualdo University of Konstanz, Azadeh Farzan University of Toronto

13:20 - 14:20	Decision ProceduresPOPL at Marco Polo

13:20 20m Talk		The Decision Problem for Regular First Order Theories POPL Umang Mathur National University of Singapore, David Mestel Maastricht University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
13:40 20m Talk		A Primal-Dual Perspective on Program Verification Algorithms POPL Takeshi Tsukada Chiba University, Hiroshi Unno Tohoku University, Oded Padon Weizmann Institute of Science, Sharon Shoham Tel Aviv University
14:00 20m Talk		Dis/Equality Graphs POPL George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Jahrim Gabriele Cesario University of St. Gallen, Guido Salvaneschi University of St. Gallen

15:00 - 16:20	Types 1POPL at Marco Polo

15:00 20m Talk		A Dependent Type Theory for Meta-programming with Intensional Analysis POPL Jason Z.S. Hu McGill University, Brigitte Pientka McGill University
15:20 20m Talk		Avoiding signature avoidance in ML modules with zippers POPL Clément Blaudeau Inria, Didier Rémy Inria, Gabriel Radanne Inria
15:40 20m Talk		Bidirectional Higher-Rank Polymorphism with Intersection and Union Types POPL Shengyi Jiang , Chen Cui University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
16:00 20m Talk		Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs POPL Taro Sekiyama National Institute of Informatics; SOKENDAI, Hiroshi Unno Tohoku University

17:00 - 17:40	Quantum Computing 2POPL at Marco Polo

17:00 20m Talk		Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime POPL Kengo Hirata University of Edinburgh, Chris Heunen University of Edinburgh
17:20 20m Talk		Verifying Quantum Circuits with Level-Synchronized Tree Automata POPL Parosh Aziz Abdulla Uppsala University, Sweden, Yo-Ga Chen Academia Sinica, Yu-Fang Chen Academia Sinica, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Fang-Yi Lo Academia Sinica, Wei-Lun Tsai Academia Sinica

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00	Synthesis and CompilationPOPL at Marco Polo

10:40 20m Talk		MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age POPL Roland Leißa University of Mannheim, School of Business Informatics and Mathematics, Marcel Ullrich Saarland University, Joachim Meyer Compiler Design Lab; Saarland Informatics Campus; Saarland University, Sebastian Hack Saarland University, Saarland Informatics Campus
11:00 20m Talk		Simple Linear Loops: Algebraic Invariants and Applications POPL Rida Ait El Manssour CNRS & IRIF, Paris, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS & IRIF, Paris, Anton Varonka TU Wien
11:20 20m Talk		Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus POPL Yufan Cai National University of Singapore, Zhe Hou Griffith University, David Sanan Nanyang Technological University, Singapore, Xiaokun Luan Peking University, Yun Lin Shanghai Jiao Tong University, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore
11:40 20m Talk		Tail Modulo Cons, OCaml, and Relational Separation Logic POPL Clément Allain INRIA, Frédéric Bour Tarides, Basile Clément OCamlPro, François Pottier Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS

13:20 - 14:20	Verification 2POPL at Marco Polo

13:20 20m Talk		Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting POPL Yonghyun Kim Seoul National University, South Korea, Minki Cho Seoul National University, Jaehyung Lee Seoul National University, Jinwoo Kim Seoul National University, Taeyoung Yoon Seoul National University, Youngju Song MPI-SWS, Chung-Kil Hur Seoul National University
13:40 20m Research paper		Formalising Graph Algorithms with Coinduction POPL Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London Pre-print
14:00 20m Talk		VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems POPL Yoonseung Kim Yale University, Sung-Hwan Lee Seoul National University, Yonghyun Kim Seoul National University, South Korea, Chung-Kil Hur Seoul National University

15:00 - 16:20	Concurrency 2POPL at Marco Polo

15:00 20m Talk		Flo: a Semantic Foundation for Progressive Stream Processing POPL Shadaj Laddad University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein UC Berkeley, Mae Milano Princeton University Pre-print
15:20 20m Talk		Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types POPL Thien Udomsrirungruang University of Oxford, Nobuko Yoshida University of Oxford
15:40 20m Talk		Semantic Logical Relations for Timed Message-Passing Protocols POPL Yue Yao Carnegie Mellon University, Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Stephanie Balzer Carnegie Mellon University, Lukasz Ziarek University at Buffalo
16:00 20m Talk		Reachability Analysis of the Domain Name System POPL Dhruv Nevatia ETH Zurich, Si Liu ETH Zurich, David Basin ETH Zurich

17:00 - 18:00	Speculative ExecutionPOPL at Marco Polo

17:00 20m Talk		Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks POPL Xaver Fabian CISPA, Marco Patrignani University of Trento, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security
17:20 20m Talk		Preservation of speculative constant-time by compilation POPL Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria
17:40 20m Talk		SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations POPL Sören van der Wall PhD Student, Roland Meyer TU Braunschweig

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Marco Polo	CPP Session 1																								CPP Session 2																																				CPP Session 3																								CPP Session 4

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Marco Polo	CPP Session 5																								CPP Session 6																																				CPP Session 7																								CPP Session 8

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Marco Polo									POPL Automata and Temporal Properties																																POPL Quantum Computing 1																				POPL Probabilistic Programming 1																								POPL TOPLAS

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Marco Polo									POPL Probabilistic Programming 2																																POPL Decision Procedures																				POPL Types 1																								POPL Quantum Computing 2

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Marco Polo									POPL Synthesis and Compilation																																POPL Verification 2																				POPL Concurrency 2																								POPL Speculative Execution

Mon 20 Jan
Displayed time zone: Mountain 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
Marco Polo	CPP Prospects for Computer Formalization of Infinite-Dimensional Category T ... 09:00 - 10:00												CPPdistinguished paper Certifying rings of integers in number fields 10:00 - 10:30												CPPdistinguished paper Split Decisions: Explicit Contexts for Substructural Languages 11:00 - 11:30						CPP Machine Checked Proofs and Programs in Algebraic Combinatorics 11:30 - 12:00						CPPremote presentation Monadic interpreters for concurrent memory models: Executable semantics ... 12:00 - 12:30																								CPP An Isabelle formalization of co-rewrite pairs for non-reachability in c ... 14:00 - 14:30						CPP Intrinsically Correct Sorting in Cubical Agda 14:30 - 15:00						CPP Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear R ... 15:00 - 15:30												CPP Formalized Burrows-Wheeler Transform 16:00 - 16:30						CPPremote presentation Verified and Efficient Matching of Regular Expressions with Lookaround 16:30 - 17:00						CPP Further Tackling Post Correspondence Problem and Proof Generation 17:00 - 17:30

Tue 21 Jan
Displayed time zone: Mountain 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
Marco Polo	CPP CRIS: The power of imagination in specification and verification 09:00 - 10:00												CPPdistinguished paper The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Se ... 10:00 - 10:30												CPP Leakage-Free Probabilistic Jasmin Programs 11:00 - 11:30						CPP Formally verified hardening of C programs against hardware fault injection 11:30 - 12:00						CPP CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq 12:00 - 12:30																								CPP Nominal Matching Logic With Fixpoints 14:00 - 14:30						CPP Tactic Script Optimisation for Aesop 14:30 - 15:00						CPP An Isabelle/HOL Framework for Synthetic Completeness Proofs 15:00 - 15:30												CPP Formalization of Differential Privacy in Isabelle/HOL 16:00 - 16:30						CPP A CHERI C Memory Model for Verified Temporal Safety 16:30 - 17:00						CPP Formalizing the One-way to Hiding Theorem 17:00 - 17:30

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	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
Marco Polo									POPL Coinductive Proofs for Temporal Hyperliveness 10:40 - 11:00				POPL Derivative-Guided Symbolic Execution 11:00 - 11:20				POPL Symbolic Automata: omega-Regularity Modulo Theories 11:20 - 11:40				POPL Translation of Temporal Logic for Efficient Infinite-State Reactive Syn ... 11:40 - 12:00																				POPL Linear and non-linear relational analyses for Quantum Program Optimization 13:20 - 13:40				POPL Automating equational proofs in Dirac notation 13:40 - 14:00				POPL Flexible Type-Based Resource Estimation in Quantum Circuit Description ... 14:00 - 14:20												POPL A quantitative probabilistic relational Hoare logic 15:00 - 15:20				POPL Approximate Relational Reasoning for Higher-Order Probabilistic Programs 15:20 - 15:40				POPL Compositional imprecise probability: a solution from graded monads and ... 15:40 - 16:00				POPL Sound and Complete Proof Rules for Probabilistic Termination 16:00 - 16:20

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	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
Marco Polo									POPL Inference Plans for Hybrid Particle Filtering 10:40 - 11:00				POPL Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic ... 11:00 - 11:20				POPL Modelling Recursion and Probabilistic Choice in Guarded Type Theory 11:20 - 11:40				POPL Bluebell: An Alliance of Relational Lifting and Independence For Probab ... 11:40 - 12:00																				POPL The Decision Problem for Regular First Order Theories 13:20 - 13:40				POPL A Primal-Dual Perspective on Program Verification Algorithms 13:40 - 14:00				POPL Dis/Equality Graphs 14:00 - 14:20												POPL A Dependent Type Theory for Meta-programming with Intensional Analysis 15:00 - 15:20				POPL Avoiding signature avoidance in ML modules with zippers 15:20 - 15:40				POPL Bidirectional Higher-Rank Polymorphism with Intersection and Union Types 15:40 - 16:00				POPL Algebraic Temporal Effects: Temporal Verification of Recursively Typed ... 16:00 - 16:20												POPL Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime 17:00 - 17:20				POPL Verifying Quantum Circuits with Level-Synchronized Tree Automata 17:20 - 17:40

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change


Room	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
Marco Polo									POPL MimIR: An Extensible and Type-Safe Intermediate Representation for the ... 10:40 - 11:00				POPL Simple Linear Loops: Algebraic Invariants and Applications 11:00 - 11:20				POPL Automated Program Refinement: Guide and Verify Code Large Language Mode ... 11:20 - 11:40				POPL Tail Modulo Cons, OCaml, and Relational Separation Logic 11:40 - 12:00																				POPL Archmage and CompCertCast: End-to-End Verification Supporting Integer-P ... 13:20 - 13:40				POPL Formalising Graph Algorithms with Coinduction 13:40 - 14:00				POPL VeriRT: An End-To-End Verification Framework for Real-Time Distributed ... 14:00 - 14:20												POPL Flo: a Semantic Foundation for Progressive Stream Processing 15:00 - 15:20				POPL Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Se ... 15:20 - 15:40				POPL Semantic Logical Relations for Timed Message-Passing Protocols 15:40 - 16:00				POPL Reachability Analysis of the Domain Name System 16:00 - 16:20												POPL Do You Even Lift? Strengthening Compiler Security Guarantees Against Sp ... 17:00 - 17:20				POPL Preservation of speculative constant-time by compilation 17:20 - 17:40				POPL SNIP: Speculative Execution and Non-Interference Preservation for Compi ... 17:40 - 18:00

Room information: Marco Polo

This program is tentative and subject to change.

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

CPP

CPP

CPP

CPP

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

CPP

CPP

CPP

CPP

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tracks

Room information: Marco Polo

This program is tentative and subject to change.

Program Display Configuration

Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change

Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change

Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change

Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change

Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change

Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change

CPP

CPP

CPP

CPP

Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change

CPP

CPP

CPP

CPP

Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change

POPL

POPL

POPL

POPL

Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change

Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change

Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change

Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change

Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change