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: Introduction and Invited TalksPLanQC at Maurepas
Chair(s): Robert RandUniversity of Maryland
09:00 - 09:30
Talk
Invited Talk: Quantum Computing for Programming Languages Researchers
PLanQC
I: Jennifer PaykinGalois, Inc.
Media Attached File Attached
09:30 - 10:00
Talk
Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper
PLanQC
I: Peter SelingerDalhousie University
Media Attached
09:00 - 10:00: Invited 1VMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
09:00 - 10:00
Talk
The Siren Song of Temporal Synthesis
VMCAI
Moshe VardiRice University
10:00 - 10:30: Sunday Morning BreakCatering at Break
10:00 - 10:30
Coffee break
Break
Catering
10:30 - 12:30: Invited Talks, Pulses, Errors and CategoriesPLanQC at Maurepas
Chair(s): Frank Fu
10:30 - 11:00
Talk
Invited Talk: Q# - Going Beyond Quantum Circuits
PLanQC
I: Bettina HeimMicrosoft
Media Attached
11:00 - 11:30
Talk
Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions
PLanQC
I: Fred ChongUniversity of Chicago
Media Attached File Attached
11:30 - 11:50
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 - 12:10
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 - 12:30
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 - 11:00
Talk
Witnessing Secure Compilation
VMCAI
Kedar NamjoshiBell Labs, Nokia, Lucas M. TabajaraRice University
11:00 - 11:30
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 - 12:00
Coffee break
Mini Break
VMCAI
12:00 - 12:30
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 - 14:00
Lunch
Lunch
Catering
14:00 - 15:05: Formal MethodsPLanQC at Maurepas
Chair(s): Dominique UnruhUniversity of Tartu
14:00 - 14:20
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 - 14:40
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 - 15:05
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 - 15:05
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 - 15:55
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 - 16:15
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 - 16:35
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 - 16:07
Talk
The Correctness of a Code Generator for a Functional Language
VMCAI
Nathanaël CourantINRIA, Antoine SereEcole Polytechnique, Natarajan ShankarSRI International, USA
16:07 - 16:40
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 - 17:12
Coffee break
Mini Break
VMCAI
17:12 - 17:45
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 - 17:10
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 - 17:30
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 - 17:50
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 - 08:45
Day opening
Opening
PADL
08:45 - 09:35
Talk
Invited Talk: Logical Engines for Cloud Configurations
PADL
I: Nikolaj BjørnerMicrosoft Research
09:35 - 10:00
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 - 10:00
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 - 10:00
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 - 10:00
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 - 09:05
Day opening
Opening
PEPM
Casper Bach PoulsenDelft University of Technology, Zhenjiang HuPeking University
09:05 - 10:00
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 - 10:00
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 - 10:00
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 - 10:00
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 - 10:00
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 - 12:30
Tutorial
[T6] Verifying Probabilistic Properties with Couplings
TutorialFest
Justin HsuUniversity of Wisconsin-Madison, USA
File Attached
10:30 - 12:00: Answer Set Programming SystemsPADL at Bacchus
Chair(s): Neng-Fa ZhouCUNY Brooklyn College and Graduate Center
10:30 - 10:55
Talk
AQuA: ASP-based Visual Question Answering
PADL
10:55 - 11:10
Short-paper
Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report
PADL
11:10 - 11:25
Short-paper
VRASP: A Virtual Reality Environment for Learning Answer Set Programming
PADL
Vinh The NguyenTexas Tech University, Yuanlin Zhang, Kwanghee Jung, Wanli Xing, Tommy DangTexas Tech University
11:25 - 12:00
Other
Panel: Programming with logic for the masses
PADL
Nikolaj BjørnerMicrosoft Research, Paul TarauUniversity of North Texas, Eduardo Blanco, Kinjal Basu, Farhad Shakerin, Gopal Gupta, Alex Brik, Jeffrey XuUCLA, Vinh The NguyenTexas Tech University, Yuanlin Zhang, Kwanghee Jung, Wanli Xing, Tommy DangTexas Tech University
10:30 - 12:30: Verified Quantum Computing (II)TutorialFest at Endymion
10:30 - 12:30
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 - 11:05
Talk
Dependently-Typed Multi-Stage Programming Revisited (invited talk)
PEPM
Atsushi IgarashiKyoto University, Japan
11:05 - 11:30
Research paper
High-Fidelity Metaprogramming with Separator Syntax Trees
PEPM
Rodin AarssenCWI, Netherlands, Tijs van der StormCWI & University of Groningen, Netherlands
DOI
11:30 - 11:45
Break
Mini Break 1
PEPM
11:45 - 12:10
Research paper
Module Generation without Regret
PEPM
Yuhi SatoUniversity of Tsukuba, Yukiyoshi KameyamaUniversity of Tsukuba, Japan, Takahisa WatanabeUniversity of Tsukuba, Japan
DOI
12:10 - 12:30
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 - 10:51
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 - 11:13
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 - 11:35
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 - 12:30
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 - 12:30
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 - 11:00
Research paper
A Systematic Approach to Abstract Interpretation of Program Transformations
VMCAI
Sven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz
Pre-print
11:00 - 11:30
Talk
Sharing Ghost Variables in a Collection of Abstract Domains
VMCAI
Marc ChevalierENS, CNRS, PSL University, INRIA, Jerome FeretINRIA Paris
11:30 - 12:00
Coffee break
Mini Break
VMCAI
12:00 - 12:30
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 - 12:07
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 - 12:30
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 - 14:00
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 - 13:55
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 - 14:20
Talk
RTMLton: An SML Runtime for Real-Time Systems
PADL
14:20 - 14:45
Talk
A Timed IO Monad
PADL
David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
14:45 - 15:00
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 - 15:05
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 - 15:05
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 - 15:00
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 - 14:21
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 - 14:43
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 - 15:05
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 - 15:05
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 - 15:05
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 - 14:32
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 - 15:05
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 - 15:55
Talk
Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming
PADL
Sheung Chi Chan, James CheneyUniversity of Edinburgh, UK
15:55 - 16:20
Talk
On Repairing Web Services Workflows
PADL
Thanh Hai Nguyen, Enrico PontelliNew Mexico State University, Tran Cao Son
16:20 - 17:00
Talk
Competitive Programming with PiCat
PADL
Neng-Fa ZhouCUNY Brooklyn College and Graduate Center
15:35 - 17:45: Closing SessionADSL at Conde
15:35 - 16:40
Talk
Programs Synthesis with Separation Logic
ADSL
Nadia PolikarpovaUniversity of California, San Diego
16:40 - 17:45
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 - 17:35
Tutorial
[T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models
TutorialFest
Konstantinos (Kostis) SagonasUppsala University, Sweden
15:35 - 17:45: Sessions 3 & 4PEPM at Frontenac
Chair(s): Jeremy YallopUniversity of Cambridge, UK, Atsushi IgarashiKyoto University, Japan
15:35 - 16:10
Talk
Frex: Free extensions for normalisation by evaluation (invited talk)
PEPM
Ohad KammarUniversity of Edinburgh
Media Attached
16:10 - 16:35
Research paper
Symbolic Bisimulation for Open and Parameterized System
PEPM
Zechen HouEast China Normal University, Eric MadelaineINRIA
DOI File Attached
16:35 - 16:50
Break
Mini Break 2
PEPM
16:50 - 17:25
Talk
Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited talk)
PEPM
17:25 - 17:45
Short-paper
An approach to generating text-based IDEs with syntax completion from syntax specification
PEPM
Isao SasanoShibaura Institute of Technology
DOI
15:35 - 16:40: Decidability and complexityCPP at Maurepas
Chair(s): Kathrin StarkPrinceton University, USA
15:35 - 15:56
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 - 16:18
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 - 16:40
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 - 17:35
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 - 17:35
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 - 16:07
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 - 16:40
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 - 17:12
Coffee break
Mini Break
VMCAI
17:12 - 17:45
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 - 17:12
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 - 17:34
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 - 17:56
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 - 09:10
Day opening
Opening
PLMW
Brigitte PientkaMcGill University
09:10 - 10:00
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 - 10:00
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 - 09:10
Day opening
Opening Plenary
HASE
09:10 - 10:10
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 - 09:30
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 - 10:00
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 - 12:30
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 - 10:51
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 - 11:13
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 - 11:35
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 - 12:30
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 - 11:00
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 - 11:30
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 - 12:00
Coffee break
Mini Break
VMCAI
12:00 - 12:30
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 - 12:07
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 - 12:30
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 - 14:00
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 - 14:00
Talk
Invited Talk: Relational Artificial Intelligence
PADL
Molham ArefRelational.ai
14:00 - 14:30
Talk
Invited Talk: Learning Interpretable Rules from Structured Data
PADL
Mayur NaikUniversity of Pennsylvania
14:30 - 15:00
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 - 15:05
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 - 14:21
Talk
Formalizing Determinacy of Concurrent Revisions
CPP
Roy OverbeekVrije Universiteit Amsterdam
DOI Pre-print Media Attached
14:21 - 14:43
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 - 15:05
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 - 14:15
Tutorial
Peer Skillshare
HASE
Sarah de HaasGoogle Research
14:00 - 15:05: CLAFI at St Claude
14:00 - 14:30
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 - 14:47
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 MansinghkaMIT, Michael CarbinMassachusetts Institute of Technology
File Attached
14:49 - 15:05
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 - 14:32
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 - 15:05
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 - 16:00
Talk
Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types
PADL
Philip WadlerUniversity of Edinburgh, UK
16:00 - 16:45
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 - 17:00
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 - 17:35
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 - 15:56
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 - 16:18
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 - 16:40
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 - 16:30
Meeting
Working Sessions II
HASE
Ben LaurieGoogle Research, Satnam SinghGoogle Research
16:30 - 17:45
Day closing
Closing Plenary
HASE
15:35 - 17:45: DLAFI at St Claude
15:35 - 16:05
Talk
Coinductive Trees for Exact Inference of Probabilistic Programs
LAFI
Alexander BagnallOhio University, Gordon StewartOhio University, Anindya BanerjeeIMDEA Software Institute
16:05 - 16:35
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 - 17:05
Talk
Density Functions of Statistical Probabilistic Programs
LAFI
Tom MattinsonUniversity of Oxford, C.-H. Luke OngUniversity of Oxford
17:05 - 17:35
Talk
Probabilistic Programming around Gaussian Processes
LAFI
17:35 - 17:45
Day closing
Closing
LAFI
15:35 - 17:45: Panel SessionVMCAI at St Jerome
Chair(s): Dirk BeyerLMU Munich
15:35 - 17:45
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 - 17:12
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 - 17:34
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 - 17:56
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 - 08:45
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 - 09:00
Day opening
Welcome + SIGPLAN Award Ceremony
Research Papers
Media Attached
10:00 - 10:30: Wednesday Morning BreakCatering at Break
10:30 - 11:35: Probabilistic ProgrammingResearch Papers at Ile de France II (IDF II)
Chair(s): Alexandra SilvaUniversity College London
10:30 - 10:51
Talk
Towards Verified Stochastic Variational Inference for Probabilistic Programs
Research Papers
Wonyeol LeeKAIST, Hangyeol YuKAIST, Xavier RivalINRIA/CNRS/ENS Paris, Hongseok YangKAIST
Link to publication DOI Media Attached
10:51 - 11:13
Talk
Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
Research Papers
Alexander K. LewMassachusetts Institute of Technology, USA, Marco Cusumano-TownerMIT-CSAIL, Benjamin ShermanMassachusetts Institute of Technology, USA, Michael CarbinMassachusetts Institute of Technology, Vikash MansinghkaMIT
Link to publication DOI Media Attached
11:13 - 11:35
Talk
Semantics of Higher-Order Probabilistic Programs with Conditioning
Research Papers
Fredrik DahlqvistUniversity College London, Dexter KozenCornell University
Link to publication DOI Media Attached File Attached
10:30 - 11:35: Complexity / Decision ProceduresResearch Papers at Ile de France III (IDF III)
Chair(s): Roopsha SamantaPurdue University
10:30 - 10:51
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 - 11:13
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 - 11:35
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 - 12:07
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 - 12:30
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 - 12:07
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 - 12:30
Talk
Synthesizing Replacement Classes
Research Papers
Malavika SamakCSAIL, MIT, Deokhwan KimCSAIL, MIT, Martin RinardMIT
Link to publication DOI Media Attached File Attached
12:30 - 14:00: LGBTQ LunchLGBTQ Lunch at Endymion
12:30 - 14:00
Lunch
LGBTQ LunchMentoring Event
LGBTQ Lunch
12:30 - 14:00: Wednesday LunchCatering at Lunch Room
12:30 - 14:00
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 - 14:21
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 - 14:43
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 - 15:05
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 - 14:21
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 - 14:43
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 - 15:05
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 - 15:56
Talk
A Simple Differentiable Programming Language
Research Papers
Link to publication DOI Media Attached
15:56 - 16:18
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 - 16:40
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 - 15:56
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 - 16:18
Talk
Reductions for Safety Proofs
Research Papers
Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto
Link to publication DOI Media Attached
16:18 - 16:40
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 - 17:12
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 - 17:35
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 - 19:00
Poster
SRC Poster Session
Student Research Competition
17:35 - 18:35: Social Hour (Supported by Facebook)Research Papers at Social Hour
17:35 - 18:35
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 - 09:00
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 - 10:51
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 - 11:13
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 - 11:35
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 - 12:07
Talk
Fast, Sound, and Effectively Complete Dynamic Race Prediction
Research Papers
Andreas PavlogiannisAarhus University
Link to publication DOI Media Attached File Attached
12:07 - 12:30
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 - 12:07
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 - 12:30
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 - 14:00
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 - 14:21
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 - 14:43
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 - 15:05
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 - 14:21
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 - 14:43
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 - 15:05
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 - 15:30
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 - 15:56
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 - 16:18
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 - 16:40
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 - 15:56
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 - 16:18
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 - 16:40
Talk
Optimal Approximate Sampling From Discrete Probability Distributions
Research Papers
Feras SaadMassachusetts Institute of Technology, Cameron FreerMassachusetts Institute of Technology, Martin RinardMIT, Vikash 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 - 18:00
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 - 19:00
Social Event
Social Hour (Supported by Microsoft)
Research Papers
19:00 - 21:00: W@POPL DinnerW@POPL Dinner at Palace Cafe
19:00 - 21:00
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 - 09:00
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 - 10:00
Talk
Probabilistic ProgrammingInvited Talk
Research Papers
Media Attached File Attached
10:00 - 10:30: Friday Morning BreakCatering at Break
10:30 - 11:35: Type SystemsResearch Papers at Ile de France II (IDF II)
Chair(s): Dominique DevrieseVrije Universiteit Brussel
10:30 - 10:51
Talk
Kind Inference for DatatypesDistinguished Paper
Research Papers
Ningning XieThe University of Hong Kong, Richard A. EisenbergBryn Mawr College, USA, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong
Link to publication DOI Media Attached
10:51 - 11:13
Talk
Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc
Research Papers
Mark JonesPortland State University, J. Garrett MorrisUniversity of Kansas, USA, Richard A. EisenbergBryn Mawr College, USA
Link to publication DOI Media Attached File Attached
11:13 - 11:35
Talk
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Research Papers
Roland MeyerTU Braunschweig, Sebastian WolffTU Braunschweig
Link to publication DOI Media Attached File Attached
10:30 - 11:35: Verification in Proof AssistantsResearch Papers at Ile de France III (IDF III)
Chair(s): Sandrine BlazyUniv Rennes- IRISA
10:30 - 10:51
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 - 11:13
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 - 11:35
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 - 12:07
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 - 12:30
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 - 12:07
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 - 12:30
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 - 14:00
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 - 14:21
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 - 14:43
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 - 15:05
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 - 14:21
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 - 14:43
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 - 15:05
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: Semantics & Type TheoryResearch Papers at Ile de France II (IDF II)
Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA
15:35 - 15:56
Talk
Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper
Research Papers
Davide BarbarossaUniversité Paris 13, Giulio ManzonettoUniversité Paris 13
Link to publication DOI Media Attached File Attached
15:56 - 16:18
Talk
Reduction Monads and Their Signatures
Research Papers
Benedikt AhrensUniversity of Birmingham, United Kingdom, André HirschowitzUniversité Côte d'Azur, Ambroise LafontInria, France, Marco MaggesiUniversità di Firenze
Link to publication DOI Media Attached
16:18 - 16:40
Talk
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Research Papers
Matthieu SozeauInria, Simon BoulierInria, Yannick ForsterSaarland University, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Media Attached File Attached
15:35 - 16:40: Verified & Secure CompilationResearch Papers at Ile de France III (IDF III)
Chair(s): Andrew AppelPrinceton
15:35 - 15:56
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 - 16:18
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 - 16:40
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 - 17:40
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 - 10:00
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 - 09:30
Talk
Gradual Typing as if Types Mattered
WGT
Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile
Pre-print
09:30 - 10:00
Talk
Fully Abstract from Static to Gradual
WGT
Koen JacobsKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Dominique DevrieseVrije Universiteit Brussel
Pre-print
09:00 - 10:00: KeynotePriSC at Rosalie
09:00 - 09:05
Day opening
PriSC Introduction
PriSC
Dominique DevrieseVrije Universiteit Brussel
File Attached
09:05 - 10:00
Industry talk
Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
PriSC
Media Attached
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 - 11:00
Talk
Deriving Instances with Dependent Types
CoqPL
Arthur Azevedo de AmorimCarnegie Mellon University, USA
File Attached
11:00 - 11:30
Talk
The use of Coq for Common Criteria Evaluations
CoqPL
File Attached
11:30 - 12:00
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 - 12:30
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 - 11:00
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 - 11:30
Talk
Gradual Typing for Extensibility by Rows
WGT
Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Pre-print
11:30 - 12:00
Talk
Foreign Function Typing: Semantic Type Soundness for FFIs
WGT
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
Pre-print
12:00 - 12:30
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 - 10:54
Talk
Exorcising Spectres with Secure Compilers
PriSC
Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute
Media Attached File Attached
10:54 - 11:18
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 - 11:42
Talk
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan BayAarhus University, Aslan AskarovAarhus University
Media Attached File Attached
11:42 - 12:06
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
12:06 - 12:30
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 - 14:00
Lunch
Lunch
Catering
14:00 - 15:05: Invited TalkCoqPL at Maurepas
Chair(s): Yves BertotINRIA
14:00 - 15:00
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 - 14:32
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 - 15:05
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 - 14:24
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 - 14:48
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 - 14:56
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 - 15:04
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 - 16:05
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 - 16:35
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 - 16:50
Break
Short break
CoqPL
16:50 - 17:35
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 - 16:07
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 - 16:40
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 - 16:50
Break
Minibreak
WGT
16:50 - 17:20
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 - 17:45
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 - 15:59
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 - 16:23
Talk
Mechanized Reasoning about a Capability Machine
PriSC
Aina Linn GeorgesAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University
Media Attached
16:23 - 16:47
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 - 16:57
Break
Mini-break
PriSC
16:57 - 17:21
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 - 17:45
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:00