POPL 2020 Program

Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper

09:30 - 10:00
Talk

Peter SelingerDalhousie University

The Siren Song of Temporal Synthesis

09:00 - 10:00: VMCAI 2020 - Invited 1 at St Jerome
Chair(s): Dirk BeyerLMU Munich

09:00 - 10:00
Talk

Moshe VardiRice University

10:00 - 10:30: Catering - Sunday Morning Break at Break

10:00 - 10:30
Coffee break

Break

10:30 - 12:30: PLanQC - Invited Talks, Pulses, Errors and Categories at Maurepas
Chair(s): Frank Fu

10:30 - 11:00
Talk

Invited Talk: Q# - Going Beyond Quantum Circuits

Bettina HeimMicrosoft

Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions

11:00 - 11:30
Talk

Fred ChongUniversity of Chicago

Tuning up entanglement through the cloud using Qiskit-OpenPulse

11:30 - 11:50
Talk

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

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

Andre KornellTulane University, Bert LindenhoviusTulane University, Michael MisloveTulane

10:30 - 12:30: VMCAI 2020 - Papers 1 at St Jerome
Chair(s): Natasha SharyginaUSI Lugano, Switzerland

10:30 - 11:00
Talk

Witnessing Secure Compilation

Kedar NamjoshiBell Labs, Nokia, Lucas M. TabajaraRice University

11:00 - 11:30
Talk

BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results

Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Luca OlivieriJuliaSoft SRL, Fausto SpotoU. Verona

11:30 - 12:00
Coffee break

Fixing Code That Explodes Under Symbolic Evaluation

12:00 - 12:30
Talk

Sorawee PorncharoenwaseUniversity of Washington, James BornholtUniversity of Texas at Austin, Emina TorlakUniversity of Washington

12:30 - 14:00: Catering - Sunday Lunch at Lunch Room

12:30 - 14:00
Lunch

Runtime Analysis of Quantum Programs: A Formal Approach

14:00 - 15:05: PLanQC - Formal Methods at Maurepas
Chair(s): Dominique UnruhUniversity of Tartu

14:00 - 14:20
Talk

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

Christopĥe CharetonCEA, LIST, France, Sebastien BardinCEA LIST, François BobotCEA, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay

Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages

14:40 - 15:05
Talk

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

Safety and Robustness for Deep Learning with Provable Guarantees

14:00 - 15:05: VMCAI 2020 - Invited 2 at St Jerome
Chair(s): Damien ZuffereyMPI-SWS

14:00 - 15:05
Talk

Marta KwiatkowskaUniversity of Oxford

15:05 - 15:35: Catering - Sunday Afternoon Break at Break

15:35 - 16:35: PLanQC - NISQ at Maurepas
Chair(s): Will ZengUnitary Fund

15:35 - 15:55
Talk

Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation

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

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

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

The Correctness of a Code Generator for a Functional Language

15:35 - 17:45: VMCAI 2020 - Papers 2 at St Jerome
Chair(s): Kedar NamjoshiBell Labs, Nokia

15:35 - 16:07
Talk

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

Jack GarzellaUniversity of Utah, Marek S. BaranowskiUniversity of Utah, Shaobo HeUniversity of Utah, Zvonimir RakamaricUniversity of Utah

16:40 - 17:12
Coffee break

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction

17:12 - 17:45
Talk

Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Noam RinetzkyTel Aviv University, Sharon ShohamTel Aviv university

16:50 - 17:50: PLanQC - Quantum-Classical Communication at Maurepas
Chair(s): Michael HicksUniversity of Maryland

16:50 - 17:10
Talk

Extending Modern C++ for Heterogeneous Quantum-Classical Computing

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

Dongho LEELRI / CEA LIST, Univ Paris Saclay, Sebastien BardinCEA LIST, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay

Automated distribution of quantum circuits via hypergraph partitioning

17:30 - 17:50
Talk

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: (GMT-06:00) Saskatchewan, Central America change

08:30 - 10:00: PADL 2020 - Logical Engines and Applications at Bacchus
Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK

08:30 - 08:45
Day opening

Opening

Gopal Gupta

08:45 - 09:35
Talk

Invited Talk: Logical Engines for Cloud Configurations

Nikolaj BjørnerMicrosoft Research

09:35 - 10:00
Talk

Interactive Text Graph Mining with a Prolog-based Dialog Engine

Paul TarauUniversity of North Texas, Eduardo Blanco

09:00 - 10:00: TutorialFest - Building Program Reasoning Tools using LLVM and Z3 (I) at Muses

09:00 - 10:00
Tutorial

[T1] Building Program Reasoning Tools using LLVM and Z3

Elizabeth DinellaUniversity of Pennsylvania, Pardis PashakhanlooUniversity of Pennsylvania, Anthony Canino, Mayur NaikUniversity of Pennsylvania

Model Checking for Safe Autonomy

09:00 - 10:00: VMCAI 2020 - Invited 3 at St Jerome
Chair(s): Damien ZuffereyMPI-SWS

09:00 - 10:00
Talk

Rajeev AlurUniversity of Pennsylvania

09:00 - 10:00: CPP 2020 - Invited talk 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

Grigore RosuUniversity of Illinois at Urbana-Champaign, Xiaohong ChenUniversity of Illinois at Urbana-Champaign

DOI Media Attached

09:00 - 10:00: ADSL 2020 - Morning Keynote at Conde

09:00 - 10:00
Talk

Relational reasoning using concurrent separation logic

Robbert KrebbersDelft University of Technology

Network Verification: Past, Present, and Future

09:00 - 10:00: PEPM 2020 - Opening & Keynote Talk 1 at Frontenac
Chair(s): Casper Bach PoulsenDelft University of Technology, Zhenjiang HuPeking University

09:00 - 09:05
Day opening

Opening

Casper Bach PoulsenDelft University of Technology, Zhenjiang HuPeking University

09:05 - 10:00
Talk

Nate FosterCornell University

09:00 - 10:00: TutorialFest - Synthesizing Programs from Types (I) at SHANGRI-LA

09:00 - 10:00
Tutorial

[T3] Synthesizing Programs from Types

Nadia PolikarpovaUniversity of California, San Diego

[T2] Verified Quantum Computing

09:00 - 10:00: TutorialFest - Verified Quantum Computing (I) at Endymion

09:00 - 10:00
Tutorial

Robert RandUniversity of Maryland

[T6] Verifying Probabilistic Properties with Couplings

09:00 - 10:00: TutorialFest - Verifying Probabilistic Properties with Couplings (I) at Babylon

09:00 - 10:00
Tutorial

Justin HsuUniversity of Wisconsin-Madison, USA

AQuA: ASP-based Visual Question Answering

10:00 - 10:30: Catering - Monday Morning Break at Break

10:30 - 12:00: PADL 2020 - Answer Set Programming Systems at Bacchus
Chair(s): Neng-Fa ZhouCUNY Brooklyn College and Graduate Center

10:30 - 10:55
Talk

Kinjal Basu, Farhad Shakerin, Gopal Gupta

10:55 - 11:10
Short-paper

Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report

Alex Brik, Jeffrey XuUCLA

11:10 - 11:25
Short-paper

VRASP: A Virtual Reality Environment for Learning Answer Set Programming

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

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: TutorialFest - Building Program Reasoning Tools using LLVM and Z3 (II) at Muses

10:30 - 12:30
Tutorial

[T1] Building Program Reasoning Tools using LLVM and Z3

Elizabeth DinellaUniversity of Pennsylvania, Pardis PashakhanlooUniversity of Pennsylvania, Anthony Canino, Mayur NaikUniversity of Pennsylvania

A Systematic Approach to Abstract Interpretation of Program Transformations

10:30 - 12:30: VMCAI 2020 - Papers 3 at St Jerome
Chair(s): Dirk BeyerLMU Munich

10:30 - 11:00
Research paper

Sven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz

Sharing Ghost Variables in a Collection of Abstract Domains

11:00 - 11:30
Talk

Marc ChevalierENS, CNRS, PSL University, INRIA, Jerome FeretINRIA Paris

11:30 - 12:00
Coffee break

Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation

12:00 - 12:30
Talk

Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Roman ManevichMellanox Technologies, Noam RinetzkyTel Aviv University

10:30 - 11:35: CPP 2020 - Program verification at Maurepas
Chair(s): Nikhil SwamyMicrosoft Research

10:30 - 10:51
Talk

A Verified Packrat Parser Interpreter for Parsing Expression Grammars

Clement BlaudeauEcole Polytechnique, Natarajan ShankarSRI International, USA

10:51 - 11:13
Talk

Proof Pearl: Braun Trees

Tobias NipkowTechnische Universität München, Thomas SewellChalmers University of Technology, Sweden

FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq

11:13 - 11:35
Talk

Thomas LetanANSSI, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2

Extending the Profile Abstraction for Complete Entailment Checking of Symbolic Heaps of Bounded Treewidth

10:30 - 12:30: ADSL 2020 - Research Papers at Conde

10:30 - 11:00
Research paper

Florian ZulegerTU Vienna, Jens Katelaan

Steel: scaling up memory reasoning for F*

11:00 - 11:30
Research paper

Denis MerigouxINRIA, Aymeric FromherzCarnegie Mellon University

11:30 - 12:00
Research paper

Strong-Separation Logic

Florian ZulegerTU Vienna, Jens Katelaan

The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions

12:00 - 12:30
Research paper

Mnacho Echenim, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier

Pre-print File Attached

10:30 - 12:30: PEPM 2020 - Sessions 1 & 2 at Frontenac
Chair(s): Ohad KammarUniversity of Edinburgh, Walid Taha

10:30 - 11:05
Talk

Dependently-Typed Multi-Stage Programming Revisited (invited talk)

Atsushi IgarashiKyoto University, Japan

11:05 - 11:30
Research paper

High-Fidelity Metaprogramming with Separator Syntax Trees

Rodin AarssenCWI, Netherlands, Tijs van der StormCWI & University of Groningen, Netherlands

DOI

11:30 - 11:45
Break

Mini Break 1

11:45 - 12:10
Research paper

Module Generation without Regret

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

Jacques CaretteMcMaster University, Brooks MacLachlanMcMaster University, Spencer SmithMcMaster University, Computing and Software Department

DOI Pre-print File Attached

10:30 - 12:30: TutorialFest - Synthesizing Programs from Types (II) at SHANGRI-LA

10:30 - 12:30
Tutorial

[T3] Synthesizing Programs from Types

Nadia PolikarpovaUniversity of California, San Diego

[T2] Verified Quantum Computing

10:30 - 12:30: TutorialFest - Verified Quantum Computing (II) at Endymion

10:30 - 12:30
Tutorial

Robert RandUniversity of Maryland

[T6] Verifying Probabilistic Properties with Couplings

10:30 - 12:30: TutorialFest - Verifying Probabilistic Properties with Couplings (II) at Babylon

10:30 - 12:30
Tutorial

Justin HsuUniversity of Wisconsin-Madison, USA

Verifying x86 Instruction Implementations

11:45 - 12:30: CPP 2020 - Automated verification and SAT solving at Maurepas
Chair(s): Ori LahavTel Aviv University

11:45 - 12:07
Talk

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

Adrian Rebola PardoTU Wien, Johannes AltmanningerTU Wien

12:30 - 14:00: Catering - Monday Lunch at Lunch Room

12:30 - 14:00
Lunch

On the Effects of Integrating Region-based Memory Managemen and Generational Garbage Collection in ML

13:30 - 15:00: PADL 2020 - Memory and Real-Time in Functional Programming at Bacchus
Chair(s): John HughesChalmers University of Technology, Sweden

13:30 - 13:55
Talk

Martin ElsmanUniversity of Copenhagen, Denmark, Niels Hallenberg

13:55 - 14:20
Talk

RTMLton: An SML Runtime for Real-Time Systems

Bhargav Shivkumar, Jeffrey Murphy, Lukasz ZiarekSUNY Buffalo, USA

14:20 - 14:45
Talk

A Timed IO Monad

David JaninBordeaux INP / CNRS LaBRI / Bordeaux University

14:45 - 15:00
Other

Panel: Memory and real-time programming in practice

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: ADSL 2020 - Afternoon Keynote at Conde

14:00 - 15:05
Talk

SLEdge: Bounded Model Checking in Separation Logic

Josh BerdineFacebook

Reasoning about Progress of Concurrent Objects

14:00 - 15:05: PEPM 2020 - Keynote Talk 2 at Frontenac
Chair(s): Casper Bach PoulsenDelft University of Technology

14:00 - 15:00
Talk

Xinyu FengNanjing University

14:00 - 15:05: VMCAI 2020 - Papers 4 at St Jerome
Chair(s): Ruzica PiskacYale University, USA

14:00 - 14:32
Talk

Synthesizing Environment Invariants for Modular Hardware Verification

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

Eric Rothstein-MorrisSingapore University of Technology and Design, Jun SunSingapore Management University, Singapore, Sudipta ChattopadhyaySingapore University of Technology and Design

14:00 - 15:05: TutorialFest - Programming and Reasoning with Kleene Algebra with Tests (I) at SHANGRI-LA

14:00 - 15:05
Tutorial

[T7] Programming and Reasoning with Kleene Algebra with Tests

Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London

An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction

14:00 - 15:05: CPP 2020 - Proof engineering and user interaction at Maurepas
Chair(s): Yves BertotINRIA

14:00 - 14:21
Talk

Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Steve ZdancewicUniversity of Pennsylvania

Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

14:21 - 14:43
Talk

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

Talia RingerUniversity of Washington, Alex Sanchez-SternUniversity of California, San Diego, Dan GrossmanUniversity of Washington, Sorin LernerUniversity of California, San Diego

[T4] Proving Semantic Type Soundness in Iris

14:00 - 15:05: TutorialFest - Proving Semantic Type Soundness in Iris (I) at Muses

14:00 - 15:05
Tutorial

Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven

[T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models

14:00 - 15:05: TutorialFest - Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (I) at Endymion

14:00 - 15:05
Tutorial

Konstantinos (Kostis) SagonasUppsala University, Sweden

15:05 - 15:35: Catering - Monday Afternoon Break at Break

15:30 - 17:00: PADL 2020 - Answer Set Programming Applications and Competitive programming experience at Bacchus
Chair(s): Alex Brik

15:30 - 15:55
Talk

Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming

Sheung Chi Chan, James CheneyUniversity of Edinburgh, UK

15:55 - 16:20
Talk

On Repairing Web Services Workflows

Thanh Hai Nguyen, Enrico PontelliNew Mexico State University, Tran Cao Son

16:20 - 17:00
Talk

Competitive Programming with PiCat

Neng-Fa ZhouCUNY Brooklyn College and Graduate Center

15:35 - 17:45: ADSL 2020 - Closing Session at Conde

15:35 - 16:40
Talk

Programs Synthesis with Separation Logic

Nadia PolikarpovaUniversity of California, San Diego

16:40 - 17:45
Talk

Local Reasoning for Global Graph Properties

Thomas WiesNew York University

15:35 - 16:40: CPP 2020 - Decidability and complexity at Maurepas
Chair(s): Kathrin StarkSaarland University, Germany

15:35 - 15:56
Talk

Verified Programming of Turing Machines in Coq

Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University

A Functional Proof Pearl: Inverting the Ackermann Hierarchy

15:56 - 16:18
Talk

Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore

Undecidability of Higher-Order Unification Formalised in Coq

16:18 - 16:40
Talk

Simon SpiesSaarland University, Yannick ForsterSaarland University

Cheap CTL Compassion in NuSMV

15:35 - 17:45: VMCAI 2020 - Papers 5 at St Jerome
Chair(s): Nikolaj BjørnerMicrosoft Research

15:35 - 16:07
Talk

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

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

Generalized Property-Directed Reachability for Hybrid Systems

17:12 - 17:45
Talk

Kohei SuenagaGraduate School of Informatics, Kyoto University, Takuya IshizawaKyoto University

Link to publication Pre-print

15:35 - 17:35: TutorialFest - Programming and Reasoning with Kleene Algebra with Tests (II) at SHANGRI-LA

15:35 - 17:35
Tutorial

[T7] Programming and Reasoning with Kleene Algebra with Tests

Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London

[T4] Proving Semantic Type Soundness in Iris

15:35 - 17:35: TutorialFest - Proving Semantic Type Soundness in Iris (II) at Muses

15:35 - 17:35
Tutorial

Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven

Frex: Free extensions for normalisation by evaluation (invited talk)

15:35 - 17:45: PEPM 2020 - Sessions 3 & 4 at Frontenac
Chair(s): Jeremy YallopUniversity of Cambridge, UK, Atsushi IgarashiKyoto University, Japan

15:35 - 16:10
Talk

Ohad KammarUniversity of Edinburgh

Symbolic Bisimulation for Open and Parameterized System

16:10 - 16:35
Research paper

Zechen HouEast China Normal University, Eric MadelaineINRIA

DOI File Attached

16:35 - 16:50
Break

Mini Break 2

16:50 - 17:25
Talk

Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited talk)

Walid Taha

17:25 - 17:45
Short-paper

An approach to generating text-based IDEs with syntax completion from syntax specification

Isao SasanoShibaura Institute of Technology

DOI

15:35 - 17:35: TutorialFest - Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (II) at Endymion

15:35 - 17:35
Tutorial

[T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models

Konstantinos (Kostis) SagonasUppsala University, Sweden

16:50 - 17:56: CPP 2020 - Homotopy Type Theory and PC chairs' report at Maurepas
Chair(s): Floris van DoornUniversity of Pittsburgh

16:50 - 17:12
Talk

Cubical Synthetic Homotopy Theory

Anders MörtbergDepartment of Mathematics, Stockholm University, Loïc PujetGallinette Project-Team, Inria

Three equivalent ordinal notation systems in Cubical Agda

17:12 - 17:34
Talk

Fredrik Nordvall ForsbergUniversity of Strathclyde, Chuangjie XuLudwig-Maximilians-Universität München, Neil GhaniUniversity of Strathclyde

DOI Media Attached File Attached

17:34 - 17:56
Talk

PC Chairs' report

Jasmin BlanchetteVrije Universiteit Amsterdam, Cătălin HriţcuInria Paris

Tue 21 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

08:30 - 10:00: PADL 2020 - Reasoning and Efficient Implementation at Bacchus
Chair(s): Y. Annie LiuStony Brook University

08:30 - 09:20
Talk

Invited Talk: Symbolic Reasoning About Machine Learning Systems

Adnan DarwicheUCLA

09:20 - 09:45
Talk

Exploiting Database Systems and Treewidth for Counting

Johannes K. FichteTU Dresden, Markus Hecher, Patrick Thier, Stefan Woltran

09:45 - 10:00
Short-paper

Whitebox Induction of Default Rules Using High-Utility Itemset Mining

Farhad Shakerin, Gopal Gupta

09:00 - 10:00: LAFI (né PPS) - A at St Claude

09:00 - 10:00
Talk

Invited talk: Nonstandard Interpretation in Pyro

Fritz Obermeyer

Invited talk: Proof Assistants at the Hardware-Software Interface

09:00 - 10:00: CPP 2020 - Invited talk at Maurepas
Chair(s): Jasmin BlanchetteVrije Universiteit Amsterdam

09:00 - 10:00
Talk

Adam ChlipalaMassachusetts Institute of Technology

DOI Media Attached

09:00 - 10:00: PLMW 2020 - Morning 1 at Ile de France III (IDF III)
Chair(s): Stephanie BalzerCarnegie Mellon University, USA

09:00 - 09:10
Day opening

Opening

Brigitte PientkaMcGill University

09:10 - 10:00
Talk

How to Write Papers So People Can Read ThemMentoring Event

Derek DreyerMPI-SWS

Interactive Knowledge Shares

09:00 - 10:00: HASE 2020 - Opening & Interactive Knowledge Shares at Orpheus

09:00 - 09:10
Day opening

Opening Plenary

09:10 - 10:10
Tutorial

Peter O'HearnFacebook, Philippa GardnerImperial College London, Muralidaran VijayaraghavanSiFive, Peter SewellUniversity of Cambridge

09:00 - 10:00: VMCAI 2020 - Papers 6 at St Jerome
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

09:00 - 09:30
Talk

How to Win First-Order Safety Games

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

Ruben LapauwKatholieke Universiteit Leuven, Maurice BruynoogheKatholieke Universiteit Leuven, Marc DeneckerKatholieke Universiteit Leuven

10:00 - 10:30: Catering - Tuesday Morning Break at Break

10:30 - 12:30: Ally Skills Session - Ally Skills Session at Frontenac

10:30 - 12:30
Other

Ally Skills SessionMentoring Event

10:30 - 12:30: LAFI (né PPS) - B at St Claude

10:30 - 11:00
Talk

A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation

Carol MakUniversity of Oxford, C.-H. Luke OngUniversity of Oxford

11:00 - 11:30
Talk

A Monad for Point Processes

Swaraj DashUniversity of Oxford, Sam StatonUniversity of Oxford

Denotational Semantics for Differentiable Programming with Manifolds

11:30 - 12:00
Talk

Jesse SigalUniversity of Edinburgh

12:00 - 12:30
Talk

Backpropagation in the Simply Typed Lambda-calculus with Linear Negation

Aloïs BrunelDeepomatic, Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris

10:30 - 11:35: CPP 2020 - Mechanized metatheory 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

Yannick ForsterSaarland University, Kathrin StarkSaarland University, Germany

A Mechanized Formalization of GraphQL

10:51 - 11:13
Talk

Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile

ConCert: A Smart Contract Certification Framework in Coq

11:13 - 11:35
Talk

Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University

Making Progress Under Uncertainty in SMT Solving, Research, and LifeMentoring Event

10:30 - 12:30: PLMW 2020 - Morning 2 at Ile de France III (IDF III)
Chair(s): Robbert KrebbersDelft University of Technology

10:30 - 11:10
Talk

Lindsey KuperUniversity of California, Santa Cruz

Research as a collaborative effortMentoring Event

11:10 - 11:50
Talk

Marco GaboardiBoston University

Theorem provers are a P.L. researcher's best friendMentoring Event

11:50 - 12:30
Talk

Xavier LeroyCollège de France

Language Inclusion for Finite Prime Event Structures

10:30 - 12:30: VMCAI 2020 - Papers 7 at St Jerome
Chair(s): Thomas WiesNew York University

10:30 - 11:00
Talk

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

Swen JacobsCISPA Helmholtz Center for Information Security, Mouhammad SakrSaarland University, Martin ZimmermannUniversity of Liverpool

11:30 - 12:00
Coffee break

Solving LIA* Using Approximations

12:00 - 12:30
Talk

Maxwell LevatichYale, Nikolaj BjørnerMicrosoft Research, Ruzica PiskacYale University, USA, Sharon ShohamTel Aviv university

10:30 - 12:00: PADL 2020 - Small Languages and Implementation at Bacchus
Chair(s): James CheneyUniversity of Edinburgh, UK

10:30 - 10:55
Talk

Explanations for Dynamic Programming

Martin ErwigOregon State University, Prashant Kumar, Alan Fern

10:55 - 11:20
Talk

A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams

Johannes Eriksson, Masoumeh Parsa

11:20 - 11:35
Short-paper

Variability-aware Datalog

Ramy Shahin, Marsha ChechikUniversity of Toronto

11:35 - 12:00
Other

Panel: Reasoning for machine learning at large

Adnan DarwicheUCLA, Johannes K. FichteTU Dresden, Markus Hecher, Patrick Thier, Stefan Woltran, Farhad Shakerin, Gopal Gupta, Martin ErwigOregon State University, Prashant Kumar, Alan Fern, Johannes Eriksson, Masoumeh Parsa, Ramy Shahin, Marsha ChechikUniversity of Toronto

10:30 - 12:30: HASE 2020 - Working Sessions I at Orpheus

10:30 - 12:30
Meeting

Working Sessions I

Ben LaurieGoogle Research, Hong-Seok Kim, Jonathan ProtzenkoMicrosoft Research, Redmond

11:45 - 12:30: CPP 2020 - Verified cryptography 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

David ButlerAlan Turing Institute, David AspinallUniversity of Edinburgh, Adria GasconAlan Turing Institute

Verified Security of BLT Signature Scheme

12:07 - 12:30
Talk

Denis FirsovGuardtime AS, Ahto BuldasTallinn University of Technology, Ahto TruuGuardtime AS, Risto LaanojaGuardtime AS

12:30 - 14:00: Catering - Tuesday Lunch at Lunch Room

12:30 - 14:00
Lunch

Invited Talk: Relational Artificial Intelligence

13:30 - 15:00: PADL 2020 - Invited Experience and Direction Session at Bacchus
Chair(s): David WarrenStony Brook University, Konstantinos (Kostis) SagonasUppsala University, Sweden

13:30 - 14:00
Talk

Molham ArefRelational.ai

14:00 - 14:30
Talk

Invited Talk: Learning Interpretable Rules from Structured Data

Mayur NaikUniversity of Pennsylvania

14:30 - 15:00
Talk

Invited Talk: An Introduction to the Imandra Automated Reasoning System

Grant PassmoreImandra Inc.

14:00 - 15:05: PLMW 2020 - Afternoon 1 at Ile de France III (IDF III)
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA

14:00 - 15:05
Talk

PanelMentoring Event

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

Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support

14:00 - 15:05: LAFI (né PPS) - C at St Claude

14:00 - 14:30
Talk

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

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

14:49 - 15:05
Talk

Monte Carlo Semantic Differencing of Probabilistic Programs

Marco Cusumano-TownerMIT-CSAIL, Vikash MansinghkaMIT

14:00 - 15:05: CPP 2020 - Concurrency and linearity at Maurepas
Chair(s): Zhong ShaoYale University

14:00 - 14:21
Talk

Formalizing Determinacy of Concurrent Revisions

Roy OverbeekVrije Universiteit Amsterdam

Formalizing π-calculus in Guarded Cubical Agda

14:21 - 14:43
Talk

Niccolò VeltriTallinn University of Technology, Andrea VezzosiIT University Copenhagen

Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages

14:43 - 15:05
Talk

Arjen RouvoetDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology

Formalizing and Checking Multilevel Consistency

14:00 - 15:05: VMCAI 2020 - Papers 8 at St Jerome
Chair(s): Ori LahavTel Aviv University

14:00 - 14:32
Talk

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

Wytse OortwijnETH Zürich, Dilian GurovKTH Royal Institute of Technology, Marieke HuismanUniversity of Twente

14:00 - 15:05: HASE 2020 - Peer Skillshare at Orpheus

13:30 - 14:15
Tutorial

Peer Skillshare

Sarah de HaasGoogle Research

15:05 - 15:35: Catering - Tuesday Afternoon Break at Break

15:30 - 17:00: PADL 2020 - Invited Experience and Direction Session (Continued) 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

Philip WadlerUniversity of Edinburgh, UK

16:00 - 16:45
Other

Panel: Experience and Direction

Molham ArefRelational.ai, Mayur NaikUniversity of Pennsylvania, Grant PassmoreImandra Inc., Philip WadlerUniversity of Edinburgh, UK

16:45 - 17:00
Day closing

Closing

Ekaterina KomendantskayaHeriot-Watt University, UK, Y. Annie LiuStony Brook University

15:35 - 17:45: PLMW 2020 - Afternoon 2 at Ile de France III (IDF III)
Chair(s): Nobuko YoshidaImperial College London

15:40 - 16:40
Talk

How Can I Academia When My Brain Can't Even? Mental Health in Grad School and BeyondMentoring Event

Kenny FonerGalois

Automated Program Verification using Abductive ReasoningMentoring Event

16:40 - 16:50
Coffee break

Mini break

16:50 - 17:35
Talk

Isil DilligUniversity of Texas Austin

Coinductive Trees for Exact Inference of Probabilistic Programs

15:35 - 17:45: HASE 2020 - Afternoon Session at Orpheus

14:30 - 16:30
Meeting

Working Sessions II

Ben LaurieGoogle Research, Satnam SinghGoogle Research

16:30 - 17:45
Day closing

Closing Plenary

15:35 - 17:45: LAFI (né PPS) - D at St Claude

15:35 - 16:05
Talk

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?)

Dario SteinUniversity of Oxford, Sam StatonUniversity of Oxford, Michael WolmanMcGill University

Density Functions of Statistical Probabilistic Programs

16:35 - 17:05
Talk

Tom MattinsonUniversity of Oxford, C.-H. Luke OngUniversity of Oxford

17:05 - 17:35
Talk

Probabilistic Programming around Gaussian Processes

David TolpinPUB+

17:35 - 17:45
Day closing

Closing

15:35 - 16:40: CPP 2020 - Formalized mathematics 1 at Maurepas
Chair(s): Robert Y. LewisVrije Universiteit Amsterdam

15:35 - 15:56
Talk

Formalising perfectoid spaces

Patrick MassotUniversité Paris Sud, Kevin BuzzardImperial College London, Johan CommelinUniversität Freiburg

A Constructive Formalization of the Weak Perfect Graph Theorem

15:56 - 16:18
Talk

Abhishek Kr SinghTata Institute of Fundamental Research Mumbai, Raja NatarajanTata Institute of Fundamental Research Mumbai

Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq

16:18 - 16:40
Talk

Christian DoczkalUniversité Côte d'Azur, Damien PousCNRS, ENS Lyon

POPLmark 15 Year Retrospective Panel

15:35 - 17:45: POPLmark 15 Year Retrospective Panel - POPLmark 15 Year Retrospective Panel at Frontenac

15:35 - 17:35
Other

15:35 - 17:45: VMCAI 2020 - Panel Session at St Jerome
Chair(s): Dirk BeyerLMU Munich

15:35 - 17:45
Other

Panel "The Future of Software Verification" at 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: CPP 2020 - Formalized mathematics 2 at Maurepas
Chair(s): Tobias NipkowTechnische Universität München

16:50 - 17:12
Talk

The Poincaré-Bendixson Theorem in Isabelle/HOL

Fabian ImmlerCarnegie Mellon University, Yong Kiam TanCarnegie Mellon University, USA

A Formal Proof of the Independence of the Continuum Hypothesis

17:12 - 17:34
Talk

Jesse Michael HanUniversity of Pittsburgh, Floris van DoornUniversity of Pittsburgh

The Lean mathematical library

17:34 - 17:56
Talk

The mathlib Community

Mentoring BreakfastMentoring Event

Wed 22 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

07:45 - 08:45: Mentoring Breakfasts - Wednesday Mentoring Breakfast at Breakfast Room

07:45 - 08:45
Social Event

08:45 - 09:00: Research Papers - Welcome + SIGPLAN Award Ceremony 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

Can Programming Languages Research impact Deep Learning 2.0?Invited Talk

09:00 - 10:00: Research Papers - Invited Talk at Ile de France II (IDF II)
Chair(s): Brigitte PientkaMcGill University

09:00 - 10:00
Talk

Martin VechevETH Zürich

The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space

10:00 - 10:30: Catering - Wednesday Morning Break at Break

10:30 - 11:35: Research Papers - Complexity / Decision Procedures at Ile de France III (IDF III)
Chair(s): Roopsha SamantaPurdue University

10:30 - 10:51
Talk

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

Yotam FeldmanTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university

Parameterized Verification under TSO is PSPACE-Complete

11:13 - 11:35
Talk

Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Rojin RezvanSharif University

Link to publication DOI

10:30 - 11:35: Research Papers - Probabilistic Programming 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

Wonyeol LeeKAIST, Hangyeol YuKAIST, Xavier RivalINRIA/CNRS/ENS Paris, Hongseok YangKAIST

Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages

10:51 - 11:13
Talk

Alexander K. LewMassachusetts Institute of Technology, USA, Marco Cusumano-TownerMIT-CSAIL, Benjamin ShermanMassachusetts Institute of Technology, USA, Michael CarbinMassachusetts Institute of Technology, Vikash MansinghkaMIT

Semantics of Higher-Order Probabilistic Programs with Conditioning

11:13 - 11:35
Talk

Fredrik DahlqvistUniversity College London, Dexter KozenCornell University

Link to publication DOI Media Attached File Attached

11:45 - 12:30: Research Papers - Reasoning about Program Complexity/Efficiency 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

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

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: Research Papers - Synthesis 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

Zheng GuoUniversity of California, San Diego, Michael 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

Malavika SamakCSAIL, MIT, Deokhwan KimCSAIL, MIT, Martin RinardMIT

Link to publication DOI Media Attached File Attached

12:30 - 14:00: LGBTQ Lunch - LGBTQ Lunch at Endymion

12:30 - 14:00
Lunch

LGBTQ LunchMentoring Event

12:30 - 14:00: Catering - Wednesday Lunch at Lunch Room

12:30 - 14:00
Lunch

What is Decidable about Gradual Types?

14:00 - 15:05: Research Papers - Gradual Typing / Language Design at Ile de France III (IDF III)
Chair(s): Jeremy G. SiekIndiana University, USA

14:00 - 14:21
Talk

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

Max NewNortheastern University, Dustin JamnerNortheastern University, USA, Amal AhmedNortheastern University, USA

Does Blame Shifting Work?

14:43 - 15:05
Talk

Lukas LazarekNorthwestern University, Alexis KingNorthwestern University, Samanvitha SundarNorthwestern University, Robby FindlerNorthwestern University, USA, Christos DimoulasPLT @ Northwestern University

The Future is Ours: Prophecy Variables in Separation Logic

14:00 - 15:05: Research Papers - Program Logics at Ile de France II (IDF II)
Chair(s): Azalea RaadMPI-SWS, Germany

14:00 - 14:21
Talk

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

Spy Game: Verifying a Local Generic Solver in Iris

14:21 - 14:43
Talk

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

Jonas Kastberg HinrichsenIT University of Copenhagen, Jesper BengtsonIT University of Copenhagen, Robbert KrebbersDelft University of Technology

Link to publication DOI Media Attached File Attached

15:05 - 15:35: Catering - Wednesday Afternoon Break at Break

15:35 - 16:40: Research Papers - Automatic Differentiation / Kleene Algebra at Ile de France II (IDF II)
Chair(s): Lars BirkedalAarhus University

15:35 - 15:56
Talk

A Simple Differentiable Programming Language

Gordon PlotkinGoogle, Martín AbadiGoogle

Backpropagation in the Simply Typed Lambda-calculus with Linear Negation

15:56 - 16:18
Talk

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

Steffen SmolkaCornell University, Nate FosterCornell University, Justin HsuUniversity of Wisconsin-Madison, USA, Tobias KappéUniversity College London, Dexter KozenCornell University, Alexandra SilvaUniversity College London

Persistency Semantics of the Intel-x86 Architecture

15:35 - 16:40: Research Papers - Concurrency / Memory at Ile de France III (IDF III)
Chair(s): Susmit SarkarUniversity of St. Andrews

15:35 - 15:56
Talk

Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, Germany

Reductions for Safety Proofs

15:56 - 16:18
Talk

Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto

RustBelt Meets Relaxed Memory

16:18 - 16:40
Talk

Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-SWS

16:50 - 19:00: Student Research Competition - SRC Poster Session at SRC

16:50 - 19:00
Poster

SRC Poster Session

16:50 - 17:35: Research Papers - Synthesis and Decision Procedures at Ile de France II (IDF II)
Chair(s): Roopsha SamantaPurdue University

16:50 - 17:12
Talk

Visualization by Example

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

Deciding Memory Safety for Single-Pass Heap-Manipulating Programs

17:12 - 17:35
Talk

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

17:35 - 18:35: Research Papers - Social Hour (Supported by Facebook) at Social Hour

17:35 - 18:35
Social Event

Social Hour (Supported by Facebook)

Thu 23 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

07:45 - 09:00: Mentoring Breakfasts - Thursday Mentoring Breakfast at Breakfast Room

07:45 - 09:00
Social Event

Mentoring BreakfastMentoring Event

09:00 - 10:00: Research Papers - Invited Talk at Ile de France II (IDF II)
Chair(s): Brigitte PientkaMcGill University

09:00 - 10:00
Talk

What is a Secure Programming Language? Invited Talk

Cristina CifuentesOracle Labs

Link to publication Media Attached

10:00 - 10:30: Catering - Thursday Morning Break at Break

10:30 - 11:35: Research Papers - Synthesis 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

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

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

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

10:30 - 11:35: Research Papers - Types and Effects at Ile de France II (IDF II)
Chair(s): Dominique DevrieseVrije Universiteit Brussel

10:30 - 10:51
Talk

Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers

Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław

The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects

10:51 - 11:13
Talk

Pierre-Marie PédrotINRIA, Nicolas TabareauInria

SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References

11:13 - 11:35
Talk

Guilhem JaberLS2N, Université de Nantes

Seminaïve Evaluation for a Higher-Order Functional LanguageDistinguished Paper

11:45 - 12:30: Research Papers - Datalog, OO + Functional Programming at Ile de France III (IDF III)
Chair(s): Brigitte PientkaMcGill University

11:45 - 12:07
Talk

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

David BinderUniversity of Tübingen, Julian JabsUniversity of Tübingen, Ingo SkupinUniversity of Tübingen, Klaus OstermannUniversity of Tübingen, Germany

Fast, Sound, and Effectively Complete Dynamic Race Prediction

11:45 - 12:30: Research Papers - Dynamic Program Analysis at Ile de France II (IDF II)
Chair(s): Peter ThiemannUniversity of Freiburg, Germany

11:45 - 12:07
Talk

Andreas PavlogiannisAarhus University

Link to publication DOI Media Attached File Attached

12:07 - 12:30
Talk

Detecting Floating-Point Errors via Atomic Conditions

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

12:30 - 14:00: Catering - Thursday Lunch at Lunch Room

12:30 - 14:00
Lunch

Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations

14:00 - 15:05: Research Papers - Abstract Interpretation at Ile de France III (IDF III)
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris

14:00 - 14:21
Talk

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

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

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: Student Research Competition - SRC Finalists Presentations at St Jerome

14:00 - 15:30
Talk

SRC Finalists Presentations

14:00 - 15:05: Research Papers - Type Systems 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

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

Julian MackayVictoria University of Wellington, Alex PotaninVictoria University of Wellington, Jonathan AldrichCarnegie Mellon University, Lindsay GrovesVictoria University of Wellington

Dependent Type Systems as Macros

14:43 - 15:05
Talk

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

15:05 - 15:35: Catering - Thursday Afternoon Break at Break

15:35 - 16:40: Research Papers - Probabilistic Programming at Ile de France III (IDF III)
Chair(s): Ohad KammarUniversity of Edinburgh

15:35 - 15:56
Talk

A Language for Probabilistically Oblivious Computation

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

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

Feras SaadMassachusetts Institute of Technology, Cameron FreerMassachusetts Institute of Technology, Martin RinardMIT, Vikash MansinghkaMIT

Link to publication DOI Media Attached File Attached

15:35 - 16:40: Research Papers - Program Logics at Ile de France II (IDF II)
Chair(s): Chung-Kil HurSeoul National University

15:35 - 15:56
Talk

Deductive Verification with Ghost Monitors

Martin ClochardETH Zürich, Claude MarchéInria Saclay & Université Paris-Saclay, Andrei PaskevichLRI, Université Paris-Sud & CNRS

The Next 700 Relational Program Logics

15:56 - 16:18
Talk

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

Peter O'HearnFacebook

Business Meeting & SRC Awards

16:50 - 18:00: Research Papers - Business Meeting & SRC Awards at Ile de France II (IDF II)

16:50 - 18:00
Meeting

Social Hour (Supported by Microsoft)

18:00 - 19:00: Research Papers - Social Hour (Supported by Microsoft) at Social Hour

18:00 - 19:00
Social Event

19:00 - 21:00: W@POPL Dinner - W@POPL Dinner at Palace Cafe

19:00 - 21:00
Dinner

W@POPL DinnerMentoring Event

Fri 24 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

07:45 - 09:00: Mentoring Breakfasts - Friday Mentoring Breakfast at Breakfast Room

07:45 - 09:00
Social Event

Mentoring BreakfastMentoring Event

09:00 - 10:00: Research Papers - Invited Talk at Ile de France II (IDF II)
Chair(s): Lars BirkedalAarhus University

09:00 - 10:00
Talk

Probabilistic ProgrammingInvited Talk

Hongseok YangKAIST

Kind Inference for DatatypesDistinguished Paper

10:00 - 10:30: Catering - Friday Morning Break at Break

10:30 - 11:35: Research Papers - Type Systems at Ile de France II (IDF II)
Chair(s): Dominique DevrieseVrije Universiteit Brussel

10:30 - 10:51
Talk

Ningning XieThe University of Hong Kong, Richard A. EisenbergBryn Mawr College, USA, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong

Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc

10:51 - 11:13
Talk

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

Roland MeyerTU Braunschweig, Sebastian WolffTU Braunschweig

Link to publication DOI Media Attached File Attached

10:30 - 11:35: Research Papers - Verification in Proof Assistants 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

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

Michael SammlerMPI-SWS, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8

Interaction Trees: Representing Recursive and Impure Programs in CoqDistinguished Paper

11:13 - 11:35
Talk

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: Research Papers - Concurrent Programming & Session Types at Ile de France II (IDF II)
Chair(s): Susmit SarkarUniversity of St. Andrews

11:45 - 12:07
Talk

Label-Dependent Session Types

Peter ThiemannUniversity of Freiburg, Germany, Vasco T. VasconcelosUniversity of Lisbon, Portugal

Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

12:07 - 12:30
Talk

Federico AschieriTU Wien, Francesco A. GencoIHPST, Université Paris 1

Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time

11:45 - 12:30: Research Papers - Probabilistic Reasoning and Verification at Ile de France III (IDF III)
Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA

11:45 - 12:07
Talk

Peixin WangShanghai Jiao Tong University, Hongfei FuShanghai Jiao Tong University, Krishnendu ChatterjeeIST Austria, Yuxin DengEast China Normal University, Ming XuEast China Normal University

Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification

12:07 - 12:30
Talk

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: Catering - Friday Lunch at Lunch Room

12:30 - 14:00
Lunch

Stacked Borrows: An Aliasing Model for Rust

14:00 - 15:05: Research Papers - Language Design at Ile de France III (IDF III)
Chair(s): Amin Timanyimec-Distrinet KU-Leuven

14:00 - 14:21
Talk

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

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

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

14:00 - 15:05: Research Papers - Semantics of Probabilistic & Quantum Programming 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

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

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

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

Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper

15:05 - 15:35: Catering - Friday Afternoon Break at Break

15:35 - 16:40: Research Papers - Semantics & Type Theory at Ile de France II (IDF II)
Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA

15:35 - 15:56
Talk

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

Benedikt AhrensUniversity of Birmingham, United Kingdom, André HirschowitzUniversité Côte d'Azur, Ambroise LafontInria, France, Marco MaggesiUniversità di Firenze

Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq

16:18 - 16:40
Talk

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: Research Papers - Verified & Secure Compilation 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

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

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

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: Research Papers - Social Hour (Supported by Tezos) at Social Hour

16:40 - 17:40
Social Event

Social Hour (Supported by Tezos)

Sat 25 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

09:00 - 10:00: WGT - Gradual Criteria at Orleans
Chair(s): Amal AhmedNortheastern University, USA

09:00 - 09:30
Talk

Gradual Typing as if Types Mattered

Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile

Fully Abstract from Static to Gradual

09:30 - 10:00
Talk

Koen JacobsKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Dominique DevrieseVrije Universiteit Brussel

SMTCoq: Safe and efficient automation in Coq (Keynote)

09:00 - 10:00: CoqPL - Invited Talk at Maurepas
Chair(s): Robbert KrebbersDelft University of Technology

09:00 - 10:00
Talk

Chantal KellerLRI, Université Paris-Sud

09:00 - 10:00: Principles of Secure Compilation 2020 - Keynote at Rosalie

09:00 - 09:05
Day opening

PriSC Introduction

Dominique DevrieseVrije Universiteit Brussel

Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing

09:05 - 10:00
Industry talk

Tyler McMullenFastly

Deriving Instances with Dependent Types

10:00 - 10:30: Catering - Saturday Morning Break at Break

10:30 - 12:30: CoqPL - Contributed Talks at Maurepas
Chair(s): Amin Timanyimec-Distrinet KU-Leuven

10:30 - 11:00
Talk

Arthur Azevedo de AmorimCarnegie Mellon University, USA

The use of Coq for Common Criteria Evaluations

11:00 - 11:30
Talk

Yves BertotINRIA, Maxime DénèsInria, Vincent LaporteInria, Arnaud FontaineANSSI, Thomas LetanANSSI

Verifying concurrent Go code in Coq with Goose

11:30 - 12:00
Talk

Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USA

12:00 - 12:30
Talk

A Tutorial on Equations

Matthieu SozeauInria

Exorcising Spectres with Secure Compilers

10:30 - 12:30: Principles of Secure Compilation 2020 - Foundations and timing channels at Rosalie
Chair(s): Marco VassenaCISPA Helmholtz Center for Information Security

10:30 - 10:54
Talk

Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute

Trace-Relating Compiler Correctness and Secure Compilation

10:54 - 11:18
Talk

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

Reconciling progress-insensitive noninterference and declassification

11:18 - 11:42
Talk

Johan BayAarhus University, Aslan AskarovAarhus University

Hermes: Implementing Cryptography without Side-channels

11:42 - 12:06
Talk

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

Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes, David PichardieUniv Rennes, ENS Rennes, IRISA

Gradual Algebraic Data Types

10:30 - 12:30: WGT - Programming features at Orleans
Chair(s): Giuseppe CastagnaCNRS - Université de Paris, France

10:30 - 11:00
Talk

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

Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan

Foreign Function Typing: Semantic Type Soundness for FFIs

11:30 - 12:00
Talk

Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA

Space-Efficient Monotonic References

12:00 - 12:30
Talk

Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA

12:30 - 14:00: Catering - Saturday Lunch at Lunch Room

12:30 - 14:00
Lunch

Hypercoercions and a Framework for Equivalence of Cast Calculi

14:00 - 15:05: WGT - Coercions at Orleans
Chair(s): Jeremy G. SiekIndiana University, USA

14:00 - 14:32
Talk

Kuang-Chen LuIndiana University Bloomington, Jeremy G. SiekIndiana University, USA, Andre KuhlenschmidtIndiana University

Space-Efficient Gradual Typing in Coercion-Passing Style

14:32 - 15:05
Talk

Yuya TsudaKyoto University, Atsushi IgarashiKyoto University, Japan, Tomoya TabuchiKyoto University

Autosubst 2: Mechanising binders in Coq (Keynote)

14:00 - 15:05: CoqPL - Invited Talk at Maurepas
Chair(s): Yves BertotINRIA

14:00 - 15:00
Talk

Kathrin StarkSaarland University, Germany

Exploits as Insecure Compilation

14:00 - 15:05: Principles of Secure Compilation 2020 - New outlooks on secure compilation at Rosalie
Chair(s): Cristina CifuentesOracle Labs

14:00 - 14:24
Talk

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

Marco PatrignaniStanford University & CISPA , Riad S. WahbyStanford University, USA, Robert KünnemannCISPA, Saarland University

Short Talk: Automatically Eliminating Speculative Leaks With Blade

14:48 - 14:56
Talk

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

14:56 - 15:04
Talk

Short Talk: Everparse

Tahina RamananandroMicrosoft Research, n.n.

Gradual Verification of Recursive Heap Data Structures

15:05 - 15:35: Catering - Saturday Afternoon Break at Break

15:35 - 17:45: WGT - Analysis, verification, blame at Orleans
Chair(s): Niki VazouIMDEA Software Institute

15:35 - 16:07
Talk

Jenna WiseCarnegie Mellon University, Johannes BaderFacebook, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Joshua SunshineCarnegie Mellon University

16:07 - 16:40
Talk

Gradual Program Analysis

Samuel EstepLiberty University, Jenna WiseCarnegie Mellon University, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Johannes BaderFacebook, Joshua SunshineCarnegie Mellon University

Blame tracking at higher fidelity

16:40 - 16:50
Break

Minibreak

16:50 - 17:20
Talk

Jakub ZalewskiUniversity of Edinburgh, James McKinnaUniversity of Edinburgh, J. Garrett MorrisUniversity of Kansas, USA, Philip WadlerUniversity of Edinburgh, UK

Discussion on gradual typing and WGT21

17:20 - 17:45
Day closing

15:35 - 17:45: Principles of Secure Compilation 2020 - Compartmentalization, memory safety, and isolation at Rosalie
Chair(s): Marco PatrignaniStanford University & CISPA , Jonathan ProtzenkoMicrosoft Research, Redmond

15:35 - 15:59
Talk

Flexible Tag-based Policies for Compartmentalized C

Sean AndersonPortland State University, Andrew TolmachPortland State University, Chris ChhakPortland State University

Mechanized Reasoning about a Capability Machine

15:59 - 16:23
Talk

Aina Linn GeorgesAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University

Securing Interruptible Enclaves

16:23 - 16:47
Talk

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

WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing

16:47 - 16:57
Break

Mini-break

16:57 - 17:21
Talk

Jay BosamiyaCarnegie Mellon University, Benjamin LimCarnegie Mellon University, Bryan ParnoCarnegie Mellon University

Memory Safety Preservation for WebAssembly

17:21 - 17:45
Talk

Marco VassenaCISPA Helmholtz Center for Information Security, Marco PatrignaniStanford University & CISPA

Link to publication Media Attached File Attached

15:35 - 17:45: CoqPL - Contributed Talks & Coq Developers at Maurepas
Chair(s): Joseph TassarottiBoston College, Robbert KrebbersDelft University of Technology

15:35 - 16:05
Talk

Towards Formally Verified Just-in-Time compilation

Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes- IRISA, David PichardieUniv Rennes, ENS Rennes, IRISA

A Coq Library of Undecidable Problems

16:05 - 16:35
Talk

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