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

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Introduction and Invited TalksPLanQC at Maurepas
Chair(s): Robert Rand University of Maryland
09:00
30m
Talk
Invited Talk: Quantum Computing for Programming Languages Researchers
PLanQC
I: Jennifer Paykin Galois, Inc.
Media Attached File Attached
09:30
30m
Talk
Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper
PLanQC
I: Peter Selinger Dalhousie University
Media Attached
09:00 - 10:00
Invited 1VMCAI at St Jerome
Chair(s): Dirk Beyer LMU Munich
09:00
60m
Talk
The Siren Song of Temporal Synthesis
VMCAI
Moshe Vardi Rice 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 Heim Microsoft
Media Attached
11:00
30m
Talk
Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions
PLanQC
I: Frederic T. Chong University of Chicago
Media Attached File Attached
11:30
20m
Talk
Tuning up entanglement through the cloud using Qiskit-OpenPulse
PLanQC
Thomas Alexander IBM T.J. Watson Research Center, New York, USA, Naoki Kanazawa IBM Research, Tokyo, Japan, Daniel Egger IBM Research, Zurich, Switzerland, Ali Javadi-Abhari IBM T.J. Watson Research Center, New York, USA, David C. McKay IBM T.J. Watson Research Center, New York, USA
11:50
20m
Talk
Tracking Errors through Types in Quantum Programs
PLanQC
Kesha Hietala University of Maryland, Robert Rand University of Maryland, Michael Hicks University of Maryland
Pre-print Media Attached File Attached
12:10
20m
Talk
Quantum CPOs
PLanQC
Andre Kornell Tulane University, Bert Lindenhovius Tulane University, Michael Mislove Tulane
10:30 - 12:30
Papers 1VMCAI at St Jerome
Chair(s): Natasha Sharygina USI Lugano, Switzerland
10:30
30m
Talk
Witnessing Secure Compilation
VMCAI
Kedar Namjoshi Bell Labs, Nokia, Lucas M. Tabajara Rice University
11:00
30m
Talk
BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results
VMCAI
Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Luca Olivieri JuliaSoft SRL, Fausto Spoto U. Verona
11:30
30m
Coffee break
Mini Break
VMCAI

12:00
30m
Talk
Fixing Code That Explodes Under Symbolic Evaluation
VMCAI
Sorawee Porncharoenwase University of Washington, James Bornholt University of Texas at Austin, Emina Torlak University 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 Unruh University of Tartu
14:00
20m
Talk
Runtime Analysis of Quantum Programs: A Formal Approach
PLanQC
Federico Olmedo University of Chile & IMFD Chile, Alejandro Díaz-Caro ICC (UBA-CONICET) & UNQ
Pre-print File Attached
14:20
20m
Talk
Qbricks: formal verification in quantum computing
PLanQC
Christopĥe Chareton CEA, LIST, France, Sébastien Bardin CEA LIST, François Bobot CEA, Valentin Perrelle CEA, LIST, France, Benoit Valiron LRI, 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 Hietala University of Maryland, Kartik Singhal University of Chicago, Robert Rand University of Maryland, Shih-Han Hung University of Maryland, Xiaodi Wu University of Maryland, College Park, Michael Hicks University of Maryland
Media Attached
14:00 - 15:05
Invited 2VMCAI at St Jerome
Chair(s): Damien Zufferey MPI-SWS
14:00
65m
Talk
Safety and Robustness for Deep Learning with Provable Guarantees
VMCAI
Marta Kwiatkowska University of Oxford
15:05 - 15:35
Sunday Afternoon BreakCatering at Break
15:35 - 16:35
NISQPLanQC at Maurepas
Chair(s): Will Zeng Unitary Fund
15:35
20m
Talk
Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation
PLanQC
Andrew N. Glaudell University of Maryland, Neil Julien Ross Dalhousie University, Jacob M. Taylor University 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 Zhang University of Science and Technology of China, Haowei Deng University of Science and Technology of China, Quanxi Li University 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 Fu Institute for Quantum Information & State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Jintao Yu State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou, China, Xing Su College of Meteorology and Oceanography, National University of Defense Technology, Changsha, China, Hanru Jiang Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Hua Wu Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China, Dong Chen Department of Computing Science, College of Computer, National University of Defense Technology, Changsha, China, Fucheng Cheng Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Xi Deng Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Jinrong Zhang Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Lei Jin School of Information Engineering, Zhengzhou University, Zhengzhou, China, Yihang Yang School of Information Engineering, Zhengzhou University, Zhengzhou, China, Le Xu School of Information Engineering, Zhengzhou University, Zhengzhou, China, Chunchao Hu School of Information Engineering, Zhengzhou University, Zhengzhou, China, Anqi Huang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Guangyao Huang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Xiaogang Qiang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Mingtang Deng Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Ping Xu Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Wanwei Liu National University of Defense Technology, Yuxin Deng East China Normal University, Junjie Wu Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Yuan Feng Centre for Quantum Software and Information, University of Technology Sydney, Australia
File Attached
15:35 - 17:45
Papers 2VMCAI at St Jerome
Chair(s): Kedar Namjoshi Bell Labs, Nokia
15:35
32m
Talk
The Correctness of a Code Generator for a Functional Language
VMCAI
Nathanaël Courant INRIA, Antoine Sere Ecole Polytechnique, Natarajan Shankar SRI International, USA
16:07
32m
Talk
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
VMCAI
Jack Garzella University of Utah, Marek S. Baranowski University of Utah, Shaobo He University of Utah, Zvonimir Rakamaric University 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-Shalom Tel Aviv University, Israel, Shachar Itzhaky Technion, Israel, Noam Rinetzky Tel Aviv University, Sharon Shoham Tel Aviv university
16:50 - 17:50
Quantum-Classical CommunicationPLanQC at Maurepas
Chair(s): Michael Hicks University of Maryland
16:50
20m
Talk
Extending Modern C++ for Heterogeneous Quantum-Classical Computing
PLanQC
Alexander McCaskey Oak Ridge National Laboratory, Tiffany Mintz Oak Ridge National Laboratory, Eugene Dumitrescu Oak Ridge National Laboratory, Sarah Powers Oak Ridge National Laboratory, Shirley Moore Oak Ridge National Laboratory, Pavel Lougovski Oak Ridge National Laboratory
17:10
20m
Talk
Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control
PLanQC
Dongho LEE LRI / CEA LIST, Univ Paris Saclay, Sébastien Bardin CEA LIST, Valentin Perrelle CEA, LIST, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay
File Attached
17:30
20m
Talk
Automated distribution of quantum circuits via hypergraph partitioning
PLanQC
Pablo Andres-Martinez University of Edinburgh, Chris Heunen University of Edinburgh
Link to publication DOI Pre-print Media Attached File Attached

Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

08:30 - 10:00
Logical Engines and ApplicationsPADL at Bacchus
Chair(s): Ekaterina Komendantskaya Heriot-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ørner Microsoft Research
09:35
25m
Talk
Interactive Text Graph Mining with a Prolog-based Dialog Engine
PADL
Paul Tarau University 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 Hsu University 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 Krebbers Delft 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 Rand University of Maryland
Pre-print
09:00 - 10:00
Opening & Keynote Talk 1PEPM at Frontenac
Chair(s): Casper Bach Poulsen Delft University of Technology, Zhenjiang Hu Peking University
09:00
5m
Day opening
Opening
PEPM
Casper Bach Poulsen Delft University of Technology, Zhenjiang Hu Peking University
09:05
55m
Talk
Network Verification: Past, Present, and Future
PEPM
Nate Foster Cornell University
09:00 - 10:00
Invited talkCPP at Maurepas
Chair(s): Cătălin Hriţcu Inria Paris
09:00
60m
Talk
Invited talk: Matching Logic: The Foundation of the K Framework
CPP
Grigore Roşu University of Illinois at Urbana-Champaign, Xiaohong Chen University 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 Dinella University of Pennsylvania, Pardis Pashakhanloo University of Pennsylvania, Anthony Canino , Mayur Naik University 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 Polikarpova University of California, San Diego
Link to publication File Attached
09:00 - 10:00
Invited 3VMCAI at St Jerome
Chair(s): Damien Zufferey MPI-SWS
09:00
60m
Talk
Model Checking for Safe Autonomy
VMCAI
Rajeev Alur University 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 Hsu University of Wisconsin-Madison, USA
File Attached
10:30 - 12:00
Answer Set Programming SystemsPADL at Bacchus
Chair(s): Neng-Fa Zhou CUNY Brooklyn College and Graduate Center
10:30
25m
Talk
AQuA: ASP-based Visual Question Answering
PADL
10:55
15m
Short-paper
Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report
PADL
11:10
15m
Short-paper
VRASP: A Virtual Reality Environment for Learning Answer Set Programming
PADL
Vinh The Nguyen Texas Tech University, Yuanlin Zhang , Kwanghee Jung , Wanli Xing , Tommy Dang Texas Tech University
11:25
35m
Other
Panel: Programming with logic for the masses
PADL
Nikolaj Bjørner Microsoft Research, Paul Tarau University of North Texas, Eduardo Blanco , Kinjal Basu , Farhad Shakerin , Gopal Gupta , Alex Brik , Jeffrey Xu UCLA, Vinh The Nguyen Texas Tech University, Yuanlin Zhang , Kwanghee Jung , Wanli Xing , Tommy Dang Texas Tech University
10:30 - 12:30
Verified Quantum Computing (II)TutorialFest at Endymion
10:30
2h
Tutorial
[T2] Verified Quantum Computing
TutorialFest
Robert Rand University of Maryland
Pre-print
10:30 - 12:30
Sessions 1 & 2PEPM at Frontenac
Chair(s): Ohad Kammar University of Edinburgh, Walid Taha
10:30
35m
Talk
Dependently-Typed Multi-Stage Programming Revisited (invited talk)
PEPM
Atsushi Igarashi Kyoto University, Japan
11:05
25m
Research paper
High-Fidelity Metaprogramming with Separator Syntax Trees
PEPM
Rodin Aarssen CWI, Netherlands, Tijs van der Storm CWI & University of Groningen, Netherlands
DOI
11:30
15m
Break
Mini Break 1
PEPM

11:45
25m
Research paper
Module Generation without Regret
PEPM
Yuhi Sato University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba, Japan, Takahisa Watanabe University of Tsukuba, Japan
DOI
12:10
20m
Short-paper
GOOL: A Generic Object-Oriented Language
PEPM
Jacques Carette McMaster University, Brooks MacLachlan McMaster University, Spencer Smith McMaster University, Computing and Software Department
DOI Pre-print File Attached
10:30 - 11:35
Program verificationCPP at Maurepas
Chair(s): Nikhil Swamy Microsoft Research
10:30
21m
Talk
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
CPP
Clément Blaudeau Ecole Polytechnique, Natarajan Shankar SRI International, USA
DOI Pre-print Media Attached
10:51
22m
Talk
Proof Pearl: Braun Trees
CPP
Tobias Nipkow Technische Universität München, Thomas Sewell Chalmers University of Technology, Sweden
DOI Pre-print Media Attached
11:13
22m
Talk
FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP
Thomas Letan ANSSI, Yann Régis-Gianas IRIF, 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 Dinella University of Pennsylvania, Pardis Pashakhanloo University of Pennsylvania, Anthony Canino , Mayur Naik University 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 Polikarpova University of California, San Diego
Link to publication File Attached
10:30 - 12:30
Papers 3VMCAI at St Jerome
Chair(s): Dirk Beyer LMU Munich
10:30
30m
Research paper
A Systematic Approach to Abstract Interpretation of Program Transformations
VMCAI
Sven Keidel JGU Mainz, Sebastian Erdweg JGU Mainz
Pre-print
11:00
30m
Talk
Sharing Ghost Variables in a Collection of Abstract Domains
VMCAI
Marc Chevalier ENS, CNRS, PSL University, INRIA, Jerome Feret INRIA 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-Shalom Tel Aviv University, Israel, Shachar Itzhaky Technion, Israel, Roman Manevich Mellanox Technologies, Noam Rinetzky Tel Aviv University
11:45 - 12:30
Automated verification and SAT solvingCPP at Maurepas
Chair(s): Ori Lahav Tel Aviv University
11:45
22m
Talk
Verifying x86 Instruction Implementations
CPP
Shilpi Goel Centaur Technology, Inc., Anna Slobodova Centaur Technology, Inc., Rob Sumners Centaur Technology, Inc., Sol Swords Centaur 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 Hughes Chalmers 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 Elsman University 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 Janin Bordeaux INP / CNRS LaBRI / Bordeaux University
14:45
15m
Other
Panel: Memory and real-time programming in practice
PADL
Martin Elsman University of Copenhagen, Denmark, Niels Hallenberg , Bhargav Shivkumar , Jeffrey Murphy , Lukasz Ziarek SUNY Buffalo, USA, David Janin Bordeaux 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 Berdine Facebook
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) Sagonas Uppsala University, Sweden
14:00 - 15:05
Keynote Talk 2PEPM at Frontenac
Chair(s): Casper Bach Poulsen Delft University of Technology
14:00
60m
Talk
Reasoning about Progress of Concurrent Objects
PEPM
Xinyu Feng Nanjing University
14:00 - 15:05
Proof engineering and user interactionCPP at Maurepas
Chair(s): Yves Bertot INRIA
14:00
21m
Talk
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
CPP
Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Steve Zdancewic University 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 Wang University of Innsbruck, Chad Brown Czech Technical University in Prague, Cezary Kaliszyk University of Innsbruck, Josef Urban Czech Technical University in Prague
DOI Pre-print
14:43
21m
Talk
REPLICA: REPL Instrumentation for Coq Analysis
CPP
Talia Ringer University of Washington, Alex Sanchez-Stern University of California, San Diego, Dan Grossman University of Washington, Sorin Lerner University 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 Dreyer MPI-SWS, Robbert Krebbers Delft University of Technology, Amin Timany imec-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 Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London
File Attached
14:00 - 15:05
Papers 4VMCAI at St Jerome
Chair(s): Ruzica Piskac Yale University, USA
14:00
32m
Talk
Synthesizing Environment Invariants for Modular Hardware Verification
VMCAI
Hongce Zhang Princeton University, Weikun Yang Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University, Sharad Malik Princeton University
14:32
32m
Talk
Systematic Classification of Attackers via Bounded Model Checking
VMCAI
Eric Rothstein-Morris Singapore University of Technology and Design, Jun Sun Singapore Management University, Singapore, Sudipta Chattopadhyay Singapore 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 Cheney University of Edinburgh, UK
15:55
25m
Talk
On Repairing Web Services Workflows
PADL
Thanh Hai Nguyen , Enrico Pontelli New Mexico State University, Tran Cao Son
16:20
40m
Talk
Competitive Programming with PiCat
PADL
Neng-Fa Zhou CUNY Brooklyn College and Graduate Center
15:35 - 17:45
Closing SessionADSL at Conde
15:35
65m
Talk
Programs Synthesis with Separation Logic
ADSL
Nadia Polikarpova University of California, San Diego
16:40
65m
Talk
Local Reasoning for Global Graph Properties
ADSL
Thomas Wies New 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) Sagonas Uppsala University, Sweden
15:35 - 16:40
Decidability and complexityCPP at Maurepas
Chair(s): Kathrin Stark Princeton University, USA
15:35
21m
Talk
Verified Programming of Turing Machines in Coq
CPP
Yannick Forster Saarland University, Fabian Kunze Saarland University, Maximilian Wuttke Saarland University
DOI Pre-print Media Attached
15:56
21m
Talk
A Functional Proof Pearl: Inverting the Ackermann Hierarchy
CPP
Linh Tran National University of Singapore, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of Singapore
DOI Pre-print Media Attached
16:18
21m
Talk
Undecidability of Higher-Order Unification Formalised in Coq
CPP
Simon Spies Saarland University, Yannick Forster Saarland 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 Dreyer MPI-SWS, Robbert Krebbers Delft University of Technology, Amin Timany imec-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 Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London
File Attached
15:35 - 17:45
Papers 5VMCAI at St Jerome
Chair(s): Nikolaj Bjørner Microsoft Research
15:35
32m
Talk
Cheap CTL Compassion in NuSMV
VMCAI
Daniel Hausmann Friedrich-Alexander-Universität Erlangen-Nürnberg, Tadeusz Litak FAU Erlangen-Nuremberg, INF 8, Christoph Rauch FAU Erlangen-Nürnberg, Lehrstuhl 8, Matthias Zinner FAU Erlangen-Nürnberg
16:07
32m
Talk
A Cooperative Parallelization Approach for Property-Directed k-Induction
VMCAI
Martin Blicha Università della Svizzera italiana, Antti Hyvärinen Università della Svizzera Italiana, Matteo Marescotti Università della Svizzera Italiana, Natasha Sharygina USI Lugano, Switzerland
16:40
32m
Coffee break
Mini Break
VMCAI

17:12
32m
Talk
Generalized Property-Directed Reachability for Hybrid Systems
VMCAI
Kohei Suenaga Graduate School of Informatics, Kyoto University, Takuya Ishizawa Kyoto University
Link to publication Pre-print
16:50 - 17:56
Homotopy Type Theory and PC chairs' reportCPP at Maurepas
Chair(s): Floris van Doorn University of Pittsburgh
16:50
22m
Talk
Cubical Synthetic Homotopy Theory
CPP
Anders Mörtberg Department of Mathematics, Stockholm University, Loïc Pujet Gallinette 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 Forsberg University of Strathclyde, Chuangjie Xu Ludwig-Maximilians-Universität München, Neil Ghani University of Strathclyde
DOI Pre-print Media Attached File Attached
17:34
22m
Talk
PC Chairs' report
CPP
Jasmin Blanchette Vrije Universiteit Amsterdam, Cătălin Hriţcu Inria Paris
DOI Media Attached File Attached

Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Morning 1PLMW at Ile de France III (IDF III)
Chair(s): Stephanie Balzer Carnegie Mellon University, USA
09:00
10m
Day opening
Opening
PLMW
Brigitte Pientka McGill University
09:10
50m
Talk
How to Write Papers So People Can Read ThemMentoring Event
PLMW
Derek Dreyer MPI-SWS
File Attached
09:00 - 10:00
Invited talkCPP at Maurepas
Chair(s): Jasmin Blanchette Vrije Universiteit Amsterdam
09:00
60m
Talk
Invited talk: Proof Assistants at the Hardware-Software Interface
CPP
Adam Chlipala Massachusetts 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'Hearn Facebook, Philippa Gardner Imperial College London, Muralidaran Vijayaraghavan SiFive, Peter Sewell University of Cambridge
09:00 - 10:00
Papers 6VMCAI at St Jerome
Chair(s): Andreas Podelski University of Freiburg, Germany
09:00
30m
Talk
How to Win First-Order Safety Games
VMCAI
Helmut Seidl Technische Universität München, Christian Müller Technical University of Munich, Bernd Finkbeiner Saarland University
09:30
30m
Talk
Improving Parity Game Solvers with Justifications
VMCAI
Ruben Lapauw Katholieke Universiteit Leuven, Maurice Bruynooghe Katholieke Universiteit Leuven, Marc Denecker Katholieke 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. Pierce University of Pennsylvania
10:30
21m
Talk
Coq à la Carte - A Practical Approach to Modular Syntax with Binders
CPP
Yannick Forster Saarland University, Kathrin Stark Princeton University, USA
DOI Pre-print Media Attached
10:51
21m
Talk
A Mechanized Formalization of GraphQL
CPP
Tomás Díaz IMFD Chile, Federico Olmedo University of Chile & IMFD Chile, Éric Tanter University of Chile
DOI Pre-print Media Attached File Attached
11:13
21m
Talk
ConCert: A Smart Contract Certification Framework in Coq
CPP
Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Jakob Botsch Nielsen Concordium Blockchain Research Center, Aarhus University, Bas Spitters Concordium 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 Laurie Google Research, Hong-Seok Kim , Jonathan Protzenko Microsoft Research, Redmond
10:30 - 12:30
Papers 7VMCAI at St Jerome
Chair(s): Thomas Wies New York University
10:30
30m
Talk
Language Inclusion for Finite Prime Event Structures
VMCAI
Andreas Fellner AIT - Austrian Institute of Technology, Thorsten Tarrach Austrian Institute of Technology, Georg Weissenbacher Technische Universität Wien
11:00
30m
Talk
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
VMCAI
Swen Jacobs CISPA Helmholtz Center for Information Security, Mouhammad Sakr Saarland University, Martin Zimmermann University of Liverpool
11:30
30m
Coffee break
Mini Break
VMCAI

12:00
30m
Talk
Solving LIA* Using Approximations
VMCAI
Maxwell Levatich Yale, Nikolaj Bjørner Microsoft Research, Ruzica Piskac Yale University, USA, Sharon Shoham Tel Aviv university
11:45 - 12:30
Verified cryptographyCPP at Maurepas
Chair(s): Adam Chlipala Massachusetts Institute of Technology
11:45
22m
Talk
Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
CPP
David Butler Alan Turing Institute, David Aspinall University of Edinburgh, Adria Gascon Alan Turing Institute
DOI Pre-print Media Attached
12:07
22m
Talk
Verified Security of BLT Signature Scheme
CPP
Denis Firsov Guardtime AS, Ahto Buldas Tallinn University of Technology, Ahto Truu Guardtime AS, Risto Laanoja Guardtime 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): Konstantinos (Kostis) Sagonas Uppsala University, Sweden, David Warren Stony Brook University
13:30
30m
Talk
Invited Talk: Relational Artificial Intelligence
PADL
Molham Aref Relational.ai
14:00
30m
Talk
Invited Talk: Learning Interpretable Rules from Structured Data
PADL
Mayur Naik University of Pennsylvania
14:30
30m
Talk
Invited Talk: An Introduction to the Imandra Automated Reasoning System
PADL
Grant Passmore Imandra Inc.
14:00 - 15:05
Afternoon 1PLMW at Ile de France III (IDF III)
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
14:00
65m
Talk
PanelMentoring Event
PLMW
William J. Bowman University of British Columbia, Kenny Foner Galois, Andrew K. Hirsch Max Planck Institute for Software Systems, Taro Sekiyama National Institute of Informatics, Juliana Franco Microsoft Research, Cambridge, Hannah Gommerstadt Vassar College
Media Attached
14:00 - 15:05
Concurrency and linearityCPP at Maurepas
Chair(s): Zhong Shao Yale University
14:00
21m
Talk
Formalizing Determinacy of Concurrent Revisions
CPP
Roy Overbeek Vrije Universiteit Amsterdam
DOI Pre-print Media Attached
14:21
21m
Talk
Formalizing π-calculus in Guarded Cubical Agda
CPP
Niccolò Veltri Tallinn University of Technology, Andrea Vezzosi IT University Copenhagen
DOI Pre-print Media Attached File Attached
14:43
21m
Talk
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
CPP
Arjen Rouvoet Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Delft University of Technology, Eelco Visser Delft 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 Haas Google 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 Zhou University of Oxford, Hongseok Yang KAIST, Yee Whye Teh University of Oxford, Tom Rainforth Department of Statistics, University of Oxford
14:32
15m
Talk
MetaPPL: Inference Algorithms as First-Class Generative Models
LAFI
Alexander K. Lew Massachusetts Institute of Technology, USA, Benjamin Sherman Massachusetts Institute of Technology, USA, Marco Cusumano-Towner MIT-CSAIL, Austin Garrett MIT, Ben Zinberg MIT, Vikash K. Mansinghka MIT, Michael Carbin Massachusetts 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 Lahav Tel Aviv University
14:00
32m
Talk
Formalizing and Checking Multilevel Consistency
VMCAI
Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea IRIF, University Paris Diderot & CNRS, Madhavan Mukund Chennai Mathematical Institute, Gautham Shenoy R Chennai Mathematical Institute, S.P. Suresh Chennai Mathematical Institute
14:32
32m
Talk
Practical Abstractions for Automated Verification of Shared-Memory Concurrency
VMCAI
Wytse Oortwijn ETH Zürich, Dilian Gurov KTH Royal Institute of Technology, Marieke Huisman University 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 Liu Stony Brook University, Konstantinos (Kostis) Sagonas Uppsala University, Sweden, David Warren Stony Brook University
15:30
30m
Talk
Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types
PADL
Philip Wadler University of Edinburgh, UK
16:00
45m
Other
Panel: Experience and Direction
PADL
I: Molham Aref Relational.ai, I: Mayur Naik University of Pennsylvania, I: Grant Passmore Imandra Inc., I: Philip Wadler University of Edinburgh, UK
16:45
15m
Day closing
Closing
PADL
Ekaterina Komendantskaya Heriot-Watt University, UK, Y. Annie Liu Stony 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. Lewis Vrije Universiteit Amsterdam
15:35
21m
Talk
Formalising perfectoid spaces
CPP
Patrick Massot Université Paris Sud, Kevin Buzzard Imperial College London, Johan Commelin Universitä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 Singh Tata Institute of Fundamental Research Mumbai, Raja Natarajan Tata 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 Doczkal Université Côte d'Azur, Damien Pous CNRS, ENS Lyon
DOI Pre-print Media Attached
15:35 - 17:45
Afternoon SessionHASE at Orpheus
14:30
2h
Meeting
Working Sessions II
HASE
Ben Laurie Google Research, Satnam Singh Google 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 Bagnall Ohio University, Gordon Stewart Ohio University, Anindya Banerjee IMDEA Software Institute
16:05
30m
Talk
Name generation and Higher-order Probabilistic Programming (Or is new=rnd?)
LAFI
Dario Stein University of Oxford, Sam Staton University of Oxford, Michael Wolman McGill University
File Attached
16:35
30m
Talk
Density Functions of Statistical Probabilistic Programs
LAFI
Tom Mattinson University of Oxford, C.-H. Luke Ong University 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 Beyer LMU Munich
15:35
2h10m
Other
Panel "The Future of Software Verification" at VMCAI
VMCAI
Lenore Zuck UIC, Michael Whalen Amazon Web Services and the University of Minnesota, Natarajan Shankar SRI International, USA, Andreas Podelski University of Freiburg, Germany, Dirk Beyer LMU Munich
16:50 - 17:56
Formalized mathematics 2CPP at Maurepas
Chair(s): Tobias Nipkow Technische Universität München
16:50
22m
Talk
The Poincaré-Bendixson Theorem in Isabelle/HOL
CPP
Fabian Immler Carnegie Mellon University, Yong Kiam Tan Carnegie 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 Han University of Pittsburgh, Floris van Doorn University 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

Displayed 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): Lars Birkedal Aarhus University, Jens Palsberg University of California, Los Angeles, Brigitte Pientka McGill 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
Probabilistic ProgrammingResearch Papers at Ile de France II (IDF II)
Chair(s): Alexandra Silva University College London
10:30
21m
Talk
Towards Verified Stochastic Variational Inference for Probabilistic Programs
Research Papers
Wonyeol Lee KAIST, Hangyeol Yu KAIST, Xavier Rival INRIA/CNRS/ENS Paris, Hongseok Yang KAIST
Link to publication DOI Media Attached
10:51
21m
Talk
Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
Research Papers
Alexander K. Lew Massachusetts Institute of Technology, USA, Marco Cusumano-Towner MIT-CSAIL, Benjamin Sherman Massachusetts Institute of Technology, USA, Michael Carbin Massachusetts Institute of Technology, Vikash K. Mansinghka MIT
Link to publication DOI Media Attached
11:13
21m
Talk
Semantics of Higher-Order Probabilistic Programs with Conditioning
Research Papers
Fredrik Dahlqvist University College London, Dexter Kozen Cornell 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 Samanta Purdue University
10:30
21m
Talk
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
Research Papers
Yannick Forster Saarland University, Fabian Kunze Saarland University, Marc Roth Saarland 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. Feldman Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
Link to publication DOI Media Attached
11:13
21m
Talk
Parameterized Verification under TSO is PSPACE-Complete
Research Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Rojin Rezvan Sharif 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 Wies New York University
11:45
22m
Talk
Recurrence Extraction for Functional Programs through Call-by-Push-Value
Research Papers
Alex Kavvos Aarhus University, Edward Morehouse Wesleyan University, Daniel R. Licata Wesleyan University, Norman Danner Wesleyan 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 Handley University of Nottingham, Niki Vazou IMDEA Software Institute, Graham Hutton University 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 Lesani University of California, Riverside
11:45
22m
Talk
Program Synthesis by Type-Guided Abstraction Refinement
Research Papers
Zheng Guo University of California, San Diego, Michael B. James University of California, San Diego, David Justo University of California, San Diego, Jiaxiao Zhou University of California, San Diego, Ziteng Wang University of California, San Diego, Ranjit Jhala University of California, San Diego, Nadia Polikarpova University of California, San Diego
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Synthesizing Replacement Classes
Research Papers
Malavika Samak CSAIL, MIT, Deokhwan Kim CSAIL, MIT, Martin C. Rinard MIT
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 Raad MPI-SWS, Germany
14:00
21m
Talk
The Future is Ours: Prophecy Variables in Separation Logic
Research Papers
Ralf Jung MPI-SWS, Rodolphe Lepigre MPI-SWS, Gaurav Parthasarathy ETH Zurich, Marianna Rapoport University of Waterloo, Amin Timany imec-Distrinet KU-Leuven, Derek Dreyer MPI-SWS, Bart Jacobs imec-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 Vilhena Inria, François Pottier Inria, France, Jacques-Henri Jourdan CNRS, 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 Hinrichsen IT University of Copenhagen, Jesper Bengtson IT University of Copenhagen, Robbert Krebbers Delft 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. Siek Indiana University, USA
14:00
21m
Talk
What is Decidable about Gradual Types?
Research Papers
Zeina Migeed University of California, Los Angeles, Jens Palsberg University 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 S. New Northeastern University, Dustin Jamner Northeastern University, USA, Amal Ahmed Northeastern University, USA
Link to publication DOI Media Attached
14:43
21m
Talk
Does Blame Shifting Work?
Research Papers
Lukas Lazarek Northwestern University, Alexis King Northwestern University, Samanvitha Sundar Northwestern University, Robert Bruce Findler Northwestern University, USA, Christos Dimoulas PLT @ 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 Birkedal Aarhus 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 Brunel Deepomatic, Damiano Mazza CNRS, Michele Pagani IRIF - 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 Smolka Cornell University, Nate Foster Cornell University, Justin Hsu University of Wisconsin-Madison, USA, Tobias Kappé University College London, Dexter Kozen Cornell University, Alexandra Silva University 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 Sarkar University of St. Andrews
15:35
21m
Talk
Persistency Semantics of the Intel-x86 Architecture
Research Papers
Azalea Raad MPI-SWS, Germany, John Wickerson Imperial College London, Gil Neiger Intel Corporation, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Media Attached
15:56
21m
Talk
Reductions for Safety Proofs
Research Papers
Azadeh Farzan University of Toronto, Anthony Vandikas University of Toronto
Link to publication DOI Media Attached
16:18
21m
Talk
RustBelt Meets Relaxed Memory
Research Papers
Hoang-Hai Dang MPI-SWS, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Jan-Oliver Kaiser MPI-SWS, Derek Dreyer MPI-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 Samanta Purdue University
16:50
22m
Talk
Visualization by Example
Research Papers
Chenglong Wang University of Washington, USA, Yu Feng University of California, Santa Barbara, Rastislav Bodík University of Washington, Alvin Cheung University of California, Berkeley, Işıl Dillig University 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 Mathur University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign, Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University 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

Displayed 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 Lesani University of California, Riverside
10:30
21m
Talk
Synthesis of Coordination Programs from Linear Temporal Specifications
Research Papers
Suguman Bansal Rice University, USA, Kedar Namjoshi Bell Labs, Nokia, Yaniv Sa'ar Nokia 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 An Purdue University, Rishabh Singh Google Brain, Sasa Misailovic University of Illinois at Urbana-Champaign, Roopsha Samanta Purdue University
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Provenance-Guided Synthesis of Datalog Programs
Research Papers
Mukund Raghothaman University of Southern California, Jonathan Mendelson University of Pennsylvania, David Zhao The University of Sydney, Mayur Naik University of Pennsylvania, Bernhard Scholz University 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 Thiemann University of Freiburg, Germany
11:45
22m
Talk
Fast, Sound, and Effectively Complete Dynamic Race Prediction
Research Papers
Andreas Pavlogiannis Aarhus University
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Detecting Floating-Point Errors via Atomic Conditions
Research Papers
Daming Zou Peking University, Muhan Zeng Peking University, Yingfei Xiong Peking University, Zhoulai Fu IT University of Copenhagen, Denmark, Lu Zhang Peking University, Zhendong Su ETH 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 Pientka McGill University
11:45
22m
Talk
Seminaïve Evaluation for a Higher-Order Functional LanguageDistinguished Paper
Research Papers
Neel Krishnaswami Computer Laboratory, University of Cambridge, Michael Arntzenius University 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 Binder University of Tübingen, Julian Jabs University of Tübingen, Ingo Skupin University of Tübingen, Klaus Ostermann University 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 Thiemann University of Freiburg, Germany
14:00
21m
Talk
Undecidability of D<: and Its Decidable FragmentsDistinguished Paper
Research Papers
Jason Z.S. Hu McGill University, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Decidable Subtyping for Path Dependent Types
Research Papers
Julian Mackay Victoria University of Wellington, Alex Potanin Victoria University of Wellington, Jonathan Aldrich Carnegie Mellon University, Lindsay Groves Victoria University of Wellington
Link to publication DOI Media Attached
14:43
21m
Talk
Dependent Type Systems as Macros
Research Papers
Stephen Chang Northeastern University, Michael Ballantyne PLT @ Northeastern University, Milo Turner PLT @ Northeastern University, William J. Bowman University 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 Rival INRIA/CNRS/ENS Paris
14:00
21m
Talk
Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Research Papers
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona and IMDEA Software Institute, Roberta Gori University of Pisa, Isabel Garcia-Contreras IMDEA Software Institute, Dusko Pavlovic University of Hawaii
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Abstract Interpretation of Distributed Network Control Planes
Research Papers
Ryan Beckett Microsoft Research, Aarti Gupta Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker Princeton University
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Deterministic Parallel Fixpoint Computation
Research Papers
Sung Kook Kim University of California, Davis, Arnaud J. Venet Facebook, Aditya V. Thakur University 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 Hur Seoul National University
15:35
21m
Talk
Deductive Verification with Ghost Monitors
Research Papers
Martin Clochard ETH Zürich, Claude Marché Inria Saclay & Université Paris-Saclay, Andrei Paskevich LRI, Université Paris-Sud & CNRS
Link to publication DOI Media Attached
15:56
21m
Talk
The Next 700 Relational Program Logics
Research Papers
Kenji Maillard Inria Nantes & University of Chile, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Antoine Van Muylder Inria Paris and Paris 7
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Incorrectness Logic
Research Papers
Peter O'Hearn Facebook
Link to publication DOI Media Attached
15:35 - 16:40
Probabilistic ProgrammingResearch Papers at Ile de France III (IDF III)
Chair(s): Ohad Kammar University of Edinburgh
15:35
21m
Talk
A Language for Probabilistically Oblivious Computation
Research Papers
David Darais University of Vermont, Ian Sweet University of Maryland, Chang Liu Citadel Securities, Michael Hicks University of Maryland
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
PλωNK: Functional Probabilistic NetKAT
Research Papers
Alexander Vandenbroucke KU Leuven, Belgium, Tom Schrijvers KU Leuven
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Optimal Approximate Sampling From Discrete Probability Distributions
Research Papers
Feras Saad Massachusetts Institute of Technology, Cameron Freer Massachusetts Institute of Technology, Martin C. Rinard MIT, Vikash K. Mansinghka MIT
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

Displayed 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 Birkedal Aarhus 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
Type SystemsResearch Papers at Ile de France II (IDF II)
Chair(s): Dominique Devriese Vrije Universiteit Brussel
10:30
21m
Talk
Kind Inference for DatatypesDistinguished Paper
Research Papers
Ningning Xie The University of Hong Kong, Richard A. Eisenberg Bryn Mawr College, USA, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong
Link to publication DOI Media Attached
10:51
21m
Talk
Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc
Research Papers
Mark Jones Portland State University, J. Garrett Morris University of Kansas, USA, Richard A. Eisenberg Bryn Mawr College, USA
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Research Papers
Roland Meyer TU Braunschweig, Sebastian Wolff TU 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 Blazy Univ Rennes- IRISA
10:30
21m
Talk
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Research Papers
Mengqi Liu Yale University, Lionel Rieg Verimag, Zhong Shao Yale University, Ronghui Gu Columbia University, David Costanzo Yale University, Jung-Eun Kim Yale University, Man-Ki Yoon Yale University
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
The High-Level Benefits of Low-Level Sandboxing
Research Papers
Michael Sammler MPI-SWS, Deepak Garg Max Planck Institute for Software Systems, Derek Dreyer MPI-SWS, Tadeusz Litak FAU 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 Xia University of Pennsylvania, Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Gregory Malecha BedRock Systems, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University 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 Sarkar University of St. Andrews
11:45
22m
Talk
Label-Dependent Session Types
Research Papers
Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos University 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 Aschieri TU Wien, Francesco A. Genco IHPST, 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 Amorim Carnegie Mellon University, USA
11:45
22m
Talk
Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Research Papers
Peixin Wang Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Krishnendu Chatterjee IST Austria, Yuxin Deng East China Normal University, Ming Xu East 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 Hark RWTH Aachen University, Germany, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Jürgen Giesl RWTH Aachen University, Joost-Pieter Katoen RWTH 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 Silva University College London
14:00
21m
Talk
Full Abstraction for the Quantum Lambda-Calculus
Research Papers
Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Relational Proofs for Quantum Programs
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Mingsheng Ying University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun Yu University of Technology Sydney, Australia, Li Zhou Max 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 Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Kevin Liao Max 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 Timany imec-Distrinet KU-Leuven
14:00
21m
Talk
Stacked Borrows: An Aliasing Model for Rust
Research Papers
Ralf Jung MPI-SWS, Hoang-Hai Dang MPI-SWS, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Executable Formal Semantics for the POSIX Shell
Research Papers
Michael Greenberg Pomona College, Austin J. Blatt Puppet Labs
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Disentanglement in Nested-Parallel Programs
Research Papers
Sam Westrick Carnegie Mellon University, Rohan Yadav Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Umut A. Acar Carnegie 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 Amorim Carnegie Mellon University, USA
15:35
21m
Talk
Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper
Research Papers
Davide Barbarossa Université Paris 13, Giulio Manzonetto Université Paris 13
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
Reduction Monads and Their Signatures
Research Papers
Benedikt Ahrens University of Birmingham, United Kingdom, André Hirschowitz Université Côte d'Azur, Ambroise Lafont Inria, France, Marco Maggesi Università di Firenze
Link to publication DOI Media Attached
16:18
21m
Talk
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Research Papers
Matthieu Sozeau Inria, Simon Boulier Inria, Yannick Forster Saarland University, Nicolas Tabareau Inria, Theo Winterhalter Inria — 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 W. Appel Princeton
15:35
21m
Talk
Formal Verification of a Constant-Time Preserving C Compiler
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine Blazy Univ Rennes- IRISA, Benjamin Gregoire INRIA, Rémi Hutin IRISA / ENS Rennes, Vincent Laporte Inria, David Pichardie Univ Rennes, ENS Rennes, IRISA, Alix Trieu Aarhus 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 Song Seoul National University, Minki Cho Seoul National University, Dongjoo Kim Seoul National University, Yonghyun Kim Seoul National University, South Korea, Jeehoon Kang KAIST, Chung-Kil Hur Seoul 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 Bourke Inria / École normale supérieure, Lelio Brun ENS/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

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Invited TalkCoqPL at Maurepas
Chair(s): Robbert Krebbers Delft University of Technology
09:00
60m
Talk
SMTCoq: Safe and efficient automation in Coq (Keynote)
CoqPL
Chantal Keller LRI, Université Paris-Sud
File Attached
09:00 - 10:00
Gradual CriteriaWGT at Orleans
Chair(s): Amal Ahmed Northeastern University, USA
09:00
30m
Talk
Gradual Typing as if Types Mattered
WGT
Ronald Garcia University of British Columbia, Éric Tanter University of Chile
Pre-print
09:30
30m
Talk
Fully Abstract from Static to Gradual
WGT
Koen Jacobs KU Leuven, Amin Timany imec-Distrinet KU-Leuven, Dominique Devriese Vrije Universiteit Brussel
Pre-print
09:00 - 10:00
KeynotePriSC at Rosalie
09:00
5m
Day opening
PriSC Introduction
PriSC
Dominique Devriese Vrije Universiteit Brussel
File Attached
09:05
55m
Industry talk
Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
PriSC
K: Tyler McMullen Fastly
Media Attached
10:00 - 10:30
Saturday Morning BreakCatering at Break
10:30 - 12:30
Contributed TalksCoqPL at Maurepas
Chair(s): Amin Timany imec-Distrinet KU-Leuven
10:30
30m
Talk
Deriving Instances with Dependent Types
CoqPL
Arthur Azevedo de Amorim Carnegie 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 Chajed Massachusetts Institute of Technology, USA, Joseph Tassarotti Boston College, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts 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 Castagna CNRS - Université de Paris, France
10:30
30m
Talk
Gradual Algebraic Data Types
WGT
Michael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile
Pre-print File Attached
11:00
30m
Talk
Gradual Typing for Extensibility by Rows
WGT
Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Pre-print
11:30
30m
Talk
Foreign Function Typing: Semantic Type Soundness for FFIs
WGT
Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA
Pre-print
12:00
30m
Talk
Space-Efficient Monotonic References
WGT
Deyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA
Pre-print
10:30 - 12:30
Foundations and timing channelsPriSC at Rosalie
Chair(s): Marco Vassena CISPA Helmholtz Center for Information Security
10:30
24m
Talk
Exorcising Spectres with Secure Compilers
PriSC
Marco Patrignani Stanford University & CISPA , Marco Guarnieri IMDEA Software Institute
Media Attached File Attached
10:54
24m
Talk
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Carmine Abate Inria Paris, Roberto Blanco Inria, Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Deepak Garg Max Planck Institute for Software Systems, Cătălin Hriţcu Inria Paris, Marco Patrignani Stanford University & CISPA , Éric Tanter University of Chile, Jérémy Thibault Inria Paris
Media Attached File Attached
11:18
24m
Talk
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan Bay Aarhus University, Aslan Askarov Aarhus University
Media Attached File Attached
11:42
24m
Talk
Hermes: Implementing Cryptography without Side-channels
PriSC
Ken Friis Larsen DIKU, University of Copenhagen, Torben Mogensen DIKU, University of Copenhagen, Michael Kirkedal Thomsen DIKU, University of Copenhagen
File Attached
12:06
24m
Talk
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Sandrine Blazy Univ Rennes- IRISA, Rémi Hutin IRISA / ENS Rennes, David Pichardie Univ 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 Bertot INRIA
14:00
60m
Talk
Autosubst 2: Mechanising binders in Coq (Keynote)
CoqPL
Kathrin Stark Princeton University, USA
File Attached
14:00 - 15:05
CoercionsWGT at Orleans
Chair(s): Jeremy G. Siek Indiana University, USA
14:00
32m
Talk
Hypercoercions and a Framework for Equivalence of Cast Calculi
WGT
Kuang-Chen Lu Indiana University Bloomington, Jeremy G. Siek Indiana University, USA, Andre Kuhlenschmidt Indiana University
Pre-print
14:32
32m
Talk
Space-Efficient Gradual Typing in Coercion-Passing Style
WGT
Yuya Tsuda Kyoto University, Atsushi Igarashi Kyoto University, Japan, Tomoya Tabuchi Kyoto University
Pre-print
14:00 - 15:05
New outlooks on secure compilationPriSC at Rosalie
Chair(s): Cristina Cifuentes Oracle Labs
14:00
24m
Talk
Exploits as Insecure Compilation
PriSC
Jennifer Paykin Galois, Inc., Eric Mertens Galois, Inc., Mark Tullsen Galois, Inc, Luke Maurer Galois, Inc, Benoit Razet Galois, Inc, Alexander Bakst Galois, Inc, Scott Moore Galois, Inc
Pre-print Media Attached File Attached
14:24
24m
Talk
Universal Composability is Secure Compilation
PriSC
Marco Patrignani Stanford University & CISPA , Riad S. Wahby Stanford University, USA, Robert Künnemann CISPA, Saarland University
Media Attached File Attached
14:48
8m
Talk
Short Talk: Automatically Eliminating Speculative Leaks With Blade
PriSC
Marco Vassena CISPA Helmholtz Center for Information Security, Klaus v. Gleissenthall University 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 Ramananandro Microsoft 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): Robbert Krebbers Delft University of Technology, Joseph Tassarotti Boston College
15:35
30m
Talk
Towards Formally Verified Just-in-Time compilation
CoqPL
Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes- IRISA, David Pichardie Univ Rennes, ENS Rennes, IRISA
File Attached
16:05
30m
Talk
A Coq Library of Undecidable Problems
CoqPL
Yannick Forster Saarland University, Dominique Larchey-Wendling CNRS, LORIA, Andrej Dudenhefner Saarland University, Edith Heiter Saarland University, Dominik Kirst Saarland University, Fabian Kunze Saarland University, Gert Smolka Saarland University, Simon Spies Saarland University, Dominik Wehr Saarland University, Universiteit van Amsterdam, Maximilian Wuttke Saarland 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 Vazou IMDEA Software Institute
15:35
32m
Talk
Gradual Verification of Recursive Heap Data Structures
WGT
Jenna Wise (DiVincenzo) Carnegie Mellon University, Johannes Bader Facebook, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
Pre-print
16:07
33m
Talk
Gradual Program Analysis
WGT
Samuel Estep Liberty University, Jenna Wise (DiVincenzo) Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Johannes Bader Facebook, Joshua Sunshine Carnegie Mellon University
Pre-print
16:40
10m
Break
Minibreak
WGT

16:50
30m
Talk
Blame tracking at higher fidelity
WGT
Jakub Zalewski University of Edinburgh, James McKinna University of Edinburgh, J. Garrett Morris University of Kansas, USA, Philip Wadler University 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 Patrignani Stanford University & CISPA , Jonathan Protzenko Microsoft Research, Redmond
15:35
24m
Talk
Flexible Tag-based Policies for Compartmentalized C
PriSC
Sean Anderson Portland State University, Andrew Tolmach Portland State University, CHR Chhak Portland State University
Media Attached File Attached
15:59
24m
Talk
Mechanized Reasoning about a Capability Machine
PriSC
Aina Linn Georges Aarhus University, Alix Trieu Aarhus University, Lars Birkedal Aarhus University
Media Attached
16:23
24m
Talk
Securing Interruptible Enclaves
PriSC
Matteo Busi Università di Pisa - Dipartimento di Informatica, Job Noorman imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Jo Van Bulck imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Letterio Galletta IMT School for Advanced Studies, Pierpaolo Degano Università di Pisa - Dipartimento di Informatica, Jan Tobias Mühlberg imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Frank Piessens KU 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 Bosamiya Carnegie Mellon University, Benjamin Lim Carnegie Mellon University, Bryan Parno Carnegie Mellon University
Media Attached File Attached
17:21
24m
Talk
Memory Safety Preservation for WebAssembly
PriSC
Marco Vassena CISPA Helmholtz Center for Information Security, Marco Patrignani Stanford University & CISPA
Link to publication Media Attached File Attached