Write a Blog >>
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sun 19 Jan
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00
Invited 1VMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
09:00
60m
Talk
The Siren Song of Temporal Synthesis
VMCAI
Moshe VardiRice University
10:00 - 10:30
Sunday Morning BreakCatering at Break
10:00
30m
Coffee break
Break
Catering
10:30 - 12:30
Invited Talks, Pulses, Errors and CategoriesPLanQC at Maurepas
Chair(s): Frank Fu
10:30
30m
Talk
Invited Talk: Q# - Going Beyond Quantum Circuits
PLanQC
I: Bettina HeimMicrosoft
Media Attached
11:00
30m
Talk
Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions
PLanQC
I: Frederic T. ChongUniversity of Chicago
Media Attached File Attached
11:30
20m
Talk
Tuning up entanglement through the cloud using Qiskit-OpenPulse
PLanQC
Thomas AlexanderIBM T.J. Watson Research Center, New York, USA, Naoki KanazawaIBM Research, Tokyo, Japan, Daniel EggerIBM Research, Zurich, Switzerland, Ali Javadi-AbhariIBM T.J. Watson Research Center, New York, USA, David C. McKayIBM T.J. Watson Research Center, New York, USA
11:50
20m
Talk
Tracking Errors through Types in Quantum Programs
PLanQC
Kesha HietalaUniversity of Maryland, Robert RandUniversity of Maryland, Michael HicksUniversity of Maryland
Pre-print Media Attached File Attached
12:10
20m
Talk
Quantum CPOs
PLanQC
Andre KornellTulane University, Bert LindenhoviusTulane University, Michael MisloveTulane
10:30 - 12:30
Papers 1VMCAI at St Jerome
Chair(s): Natasha SharyginaUSI Lugano, Switzerland
10:30
30m
Talk
Witnessing Secure Compilation
VMCAI
Kedar NamjoshiBell Labs, Nokia, Lucas M. TabajaraRice University
11:00
30m
Talk
BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
VMCAI
Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Luca OlivieriJuliaSoft SRL, Fausto SpotoU. Verona
11:30
30m
Coffee break
Mini Break
VMCAI
12:00
30m
Talk
Fixing Code That Explodes Under Symbolic Evaluation
VMCAI
Sorawee PorncharoenwaseUniversity of Washington, James BornholtUniversity of Texas at Austin, Emina TorlakUniversity of Washington
12:30 - 14:00
Sunday LunchCatering at Lunch Room
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:05
Formal MethodsPLanQC at Maurepas
Chair(s): Dominique UnruhUniversity of Tartu
14:00
20m
Talk
Runtime Analysis of Quantum Programs: A Formal Approach
PLanQC
Federico OlmedoUniversity of Chile & IMFD Chile, Alejandro Díaz-CaroICC (UBA-CONICET) & UNQ
Pre-print File Attached
14:20
20m
Talk
Qbricks: formal verification in quantum computing
PLanQC
Christopĥe CharetonCEA, LIST, France, Sébastien BardinCEA LIST, François BobotCEA, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay
File Attached
14:40
25m
Talk
Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages
PLanQC
Kesha HietalaUniversity of Maryland, Kartik SinghalUniversity of Chicago, Robert RandUniversity of Maryland, Shih-Han HungUniversity of Maryland, Xiaodi WuUniversity of Maryland, College Park, Michael HicksUniversity of Maryland
Media Attached
14:00 - 15:05
Invited 2VMCAI at St Jerome
Chair(s): Damien ZuffereyMPI-SWS
14:00
65m
Talk
Safety and Robustness for Deep Learning with Provable Guarantees
VMCAI
Marta KwiatkowskaUniversity of Oxford
15:05 - 15:35
Sunday Afternoon BreakCatering at Break
15:35 - 16:35
NISQPLanQC at Maurepas
Chair(s): Will ZengUnitary Fund
15:35
20m
Talk
Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation
PLanQC
Andrew N. GlaudellUniversity of Maryland, Neil Julien RossDalhousie University, Jacob M. TaylorUniversity of Maryland
Pre-print Media Attached File Attached
15:55
20m
Talk
Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices
PLanQC
Yu ZhangUniversity of Science and Technology of China, Haowei DengUniversity of Science and Technology of China, Quanxi LiUniversity of Science and Technology of China
Pre-print Media Attached
16:15
20m
Talk
Quingo: A Domain Specific Language for Quantum Computing with NISQ Features
PLanQC
Xiang FuInstitute for Quantum Information & State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Jintao YuState Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou, China, Xing SuCollege of Meteorology and Oceanography, National University of Defense Technology, Changsha, China, Hanru JiangCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Hua WuShanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China, Dong ChenDepartment of Computing Science, College of Computer, National University of Defense Technology, Changsha, China, Fucheng ChengCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Xi DengCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Jinrong ZhangCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Lei JinSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Yihang YangSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Le XuSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Chunchao HuSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Anqi HuangInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Guangyao HuangInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Xiaogang QiangInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Mingtang DengInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Ping XuInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Wanwei LiuNational University of Defense Technology, Yuxin DengEast China Normal University, Junjie WuInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Yuan FengCentre for Quantum Software and Information, University of Technology Sydney, Australia
File Attached
15:35 - 17:45
Papers 2VMCAI at St Jerome
Chair(s): Kedar NamjoshiBell Labs, Nokia
15:35
32m
Talk
The Correctness of a Code Generator for a Functional Language
VMCAI
Nathanaël CourantINRIA, Antoine SereEcole Polytechnique, Natarajan ShankarSRI International, USA
16:07
32m
Talk
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
VMCAI
Jack GarzellaUniversity of Utah, Marek S. BaranowskiUniversity of Utah, Shaobo HeUniversity of Utah, Zvonimir RakamaricUniversity of Utah
16:40
32m
Coffee break
Mini Break
VMCAI
17:12
32m
Talk
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
VMCAI
Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Noam RinetzkyTel Aviv University, Sharon ShohamTel Aviv university
16:50 - 17:50
Quantum-Classical CommunicationPLanQC at Maurepas
Chair(s): Michael HicksUniversity of Maryland
16:50
20m
Talk
Extending Modern C++ for Heterogeneous Quantum-Classical Computing
PLanQC
Alexander McCaskeyOak Ridge National Laboratory, Tiffany MintzOak Ridge National Laboratory, Eugene DumitrescuOak Ridge National Laboratory, Sarah PowersOak Ridge National Laboratory, Shirley MooreOak Ridge National Laboratory, Pavel LougovskiOak Ridge National Laboratory
17:10
20m
Talk
Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
PLanQC
Dongho LEELRI / CEA LIST, Univ Paris Saclay, Sébastien BardinCEA LIST, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay
File Attached
17:30
20m
Talk
Automated distribution of quantum circuits via hypergraph partitioning
PLanQC
Pablo Andres-MartinezUniversity of Edinburgh, Chris HeunenUniversity of Edinburgh
Link to publication DOI Pre-print Media Attached File Attached

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change

08:30 - 10:00
Logical Engines and ApplicationsPADL at Bacchus
Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK
08:30
15m
Day opening
Opening
PADL
08:45
50m
Talk
Invited Talk: Logical Engines for Cloud Configurations
PADL
I: Nikolaj BjørnerMicrosoft Research
09:35
25m
Talk
Interactive Text Graph Mining with a Prolog-based Dialog Engine
PADL
Paul TarauUniversity of North Texas, Eduardo Blanco
09:00 - 10:00
Verifying Probabilistic Properties with Couplings (I)TutorialFest at Babylon
09:00
60m
Tutorial
[T6] Verifying Probabilistic Properties with Couplings
TutorialFest
Justin HsuUniversity of Wisconsin-Madison, USA
File Attached
09:00 - 10:00
Morning KeynoteADSL at Conde
09:00
60m
Talk
Relational reasoning using concurrent separation logic
ADSL
A: Robbert KrebbersDelft University of Technology
Media Attached File Attached
09:00 - 10:00
Verified Quantum Computing (I)TutorialFest at Endymion
09:00
60m
Tutorial
[T2] Verified Quantum Computing
TutorialFest
Robert RandUniversity of Maryland
Pre-print
09:00 - 10:00
Opening & Keynote Talk 1PEPM at Frontenac
Chair(s): Casper Bach PoulsenDelft University of Technology, Zhenjiang HuPeking University
09:00
5m
Day opening
Opening
PEPM
Casper Bach PoulsenDelft University of Technology, Zhenjiang HuPeking University
09:05
55m
Talk
Network Verification: Past, Present, and Future
PEPM
Nate FosterCornell University
09:00 - 10:00
Invited talkCPP at Maurepas
Chair(s): Cătălin HriţcuInria Paris
09:00
60m
Talk
Invited talk: Matching Logic: The Foundation of the K Framework
CPP
Grigore RoşuUniversity of Illinois at Urbana-Champaign, Xiaohong ChenUniversity of Illinois at Urbana-Champaign
DOI Media Attached
09:00 - 10:00
Building Program Reasoning Tools using LLVM and Z3 (I)TutorialFest at Muses
09:00
60m
Tutorial
[T1] Building Program Reasoning Tools using LLVM and Z3
TutorialFest
Elizabeth DinellaUniversity of Pennsylvania, Pardis PashakhanlooUniversity of Pennsylvania, Anthony Canino, Mayur NaikUniversity of Pennsylvania
Pre-print
09:00 - 10:00
Synthesizing Programs from Types (I)TutorialFest at SHANGRI-LA
09:00
60m
Tutorial
[T3] Synthesizing Programs from Types
TutorialFest
Nadia PolikarpovaUniversity of California, San Diego
Link to publication File Attached
09:00 - 10:00
Invited 3VMCAI at St Jerome
Chair(s): Damien ZuffereyMPI-SWS
09:00
60m
Talk
Model Checking for Safe Autonomy
VMCAI
Rajeev AlurUniversity of Pennsylvania
10:00 - 10:30
Monday Morning BreakCatering at Break
10:30 - 12:30
Verifying Probabilistic Properties with Couplings (II)TutorialFest at Babylon
10:30
2h
Tutorial
[T6] Verifying Probabilistic Properties with Couplings
TutorialFest
Justin HsuUniversity of Wisconsin-Madison, USA
File Attached
10:30 - 12:30
Verified Quantum Computing (II)TutorialFest at Endymion
10:30
2h
Tutorial
[T2] Verified Quantum Computing
TutorialFest
Robert RandUniversity of Maryland
Pre-print
10:30 - 12:30
Sessions 1 & 2PEPM at Frontenac
Chair(s): Ohad KammarUniversity of Edinburgh, Walid Taha
10:30
35m
Talk
Dependently-Typed Multi-Stage Programming Revisited (invited talk)
PEPM
Atsushi IgarashiKyoto University, Japan
11:05
25m
Research paper
High-Fidelity Metaprogramming with Separator Syntax Trees
PEPM
Rodin AarssenCWI, Netherlands, Tijs van der StormCWI & University of Groningen, Netherlands
DOI
11:30
15m
Break
Mini Break 1
PEPM
11:45
25m
Research paper
Module Generation without Regret
PEPM
Yuhi SatoUniversity of Tsukuba, Yukiyoshi KameyamaUniversity of Tsukuba, Japan, Takahisa WatanabeUniversity of Tsukuba, Japan
DOI
12:10
20m
Short-paper
GOOL: A Generic Object-Oriented Language
PEPM
Jacques CaretteMcMaster University, Brooks MacLachlanMcMaster University, Spencer SmithMcMaster University, Computing and Software Department
DOI Pre-print File Attached
10:30 - 11:35
Program verificationCPP at Maurepas
Chair(s): Nikhil SwamyMicrosoft Research
10:30
21m
Talk
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
CPP
Clement BlaudeauEcole Polytechnique, Natarajan ShankarSRI International, USA
DOI Pre-print Media Attached
10:51
22m
Talk
Proof Pearl: Braun Trees
CPP
Tobias NipkowTechnische Universität München, Thomas SewellChalmers University of Technology, Sweden
DOI Pre-print Media Attached
11:13
22m
Talk
FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP
Thomas LetanANSSI, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
DOI Pre-print Media Attached
10:30 - 12:30
Building Program Reasoning Tools using LLVM and Z3 (II)TutorialFest at Muses
10:30
2h
Tutorial
[T1] Building Program Reasoning Tools using LLVM and Z3
TutorialFest
Elizabeth DinellaUniversity of Pennsylvania, Pardis PashakhanlooUniversity of Pennsylvania, Anthony Canino, Mayur NaikUniversity of Pennsylvania
Pre-print
10:30 - 12:30
Synthesizing Programs from Types (II)TutorialFest at SHANGRI-LA
10:30
2h
Tutorial
[T3] Synthesizing Programs from Types
TutorialFest
Nadia PolikarpovaUniversity of California, San Diego
Link to publication File Attached
10:30 - 12:30
Papers 3VMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
10:30
30m
Research paper
A Systematic Approach to Abstract Interpretation of Program Transformations
VMCAI
Sven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz
Pre-print
11:00
30m
Talk
Sharing Ghost Variables in a Collection of Abstract Domains
VMCAI
Marc ChevalierENS, CNRS, PSL University, INRIA, Jerome FeretINRIA Paris
11:30
30m
Coffee break
Mini Break
VMCAI
12:00
30m
Talk
Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
VMCAI
Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Roman ManevichMellanox Technologies, Noam RinetzkyTel Aviv University
11:45 - 12:30
Automated verification and SAT solvingCPP at Maurepas
Chair(s): Ori LahavTel Aviv University
11:45
22m
Talk
Verifying x86 Instruction Implementations
CPP
Shilpi GoelCentaur Technology, Inc., Anna SlobodovaCentaur Technology, Inc., Rob SumnersCentaur Technology, Inc., Sol SwordsCentaur Technology, Inc.
DOI Pre-print File Attached
12:07
22m
Talk
Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs
CPP
DOI Pre-print Media Attached
12:30 - 14:00
Monday LunchCatering at Lunch Room
12:30
90m
Lunch
Lunch
Catering
13:30 - 15:00
Memory and Real-Time in Functional ProgrammingPADL at Bacchus
Chair(s): John HughesChalmers University of Technology, Sweden
13:30
25m
Talk
On the Effects of Integrating Region-based Memory Managemen and Generational Garbage Collection in ML
PADL
Martin ElsmanUniversity of Copenhagen, Denmark, Niels Hallenberg
13:55
25m
Talk
RTMLton: An SML Runtime for Real-Time Systems
PADL
14:20
25m
Talk
A Timed IO Monad
PADL
David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
14:45
15m
Other
Panel: Memory and real-time programming in practice
PADL
Martin ElsmanUniversity of Copenhagen, Denmark, Niels Hallenberg, Bhargav Shivkumar, Jeffrey Murphy, Lukasz ZiarekSUNY Buffalo, USA, David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
14:00 - 15:05
Afternoon KeynoteADSL at Conde
14:00
65m
Talk
SLEdge: Bounded Model Checking in Separation Logic
ADSL
A: Josh BerdineFacebook
File Attached
14:00 - 15:05
Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (I)TutorialFest at Endymion
14:00
65m
Tutorial
[T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models
TutorialFest
Konstantinos (Kostis) SagonasUppsala University, Sweden
14:00 - 15:05
Keynote Talk 2PEPM at Frontenac
Chair(s): Casper Bach PoulsenDelft University of Technology
14:00
60m
Talk
Reasoning about Progress of Concurrent Objects
PEPM
Xinyu FengNanjing University
14:00 - 15:05
Proof engineering and user interactionCPP at Maurepas
Chair(s): Yves BertotINRIA
14:00
21m
Talk
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
CPP
Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Steve ZdancewicUniversity of Pennsylvania
DOI Pre-print Media Attached File Attached
14:21
21m
Talk
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
CPP
Qingxiang WangUniversity of Innsbruck, Chad BrownCzech Technical University in Prague, Cezary KaliszykUniversity of Innsbruck, Josef UrbanCzech Technical University in Prague
DOI Pre-print
14:43
21m
Talk
REPLICA: REPL Instrumentation for Coq Analysis
CPP
Talia RingerUniversity of Washington, Alex Sanchez-SternUniversity of California, San Diego, Dan GrossmanUniversity of Washington, Sorin LernerUniversity of California, San Diego
DOI Pre-print Media Attached
14:00 - 15:05
Proving Semantic Type Soundness in Iris (I)TutorialFest at Muses
14:00
65m
Tutorial
[T4] Proving Semantic Type Soundness in Iris
TutorialFest
Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven
Link to publication File Attached
14:00 - 15:05
Programming and Reasoning with Kleene Algebra with Tests (I)TutorialFest at SHANGRI-LA
14:00
65m
Tutorial
[T7] Programming and Reasoning with Kleene Algebra with Tests
TutorialFest
Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London
File Attached
14:00 - 15:05
Papers 4VMCAI at St Jerome
Chair(s): Ruzica PiskacYale University, USA
14:00
32m
Talk
Synthesizing Environment Invariants for Modular Hardware Verification
VMCAI
Hongce ZhangPrinceton University, Weikun YangPrinceton University, Grigory FedyukovichFlorida State University, Aarti GuptaPrinceton University, Sharad MalikPrinceton University
14:32
32m
Talk
Systematic Classification of Attackers via Bounded Model Checking
VMCAI
Eric Rothstein-MorrisSingapore University of Technology and Design, Jun SunSingapore Management University, Singapore, Sudipta ChattopadhyaySingapore University of Technology and Design
15:05 - 15:35
Monday Afternoon BreakCatering at Break
15:30 - 17:00
Answer Set Programming Applications and Competitive programming experiencePADL at Bacchus
Chair(s): Alex Brik
15:30
25m
Talk
Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming
PADL
Sheung Chi Chan, James CheneyUniversity of Edinburgh, UK
15:55
25m
Talk
On Repairing Web Services Workflows
PADL
Thanh Hai Nguyen, Enrico PontelliNew Mexico State University, Tran Cao Son
16:20
40m
Talk
Competitive Programming with PiCat
PADL
Neng-Fa ZhouCUNY Brooklyn College and Graduate Center
15:35 - 17:45
Closing SessionADSL at Conde
15:35
65m
Talk
Programs Synthesis with Separation Logic
ADSL
Nadia PolikarpovaUniversity of California, San Diego
16:40
65m
Talk
Local Reasoning for Global Graph Properties
ADSL
Thomas WiesNew York University
15:35 - 17:35
Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (II)TutorialFest at Endymion
15:35
2h
Tutorial
[T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models
TutorialFest
Konstantinos (Kostis) SagonasUppsala University, Sweden
15:35 - 16:40
Decidability and complexityCPP at Maurepas
Chair(s): Kathrin StarkPrinceton University, USA
15:35
21m
Talk
Verified Programming of Turing Machines in Coq
CPP
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University
DOI Pre-print Media Attached
15:56
21m
Talk
A Functional Proof Pearl: Inverting the Ackermann Hierarchy
CPP
Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore
DOI Pre-print Media Attached
16:18
21m
Talk
Undecidability of Higher-Order Unification Formalised in Coq
CPP
Simon SpiesSaarland University, Yannick ForsterSaarland University
DOI Pre-print Media Attached
15:35 - 17:35
Proving Semantic Type Soundness in Iris (II)TutorialFest at Muses
15:35
2h
Tutorial
[T4] Proving Semantic Type Soundness in Iris
TutorialFest
Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven
Link to publication File Attached
15:35 - 17:35
Programming and Reasoning with Kleene Algebra with Tests (II)TutorialFest at SHANGRI-LA
15:35
2h
Tutorial
[T7] Programming and Reasoning with Kleene Algebra with Tests
TutorialFest
Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London
File Attached
15:35 - 17:45
Papers 5VMCAI at St Jerome
Chair(s): Nikolaj BjørnerMicrosoft Research
15:35
32m
Talk
Cheap CTL Compassion in NuSMV
VMCAI
Daniel HausmannFriedrich-Alexander-Universität Erlangen-Nürnberg, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8, Christoph RauchFAU Erlangen-Nürnberg, Lehrstuhl 8, Matthias ZinnerFAU Erlangen-Nürnberg
16:07
32m
Talk
A Cooperative Parallelization Approach for Property-Directed k-Induction
VMCAI
Martin BlichaUniversità della Svizzera italiana, Antti HyvärinenUniversità della Svizzera Italiana, Matteo MarescottiUniversità della Svizzera Italiana, Natasha SharyginaUSI Lugano, Switzerland
16:40
32m
Coffee break
Mini Break
VMCAI
17:12
32m
Talk
Generalized Property-Directed Reachability for Hybrid Systems
VMCAI
Kohei SuenagaGraduate School of Informatics, Kyoto University, Takuya IshizawaKyoto University
Link to publication Pre-print
16:50 - 17:56
Homotopy Type Theory and PC chairs' reportCPP at Maurepas
Chair(s): Floris van DoornUniversity of Pittsburgh
16:50
22m
Talk
Cubical Synthetic Homotopy Theory
CPP
Anders MörtbergDepartment of Mathematics, Stockholm University, Loïc PujetGallinette Project-Team, Inria
DOI Pre-print Media Attached File Attached
17:12
22m
Talk
Three equivalent ordinal notation systems in Cubical Agda
CPP
Fredrik Nordvall ForsbergUniversity of Strathclyde, Chuangjie XuLudwig-Maximilians-Universität München, Neil GhaniUniversity of Strathclyde
DOI Pre-print Media Attached File Attached
17:34
22m
Talk
PC Chairs' report
CPP
Jasmin BlanchetteVrije Universiteit Amsterdam, Cătălin HriţcuInria Paris
DOI Media Attached File Attached

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00
Morning 1PLMW at Ile de France III (IDF III)
Chair(s): Stephanie BalzerCarnegie Mellon University, USA
09:00
10m
Day opening
Opening
PLMW
Brigitte PientkaMcGill University
09:10
50m
Talk
How to Write Papers So People Can Read ThemMentoring Event
PLMW
File Attached
09:00 - 10:00
Invited talkCPP at Maurepas
Chair(s): Jasmin BlanchetteVrije Universiteit Amsterdam
09:00
60m
Talk
Invited talk: Proof Assistants at the Hardware-Software Interface
CPP
Adam ChlipalaMassachusetts Institute of Technology
DOI Media Attached
09:00 - 10:00
Opening & Interactive Knowledge SharesHASE at Orpheus
09:00
10m
Day opening
Opening Plenary
HASE
09:10
60m
Tutorial
Interactive Knowledge Shares
HASE
Peter O'HearnFacebook, Philippa GardnerImperial College London, Muralidaran VijayaraghavanSiFive, Peter SewellUniversity of Cambridge
09:00 - 10:00
Papers 6VMCAI at St Jerome
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany
09:00
30m
Talk
How to Win First-Order Safety Games
VMCAI
Helmut SeidlTechnische Universität München, Christian MüllerTechnical University of Munich, Bernd FinkbeinerSaarland University
09:30
30m
Talk
Improving Parity Game Solvers with Justifications
VMCAI
Ruben LapauwKatholieke Universiteit Leuven, Maurice BruynoogheKatholieke Universiteit Leuven, Marc DeneckerKatholieke Universiteit Leuven
10:00 - 10:30
Tuesday Morning BreakCatering at Break
10:30 - 12:30
Ally Skills SessionAlly Skills Session at Frontenac
10:30
2h
Other
Ally Skills SessionMentoring Event
Ally Skills Session
10:30 - 11:35
Mechanized metatheoryCPP at Maurepas
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
10:30
21m
Talk
Coq à la Carte - A Practical Approach to Modular Syntax with Binders
CPP
Yannick ForsterSaarland University, Kathrin StarkPrinceton University, USA
DOI Pre-print Media Attached
10:51
21m
Talk
A Mechanized Formalization of GraphQL
CPP
Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile
DOI Pre-print Media Attached File Attached
11:13
21m
Talk
ConCert: A Smart Contract Certification Framework in Coq
CPP
Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University
DOI Pre-print Media Attached File Attached
10:30 - 12:30
Working Sessions IHASE at Orpheus
10:30
2h
Meeting
Working Sessions I
HASE
Ben LaurieGoogle Research, Hong-Seok Kim, Jonathan ProtzenkoMicrosoft Research, Redmond
10:30 - 12:30
Papers 7VMCAI at St Jerome
Chair(s): Thomas WiesNew York University
10:30
30m
Talk
Language Inclusion for Finite Prime Event Structures
VMCAI
Andreas FellnerAIT - Austrian Institute of Technology, Thorsten TarrachAustrian Institute of Technology, Georg WeissenbacherTechnische Universität Wien
11:00
30m
Talk
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
VMCAI
Swen JacobsCISPA Helmholtz Center for Information Security, Mouhammad SakrSaarland University, Martin ZimmermannUniversity of Liverpool
11:30
30m
Coffee break
Mini Break
VMCAI
12:00
30m
Talk
Solving LIA* Using Approximations
VMCAI
Maxwell LevatichYale, Nikolaj BjørnerMicrosoft Research, Ruzica PiskacYale University, USA, Sharon ShohamTel Aviv university
11:45 - 12:30
Verified cryptographyCPP at Maurepas
Chair(s): Adam ChlipalaMassachusetts Institute of Technology
11:45
22m
Talk
Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
CPP
David ButlerAlan Turing Institute, David AspinallUniversity of Edinburgh, Adria GasconAlan Turing Institute
DOI Pre-print Media Attached
12:07
22m
Talk
Verified Security of BLT Signature Scheme
CPP
Denis FirsovGuardtime AS, Ahto BuldasTallinn University of Technology, Ahto TruuGuardtime AS, Risto LaanojaGuardtime AS
DOI Pre-print Media Attached File Attached
12:30 - 14:00
Tuesday LunchCatering at Lunch Room
12:30
90m
Lunch
Lunch
Catering
13:30 - 15:00
Invited Experience and Direction SessionPADL at Bacchus
Chair(s): David WarrenStony Brook University, Konstantinos (Kostis) SagonasUppsala University, Sweden
13:30
30m
Talk
Invited Talk: Relational Artificial Intelligence
PADL
Molham ArefRelational.ai
14:00
30m
Talk
Invited Talk: Learning Interpretable Rules from Structured Data
PADL
Mayur NaikUniversity of Pennsylvania
14:30
30m
Talk
Invited Talk: An Introduction to the Imandra Automated Reasoning System
PADL
Grant PassmoreImandra Inc.
14:00 - 15:05
Afternoon 1PLMW at Ile de France III (IDF III)
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA
14:00
65m
Talk
PanelMentoring Event
PLMW
William J. BowmanUniversity of British Columbia, Kenny FonerGalois, Andrew HirschMax Planck Institute for Software Systems, Taro SekiyamaNational Institute of Informatics, Juliana FrancoMicrosoft Research, Cambridge, Hannah GommerstadtVassar College
Media Attached
14:00 - 15:05
Concurrency and linearityCPP at Maurepas
Chair(s): Zhong ShaoYale University
14:00
21m
Talk
Formalizing Determinacy of Concurrent Revisions
CPP
Roy OverbeekVrije Universiteit Amsterdam
DOI Pre-print Media Attached
14:21
21m
Talk
Formalizing π-calculus in Guarded Cubical Agda
CPP
Niccolò VeltriTallinn University of Technology, Andrea VezzosiIT University Copenhagen
DOI Pre-print Media Attached File Attached
14:43
21m
Talk
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
CPP
Arjen RouvoetDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
DOI Pre-print Media Attached File Attached
14:00 - 15:05
Peer SkillshareHASE at Orpheus
13:30
45m
Tutorial
Peer Skillshare
HASE
Sarah de HaasGoogle Research
14:00 - 15:05
14:00
30m
Talk
Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support
LAFI
Yuan ZhouUniversity of Oxford, Hongseok YangKAIST, Yee Whye TehUniversity of Oxford, Tom RainforthDepartment of Statistics, University of Oxford
14:32
15m
Talk
MetaPPL: Inference Algorithms as First-Class Generative Models
LAFI
Alexander K. LewMassachusetts Institute of Technology, USA, Benjamin ShermanMassachusetts Institute of Technology, USA, Marco Cusumano-TownerMIT-CSAIL, Austin GarrettMIT, Ben ZinbergMIT, Vikash K. MansinghkaMIT, Michael CarbinMassachusetts Institute of Technology
File Attached
14:49
16m
Talk
Monte Carlo Semantic Differencing of Probabilistic Programs
LAFI
14:00 - 15:05
Papers 8VMCAI at St Jerome
Chair(s): Ori LahavTel Aviv University
14:00
32m
Talk
Formalizing and Checking Multilevel Consistency
VMCAI
Ahmed BouajjaniIRIF, Université Paris Diderot, Constantin EneaIRIF, University Paris Diderot & CNRS, Madhavan MukundChennai Mathematical Institute, Gautham Shenoy RChennai Mathematical Institute, S.P. SureshChennai Mathematical Institute
14:32
32m
Talk
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
VMCAI
Wytse OortwijnETH Zürich, Dilian GurovKTH Royal Institute of Technology, Marieke HuismanUniversity of Twente
15:05 - 15:35
Tuesday Afternoon BreakCatering at Break
15:30 - 17:00
Invited Experience and Direction Session (Continued)PADL at Bacchus
Chair(s): Y. Annie LiuStony Brook University, David WarrenStony Brook University, Konstantinos (Kostis) SagonasUppsala University, Sweden
15:30
30m
Talk
Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types
PADL
Philip WadlerUniversity of Edinburgh, UK
16:00
45m
Other
Panel: Experience and Direction
PADL
I: Molham ArefRelational.ai, I: Mayur NaikUniversity of Pennsylvania, I: Grant PassmoreImandra Inc., I: Philip WadlerUniversity of Edinburgh, UK
16:45
15m
Day closing
Closing
PADL
Ekaterina KomendantskayaHeriot-Watt University, UK, Y. Annie LiuStony Brook University
15:35 - 17:45
POPLmark 15 Year Retrospective PanelPOPLmark 15 Year Retrospective Panel at Frontenac
15:35
2h
Other
POPLmark 15 Year Retrospective Panel
POPLmark 15 Year Retrospective Panel
15:35 - 16:40
Formalized mathematics 1CPP at Maurepas
Chair(s): Robert Y. LewisVrije Universiteit Amsterdam
15:35
21m
Talk
Formalising perfectoid spaces
CPP
Patrick MassotUniversité Paris Sud, Kevin BuzzardImperial College London, Johan CommelinUniversität Freiburg
DOI Pre-print Media Attached File Attached
15:56
21m
Talk
A Constructive Formalization of the Weak Perfect Graph Theorem
CPP
Abhishek Kr SinghTata Institute of Fundamental Research Mumbai, Raja NatarajanTata Institute of Fundamental Research Mumbai
DOI Pre-print Media Attached File Attached
16:18
21m
Talk
Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
CPP
Christian DoczkalUniversité Côte d'Azur, Damien PousCNRS, ENS Lyon
DOI Pre-print Media Attached
15:35 - 17:45
Afternoon SessionHASE at Orpheus
14:30
2h
Meeting
Working Sessions II
HASE
Ben LaurieGoogle Research, Satnam SinghGoogle Research
16:30
75m
Day closing
Closing Plenary
HASE
15:35 - 17:45
15:35
30m
Talk
Coinductive Trees for Exact Inference of Probabilistic Programs
LAFI
Alexander BagnallOhio University, Gordon StewartOhio University, Anindya BanerjeeIMDEA Software Institute
16:05
30m
Talk
Name generation and Higher-order Probabilistic Programming (Or is new=rnd?)
LAFI
Dario SteinUniversity of Oxford, Sam StatonUniversity of Oxford, Michael WolmanMcGill University
File Attached
16:35
30m
Talk
Density Functions of Statistical Probabilistic Programs
LAFI
Tom MattinsonUniversity of Oxford, C.-H. Luke OngUniversity of Oxford
17:05
30m
Talk
Probabilistic Programming around Gaussian Processes
LAFI
17:35
10m
Day closing
Closing
LAFI
15:35 - 17:45
Panel SessionVMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
15:35
2h10m
Other
Panel "The Future of Software Verification" at VMCAI
VMCAI
Lenore ZuckUIC, Michael WhalenAmazon Web Services and the University of Minnesota, Natarajan ShankarSRI International, USA, Andreas PodelskiUniversity of Freiburg, Germany, Dirk BeyerLMU Munich
16:50 - 17:56
Formalized mathematics 2CPP at Maurepas
Chair(s): Tobias NipkowTechnische Universität München
16:50
22m
Talk
The Poincaré-Bendixson Theorem in Isabelle/HOL
CPP
Fabian ImmlerCarnegie Mellon University, Yong Kiam TanCarnegie Mellon University, USA
DOI Pre-print Media Attached
17:12
22m
Talk
A Formal Proof of the Independence of the Continuum Hypothesis
CPP
Jesse Michael HanUniversity of Pittsburgh, Floris van DoornUniversity of Pittsburgh
DOI Pre-print Media Attached
17:34
22m
Talk
The Lean mathematical library
CPP
DOI Pre-print Media Attached File Attached

Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change

07:45 - 08:45
Wednesday Mentoring BreakfastMentoring Breakfasts at Breakfast Room
07:45
60m
Social Event
Mentoring BreakfastMentoring Event
Mentoring Breakfasts
08:45 - 09:00
Welcome + SIGPLAN Award CeremonyResearch Papers at Ile de France II (IDF II)
Chair(s): Brigitte PientkaMcGill University, Jens PalsbergUniversity of California, Los Angeles, Lars BirkedalAarhus University
08:45
15m
Day opening
Welcome + SIGPLAN Award Ceremony
Research Papers
Media Attached
10:00 - 10:30
Wednesday Morning BreakCatering at Break
10:30 - 11:35
Complexity / Decision ProceduresResearch Papers at Ile de France III (IDF III)
Chair(s): Roopsha SamantaPurdue University
10:30
21m
Talk
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
Research Papers
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Marc RothSaarland University and MMCI and Merton College, Oxford University
Link to publication DOI Pre-print Media Attached
10:51
21m
Talk
Complexity and Information in Invariant Inference
Research Papers
Yotam M. Y. FeldmanTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
Link to publication DOI Media Attached
11:13
21m
Talk
Parameterized Verification under TSO is PSPACE-Complete
Research Papers
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Rojin RezvanSharif University
Link to publication DOI
11:45 - 12:30
Reasoning about Program Complexity/EfficiencyResearch Papers at Ile de France II (IDF II)
Chair(s): Thomas WiesNew York University
11:45
22m
Talk
Recurrence Extraction for Functional Programs through Call-by-Push-Value
Research Papers
Alex KavvosAarhus University, Edward MorehouseWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan University
Link to publication DOI File Attached
12:07
22m
Talk
Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell
Research Papers
Martin Adam Thomas HandleyUniversity of Nottingham, Niki VazouIMDEA Software Institute, Graham HuttonUniversity of Nottingham, UK
Link to publication DOI Media Attached File Attached
11:45 - 12:30
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen LesaniUniversity of California, Riverside
11:45
22m
Talk
Program Synthesis by Type-Guided Abstraction Refinement
Research Papers
Zheng GuoUniversity of California, San Diego, Michael B. JamesUniversity of California, San Diego, David JustoUniversity of California, San Diego, Jiaxiao ZhouUniversity of California, San Diego, Ziteng WangUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Synthesizing Replacement Classes
Research Papers
Link to publication DOI Media Attached File Attached
12:30 - 14:00
LGBTQ LunchLGBTQ Lunch at Endymion
12:30
90m
Lunch
LGBTQ LunchMentoring Event
LGBTQ Lunch
12:30 - 14:00
Wednesday LunchCatering at Lunch Room
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:05
Program LogicsResearch Papers at Ile de France II (IDF II)
Chair(s): Azalea RaadMPI-SWS, Germany
14:00
21m
Talk
The Future is Ours: Prophecy Variables in Separation Logic
Research Papers
Ralf JungMPI-SWS, Rodolphe LepigreMPI-SWS, Gaurav ParthasarathyETH Zurich, Marianna RapoportUniversity of Waterloo, Amin Timanyimec-Distrinet KU-Leuven, Derek DreyerMPI-SWS, Bart Jacobsimec-DistriNet, Dept. CS, KU Leuven
Link to publication DOI Media Attached
14:21
21m
Talk
Spy Game: Verifying a Local Generic Solver in Iris
Research Papers
Paulo Emílio de VilhenaInria, François PottierInria, France, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Actris: Session-Type Based Reasoning in Separation Logic
Research Papers
Jonas Kastberg HinrichsenIT University of Copenhagen, Jesper BengtsonIT University of Copenhagen, Robbert KrebbersDelft University of Technology
Link to publication DOI Media Attached File Attached
14:00 - 15:05
Gradual Typing / Language DesignResearch Papers at Ile de France III (IDF III)
Chair(s): Jeremy G. SiekIndiana University, USA
14:00
21m
Talk
What is Decidable about Gradual Types?
Research Papers
Zeina MigeedUniversity of California, Los Angeles, Jens PalsbergUniversity of California, Los Angeles
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Graduality and Parametricity: Together Again for the First Time
Research Papers
Max NewNortheastern University, Dustin JamnerNortheastern University, USA, Amal AhmedNortheastern University, USA
Link to publication DOI Media Attached
14:43
21m
Talk
Does Blame Shifting Work?
Research Papers
Lukas LazarekNorthwestern University, Alexis KingNorthwestern University, Samanvitha SundarNorthwestern University, Robby FindlerNorthwestern University, USA, Christos DimoulasPLT @ Northwestern University
Link to publication DOI Media Attached
15:05 - 15:35
Wednesday Afternoon BreakCatering at Break
15:35 - 16:40
Automatic Differentiation / Kleene AlgebraResearch Papers at Ile de France II (IDF II)
Chair(s): Lars BirkedalAarhus University
15:35
21m
Talk
A Simple Differentiable Programming Language
Research Papers
Link to publication DOI Media Attached
15:56
21m
Talk
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Research Papers
Aloïs BrunelDeepomatic, Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear TimeDistinguished Paper
Research Papers
Steffen SmolkaCornell University, Nate FosterCornell University, Justin HsuUniversity of Wisconsin-Madison, USA, Tobias KappéUniversity College London, Dexter KozenCornell University, Alexandra SilvaUniversity College London
Link to publication DOI Media Attached
15:35 - 16:40
Concurrency / MemoryResearch Papers at Ile de France III (IDF III)
Chair(s): Susmit SarkarUniversity of St. Andrews
15:35
21m
Talk
Persistency Semantics of the Intel-x86 Architecture
Research Papers
Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, Germany
Link to publication DOI Media Attached
15:56
21m
Talk
Reductions for Safety Proofs
Research Papers
Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto
Link to publication DOI Media Attached
16:18
21m
Talk
RustBelt Meets Relaxed Memory
Research Papers
Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-SWS
Link to publication DOI Media Attached
16:50 - 17:35
Synthesis and Decision ProceduresResearch Papers at Ile de France II (IDF II)
Chair(s): Roopsha SamantaPurdue University
16:50
22m
Talk
Visualization by Example
Research Papers
Chenglong WangUniversity of Washington, USA, Yu FengUniversity of California, Santa Barbara, Rastislav BodikUniversity of Washington, Alvin CheungUniversity of California, Berkeley, Isil DilligUniversity of Texas Austin
Link to publication DOI Media Attached
17:12
22m
Talk
Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Research Papers
Umang MathurUniversity of Illinois at Urbana-Champaign, Adithya MuraliUniversity of Illinois at Urbana-Champaign, Paul KrogmeierUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached File Attached
16:50 - 19:00
SRC Poster SessionStudent Research Competition at SRC
16:50
2h10m
Poster
SRC Poster Session
Student Research Competition
17:35 - 18:35
Social Hour (Supported by Facebook)Research Papers at Social Hour
17:35
60m
Social Event
Social Hour (Supported by Facebook)
Research Papers

Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change

07:45 - 09:00
Thursday Mentoring BreakfastMentoring Breakfasts at Breakfast Room
07:45
75m
Social Event
Mentoring BreakfastMentoring Event
Mentoring Breakfasts
10:00 - 10:30
Thursday Morning BreakCatering at Break
10:30 - 11:35
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen LesaniUniversity of California, Riverside
10:30
21m
Talk
Synthesis of Coordination Programs from Linear Temporal Specifications
Research Papers
Suguman BansalRice University, USA, Kedar NamjoshiBell Labs, Nokia, Yaniv Sa'arNokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
Augmented Example-based Synthesis using Relational Perturbation Properties
Research Papers
Shengwei AnPurdue University, Rishabh SinghGoogle Brain, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Roopsha SamantaPurdue University
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Provenance-Guided Synthesis of Datalog Programs
Research Papers
Mukund RaghothamanUniversity of Southern California, Jonathan MendelsonUniversity of Pennsylvania, David ZhaoThe University of Sydney, Mayur NaikUniversity of Pennsylvania, Bernhard ScholzUniversity of Sydney, Australia
Link to publication DOI Media Attached File Attached
11:45 - 12:30
Dynamic Program AnalysisResearch Papers at Ile de France II (IDF II)
Chair(s): Peter ThiemannUniversity of Freiburg, Germany
11:45
22m
Talk
Fast, Sound, and Effectively Complete Dynamic Race Prediction
Research Papers
Andreas PavlogiannisAarhus University
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Detecting Floating-Point Errors via Atomic Conditions
Research Papers
Daming ZouPeking University, Muhan ZengPeking University, Yingfei XiongPeking University, Zhoulai FuIT University of Copenhagen, Denmark, Lu ZhangPeking University, Zhendong SuETH Zurich
Link to publication DOI Media Attached File Attached
11:45 - 12:30
Datalog, OO + Functional ProgrammingResearch Papers at Ile de France III (IDF III)
Chair(s): Brigitte PientkaMcGill University
11:45
22m
Talk
Seminaïve Evaluation for a Higher-Order Functional LanguageDistinguished Paper
Research Papers
Neel KrishnaswamiComputer Laboratory, University of Cambridge, Michael ArntzeniusUniversity of Birmingham, UK
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Decomposition Diversity with Symmetric Data and Codata
Research Papers
David BinderUniversity of Tübingen, Julian JabsUniversity of Tübingen, Ingo SkupinUniversity of Tübingen, Klaus OstermannUniversity of Tübingen, Germany
Link to publication DOI Media Attached
12:30 - 14:00
Thursday LunchCatering at Lunch Room
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:05
Type SystemsResearch Papers at Ile de France II (IDF II)
Chair(s): Peter ThiemannUniversity of Freiburg, Germany
14:00
21m
Talk
Undecidability of D<: and Its Decidable FragmentsDistinguished Paper
Research Papers
Jason Z.S. HuMcGill University, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Decidable Subtyping for Path Dependent Types
Research Papers
Julian MackayVictoria University of Wellington, Alex PotaninVictoria University of Wellington, Jonathan AldrichCarnegie Mellon University, Lindsay GrovesVictoria University of Wellington
Link to publication DOI Media Attached
14:43
21m
Talk
Dependent Type Systems as Macros
Research Papers
Stephen ChangNortheastern University, Michael BallantynePLT @ Northeastern University, Milo TurnerPLT @ Northeastern University, William J. BowmanUniversity of British Columbia
Link to publication DOI Media Attached File Attached
14:00 - 15:05
Abstract InterpretationResearch Papers at Ile de France III (IDF III)
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris
14:00
21m
Talk
Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Research Papers
Roberto BruniUniversity of Pisa, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Roberta GoriUniversity of Pisa, Isabel Garcia-ContrerasIMDEA Software Institute, Dusko PavlovicUniversity of Hawaii
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Abstract Interpretation of Distributed Network Control Planes
Research Papers
Ryan BeckettMicrosoft Research, Aarti GuptaPrinceton University, Ratul MahajanUniversity of Washington, Intentionet, David WalkerPrinceton University
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Deterministic Parallel Fixpoint Computation
Research Papers
Sung Kook KimUniversity of California, Davis, Arnaud J. VenetFacebook, Aditya V. ThakurUniversity of California, Davis
Link to publication DOI Pre-print Media Attached File Attached
14:00 - 15:30
SRC Finalists PresentationsStudent Research Competition at St Jerome
14:00
90m
Talk
SRC Finalists Presentations
Student Research Competition
15:05 - 15:35
Thursday Afternoon BreakCatering at Break
15:35 - 16:40
Program LogicsResearch Papers at Ile de France II (IDF II)
Chair(s): Chung-Kil HurSeoul National University
15:35
21m
Talk
Deductive Verification with Ghost Monitors
Research Papers
Martin ClochardETH Zürich, Claude MarchéInria Saclay & Université Paris-Saclay, Andrei PaskevichLRI, Université Paris-Sud & CNRS
Link to publication DOI Media Attached
15:56
21m
Talk
The Next 700 Relational Program Logics
Research Papers
Kenji MaillardInria Nantes & University of Chile, Cătălin HriţcuInria Paris, Exequiel RivasInria Paris, Antoine Van MuylderInria Paris and Paris 7
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Incorrectness Logic
Research Papers
Link to publication DOI Media Attached
15:35 - 16:40
Probabilistic ProgrammingResearch Papers at Ile de France III (IDF III)
Chair(s): Ohad KammarUniversity of Edinburgh
15:35
21m
Talk
A Language for Probabilistically Oblivious Computation
Research Papers
David DaraisUniversity of Vermont, Ian SweetUniversity of Maryland, Chang LiuCitadel Securities, Michael HicksUniversity of Maryland
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
PλωNK: Functional Probabilistic NetKAT
Research Papers
Alexander VandenbrouckeKU Leuven, Belgium, Tom SchrijversKU Leuven
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Optimal Approximate Sampling From Discrete Probability Distributions
Research Papers
Feras A. SaadMassachusetts Institute of Technology, Cameron FreerMassachusetts Institute of Technology, Martin C. RinardMIT, Vikash K. MansinghkaMIT
Link to publication DOI Media Attached File Attached
16:50 - 18:00
Business Meeting & SRC AwardsResearch Papers at Ile de France II (IDF II)
16:50
70m
Meeting
Business Meeting & SRC Awards
Research Papers
Media Attached
18:00 - 19:00
Social Hour (Supported by Microsoft)Research Papers at Social Hour
18:00
60m
Social Event
Social Hour (Supported by Microsoft)
Research Papers
19:00 - 21:00
W@POPL DinnerW@POPL Dinner at Palace Cafe
19:00
2h
Dinner
W@POPL DinnerMentoring Event
W@POPL Dinner

Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change

07:45 - 09:00
Friday Mentoring BreakfastMentoring Breakfasts at Breakfast Room
07:45
75m
Social Event
Mentoring BreakfastMentoring Event
Mentoring Breakfasts
09:00 - 10:00
Invited TalkResearch Papers at Ile de France II (IDF II)
Chair(s): Lars BirkedalAarhus University
09:00
60m
Talk
Probabilistic ProgrammingInvited Talk
Research Papers
Media Attached File Attached
10:00 - 10:30
Friday Morning BreakCatering at Break
10:30 - 11:35
Verification in Proof AssistantsResearch Papers at Ile de France III (IDF III)
Chair(s): Sandrine BlazyUniv Rennes- IRISA
10:30
21m
Talk
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Research Papers
Mengqi LiuYale University, Lionel RiegVerimag, Zhong ShaoYale University, Ronghui GuColumbia University, David CostanzoYale University, Jung-Eun KimYale University, Man-Ki YoonYale University
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
The High-Level Benefits of Low-Level Sandboxing
Research Papers
Michael SammlerMPI-SWS, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8
Link to publication DOI Media Attached
11:13
21m
Talk
Interaction Trees: Representing Recursive and Impure Programs in CoqDistinguished Paper
Research Papers
Li-yao XiaUniversity of Pennsylvania, Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Gregory MalechaBedRock Systems, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI Media Attached File Attached
11:45 - 12:30
Concurrent Programming & Session TypesResearch Papers at Ile de France II (IDF II)
Chair(s): Susmit SarkarUniversity of St. Andrews
11:45
22m
Talk
Label-Dependent Session Types
Research Papers
Peter ThiemannUniversity of Freiburg, Germany, Vasco T. VasconcelosUniversity of Lisbon, Portugal
Link to publication DOI Media Attached
12:07
22m
Talk
Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Research Papers
Federico AschieriTU Wien, Francesco A. GencoIHPST, Université Paris 1
Link to publication DOI Media Attached
11:45 - 12:30
Probabilistic Reasoning and VerificationResearch Papers at Ile de France III (IDF III)
Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA
11:45
22m
Talk
Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Research Papers
Peixin WangShanghai Jiao Tong University, Hongfei FuShanghai Jiao Tong University, Krishnendu ChatterjeeIST Austria, Yuxin DengEast China Normal University, Ming XuEast China Normal University
Link to publication DOI Media Attached
12:07
22m
Talk
Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
Research Papers
Marcel HarkRWTH Aachen University, Germany, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Jürgen GieslRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University
Link to publication DOI Media Attached File Attached
12:30 - 14:00
Friday LunchCatering at Lunch Room
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:05
Semantics of Probabilistic & Quantum ProgrammingResearch Papers at Ile de France II (IDF II)
Chair(s): Alexandra SilvaUniversity College London
14:00
21m
Talk
Full Abstraction for the Quantum Lambda-Calculus
Research Papers
Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Relational Proofs for Quantum Programs
Research Papers
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun YuUniversity of Technology Sydney, Australia, Li ZhouMax Planck Institute for Security and Privacy/Tsinghua University
Link to publication DOI Pre-print Media Attached File Attached
14:43
21m
Talk
A Probabilistic Separation Logic
Research Papers
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Kevin LiaoMax Planck Institute for Security and Privacy
Link to publication DOI Media Attached
14:00 - 15:05
Language DesignResearch Papers at Ile de France III (IDF III)
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
14:00
21m
Talk
Stacked Borrows: An Aliasing Model for Rust
Research Papers
Ralf JungMPI-SWS, Hoang-Hai DangMPI-SWS, Jeehoon KangKAIST, Derek DreyerMPI-SWS
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Executable Formal Semantics for the POSIX Shell
Research Papers
Michael GreenbergPomona College, Austin J. BlattPuppet Labs
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Disentanglement in Nested-Parallel Programs
Research Papers
Sam WestrickCarnegie Mellon University, Rohan YadavCarnegie Mellon University, Matthew FluetRochester Institute of Technology, Umut A. AcarCarnegie Mellon University
Link to publication DOI Media Attached File Attached
15:05 - 15:35
Friday Afternoon BreakCatering at Break
15:35 - 16:40
Verified & Secure CompilationResearch Papers at Ile de France III (IDF III)
Chair(s): Andrew AppelPrinceton
15:35
21m
Talk
Formal Verification of a Constant-Time Preserving C Compiler
Research Papers
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine BlazyUniv Rennes- IRISA, Benjamin GregoireINRIA, Rémi HutinIRISA / ENS Rennes, Vincent LaporteInria, David PichardieUniv Rennes, ENS Rennes, IRISA, Alix TrieuAarhus University
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Research Papers
Youngju SongSeoul National University, Minki ChoSeoul National University, Dongjoo KimSeoul National University, Yonghyun KimSeoul National University, South Korea, Jeehoon KangKAIST, Chung-Kil HurSeoul National University
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Research Papers
Timothy BourkeInria / École normale supérieure, Lélio BrunENS/Inria, Marc PouzetÉcole normale supérieure
Link to publication DOI Media Attached File Attached
16:40 - 17:40
Social Hour (Supported by Tezos)Research Papers at Social Hour
16:40
60m
Social Event
Social Hour (Supported by Tezos)
Research Papers

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00
Invited TalkCoqPL at Maurepas
Chair(s): Robbert KrebbersDelft University of Technology
09:00
60m
Talk
SMTCoq: Safe and efficient automation in Coq (Keynote)
CoqPL
Chantal KellerLRI, Université Paris-Sud
File Attached
09:00 - 10:00
Gradual CriteriaWGT at Orleans
Chair(s): Amal AhmedNortheastern University, USA
09:00
30m
Talk
Gradual Typing as if Types Mattered
WGT
Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile
Pre-print
09:30
30m
Talk
Fully Abstract from Static to Gradual
WGT
Koen JacobsKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Dominique DevrieseVrije Universiteit Brussel
Pre-print
10:00 - 10:30
Saturday Morning BreakCatering at Break
10:30 - 12:30
Contributed TalksCoqPL at Maurepas
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
10:30
30m
Talk
Deriving Instances with Dependent Types
CoqPL
Arthur Azevedo de AmorimCarnegie Mellon University, USA
File Attached
11:00
30m
Talk
The use of Coq for Common Criteria Evaluations
CoqPL
File Attached
11:30
30m
Talk
Verifying concurrent Go code in Coq with Goose
CoqPL
Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USA
Link to publication File Attached
12:00
30m
Talk
A Tutorial on Equations
CoqPL
Media Attached File Attached
10:30 - 12:30
Programming featuresWGT at Orleans
Chair(s): Giuseppe CastagnaCNRS - Université de Paris, France
10:30
30m
Talk
Gradual Algebraic Data Types
WGT
Michael GreenbergPomona College, Stefan MalewskiUniversity of Santiago de Chile, Éric TanterUniversity of Chile
Pre-print File Attached
11:00
30m
Talk
Gradual Typing for Extensibility by Rows
WGT
Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Pre-print
11:30
30m
Talk
Foreign Function Typing: Semantic Type Soundness for FFIs
WGT
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
Pre-print
12:00
30m
Talk
Space-Efficient Monotonic References
WGT
Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA
Pre-print
10:30 - 12:30
Foundations and timing channelsPriSC at Rosalie
Chair(s): Marco VassenaCISPA Helmholtz Center for Information Security
10:30
24m
Talk
Exorcising Spectres with Secure Compilers
PriSC
Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute
Media Attached File Attached
10:54
24m
Talk
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Carmine AbateInria Paris, Roberto BlancoInria, Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Deepak GargMax Planck Institute for Software Systems, Cătălin HriţcuInria Paris, Marco PatrignaniStanford University & CISPA , Éric TanterUniversity of Chile, Jérémy ThibaultInria Paris
Media Attached File Attached
11:18
24m
Talk
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan BayAarhus University, Aslan AskarovAarhus University
Media Attached File Attached
11:42
24m
Talk
Hermes: Implementing Cryptography without Side-channels
PriSC
Ken Friis LarsenDIKU, University of Copenhagen, Torben MogensenDIKU, University of Copenhagen, Michael Kirkedal ThomsenDIKU, University of Copenhagen
File Attached
12:06
24m
Talk
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes, David PichardieUniv Rennes, ENS Rennes, IRISA
Media Attached
12:30 - 14:00
Saturday LunchCatering at Lunch Room
12:30
90m
Lunch
Lunch
Catering
14:00 - 15:05
Invited TalkCoqPL at Maurepas
Chair(s): Yves BertotINRIA
14:00
60m
Talk
Autosubst 2: Mechanising binders in Coq (Keynote)
CoqPL
Kathrin StarkPrinceton University, USA
File Attached
14:00 - 15:05
CoercionsWGT at Orleans
Chair(s): Jeremy G. SiekIndiana University, USA
14:00
32m
Talk
Hypercoercions and a Framework for Equivalence of Cast Calculi
WGT
Kuang-Chen LuIndiana University Bloomington, Jeremy G. SiekIndiana University, USA, Andre KuhlenschmidtIndiana University
Pre-print
14:32
32m
Talk
Space-Efficient Gradual Typing in Coercion-Passing Style
WGT
Yuya TsudaKyoto University, Atsushi IgarashiKyoto University, Japan, Tomoya TabuchiKyoto University
Pre-print
14:00 - 15:05
New outlooks on secure compilationPriSC at Rosalie
Chair(s): Cristina CifuentesOracle Labs
14:00
24m
Talk
Exploits as Insecure Compilation
PriSC
Jennifer PaykinGalois, Inc., Eric MertensGalois, Inc., Mark TullsenGalois, Inc, Luke MaurerGalois, Inc, Benoit RazetGalois, Inc, Alexander BakstGalois, Inc, Scott MooreGalois, Inc
Pre-print Media Attached File Attached
14:24
24m
Talk
Universal Composability is Secure Compilation
PriSC
Marco PatrignaniStanford University & CISPA , Riad S. WahbyStanford University, USA, Robert KünnemannCISPA, Saarland University
Media Attached File Attached
14:48
8m
Talk
Short Talk: Automatically Eliminating Speculative Leaks With Blade
PriSC
Marco VassenaCISPA Helmholtz Center for Information Security, Klaus v. GleissenthallUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA
Media Attached File Attached
14:56
8m
Talk
Short Talk: Everparse
PriSC
Tahina RamananandroMicrosoft Research, n.n.
Media Attached
15:05 - 15:35
Saturday Afternoon BreakCatering at Break
15:35 - 17:45
Contributed Talks & Coq DevelopersCoqPL at Maurepas
Chair(s): Joseph TassarottiBoston College, Robbert KrebbersDelft University of Technology
15:35
30m
Talk
Towards Formally Verified Just-in-Time compilation
CoqPL
Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes- IRISA, David PichardieUniv Rennes, ENS Rennes, IRISA
File Attached
16:05
30m
Talk
A Coq Library of Undecidable Problems
CoqPL
Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA, Andrej DudenhefnerSaarland University, Edith HeiterSaarland University, Dominik KirstSaarland University, Fabian KunzeSaarland University, Gert SmolkaSaarland University, Simon SpiesSaarland University, Dominik WehrSaarland University, Universiteit van Amsterdam, Maximilian WuttkeSaarland University
Media Attached File Attached
16:35
15m
Break
Short break
CoqPL
16:50
45m
Demonstration
Session with the Coq Development Team
CoqPL
15:35 - 17:45
Analysis, verification, blameWGT at Orleans
Chair(s): Niki VazouIMDEA Software Institute
15:35
32m
Talk
Gradual Verification of Recursive Heap Data Structures
WGT
Jenna WiseCarnegie Mellon University, Johannes BaderFacebook, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Joshua SunshineCarnegie Mellon University
Pre-print
16:07
33m
Talk
Gradual Program Analysis
WGT
Samuel EstepLiberty University, Jenna WiseCarnegie Mellon University, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Johannes BaderFacebook, Joshua SunshineCarnegie Mellon University
Pre-print
16:40
10m
Break
Minibreak
WGT
16:50
30m
Talk
Blame tracking at higher fidelity
WGT
Jakub ZalewskiUniversity of Edinburgh, James McKinnaUniversity of Edinburgh, J. Garrett MorrisUniversity of Kansas, USA, Philip WadlerUniversity of Edinburgh, UK
Pre-print
17:20
25m
Day closing
Discussion on gradual typing and WGT21
WGT
15:35 - 17:45
Compartmentalization, memory safety, and isolationPriSC at Rosalie
Chair(s): Marco PatrignaniStanford University & CISPA , Jonathan ProtzenkoMicrosoft Research, Redmond
15:35
24m
Talk
Flexible Tag-based Policies for Compartmentalized C
PriSC
Sean AndersonPortland State University, Andrew TolmachPortland State University, CHR ChhakPortland State University
Media Attached File Attached
15:59
24m
Talk
Mechanized Reasoning about a Capability Machine
PriSC
Aina Linn GeorgesAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University
Media Attached
16:23
24m
Talk
Securing Interruptible Enclaves
PriSC
Matteo BusiUniversità di Pisa - Dipartimento di Informatica, Job Noormanimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Jo Van Bulckimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Letterio GallettaIMT School for Advanced Studies, Pierpaolo DeganoUniversità di Pisa - Dipartimento di Informatica, Jan Tobias Mühlbergimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Frank PiessensKU Leuven
Media Attached File Attached
16:47
10m
Break
Mini-break
PriSC
16:57
24m
Talk
WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
PriSC
Jay BosamiyaCarnegie Mellon University, Benjamin LimCarnegie Mellon University, Bryan ParnoCarnegie Mellon University
Media Attached File Attached
17:21
24m
Talk
Memory Safety Preservation for WebAssembly
PriSC
Marco VassenaCISPA Helmholtz Center for Information Security, Marco PatrignaniStanford University & CISPA
Link to publication Media Attached File Attached

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Room8:00309:003010:003011:003012:003013:003014:003015:003016:003017:0030
Babylon
Bacchus
Break
Conde
Endymion
Frontenac
Lunch Room
Maurepas
Muses
SHANGRI-LA
St Jerome

Sun 19 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Break
POPL Catering
Break
10:00 - 10:30
Lunch Room
POPL Catering
Lunch
12:30 - 14:00
Maurepas
PLanQC
Quantum CPOs
12:10 - 12:30
St Jerome
VMCAI
Mini Break
11:30 - 12:00
VMCAI
Mini Break
16:40 - 17:12

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Babylon
Bacchus
PADL
Opening
08:30 - 08:45
Conde
Endymion
Frontenac
PEPM
Opening
09:00 - 09:05
PEPM
Mini Break 1
11:30 - 11:45
PEPM
Mini Break 2
16:35 - 16:50
Lunch Room
POPL Catering
Lunch
12:30 - 14:00
Maurepas
Muses
SHANGRI-LA
St Jerome
VMCAI
Mini Break
11:30 - 12:00
VMCAI
Mini Break
16:40 - 17:12

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Bacchus
PADL
Closing
16:45 - 17:00
Frontenac
Ile de France III (IDF III)
PLMW
Opening
09:00 - 09:10
PLMW
Mini break
16:40 - 16:50
Lunch Room
POPL Catering
Lunch
12:30 - 14:00
Maurepas