Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

Dates
Rooms
Tracks
Badges
Your Program
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sun 13 Jan

Displayed time zone: Belfast change

08:30 - 10:30
Session 1BEAT at Sala VII
Chair(s): Philip Wadler University of Edinburgh, UK
08:30
10m
Day opening
Opening
BEAT
Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. Pérez University of Groningen, The Netherlands
08:40
50m
Talk
Invited Talk: Gradual Session Types — an Ongoing Journey
BEAT
Peter Thiemann University of Freiburg, Germany
09:30
20m
Talk
Gradual Session Types in Imperative Style
BEAT
Kaede Kobayashi Kyoto University, Atsushi Igarashi Kyoto University, Japan
09:50
20m
Talk
Checking the Equivalence of Context-Free Session Types
BEAT
Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon
File Attached
10:10
20m
Talk
Effpi: Concurrent Programming with Dependent Behavioural Types
BEAT
Alceste Scalas Imperial College London, Elias Benussi Imperial College London, Nobuko Yoshida Imperial College London
File Attached
09:00 - 10:30
Invited Talk 1VMCAI at Sala III
Chair(s): Constantin Enea Université Paris Diderot
09:00
90m
Talk
Under and Over Approximated Reachability Analysis for the Verifcation of Control Systems
VMCAI
Sylvie Putot École Polytechnique
09:00 - 10:30
Session 1PriSC at Sala VI
Chair(s): Deepak Garg Max Planck Institute for Software Systems
09:00
60m
Talk
PriSC Keynote - Jasmin: A Compiler and Framework for High-Assurance and High-Speed Cryptography
PriSC
File Attached
10:00
30m
Talk
Towards Secure Compilation of Power Side-Channel Countermeasures
PriSC
Marc Gourjon Hamburg University of Technology and NXP Semiconductors Germany GmbH
File Attached
11:00 - 12:30
Session 2PriSC at Sala VI
Chair(s): Dominique Devriese Vrije Universiteit Brussel, Belgium
11:00
30m
Talk
Trestle: Bridging the Performance and Safety Divide in WebAssembly
PriSC
Craig Disselkoen University of California San Diego, Tal Garfinkel Stanford University, Deian Stefan University of California San Diego, Conrad Watt University of Cambridge
File Attached
11:30
30m
Talk
Protecting C++ Applications Using CHERI
PriSC
Khilan Gudka University of Cambridge, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge
File Attached
12:00
30m
Talk
Secure Linking in the CheriBSD Operating System
PriSC
Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge
File Attached
11:00 - 12:30
Session 2BEAT at Sala VII
Chair(s): Dominic Orchard University of Kent, UK
11:00
50m
Talk
Invited Talk: On Type-Based Complexity Analysis of Programs and Processes
BEAT
Ugo Dal Lago University of Bologna, Italy / Inria, France
11:50
20m
Talk
Global Types with Internal Delegation
BEAT
Ilaria Castellani INRIA Sophia Antipolis, France, Mariangiola Dezani Università di Torino, Paola Giannini Universita' del Piemonte Orientale, Ross Horne Computer Science and Communications Research Unit, University of Luxembourg
File Attached
12:10
20m
Talk
Two Declarative Approaches for Session-Based Concurrency
BEAT
12:30 - 14:00
Sunday LunchWorkshops at Lunch Room
12:30
90m
Lunch
Lunch
Workshops

13:30 - 15:30
Session 3BEAT at Sala VII
Chair(s): Paola Giannini Universita' del Piemonte Orientale
13:30
50m
Talk
Invited Talk: Resource-Aware Session Types
BEAT
Jan Hoffmann Carnegie Mellon University
14:20
50m
Talk
Invited Talk: A Session Type Provider: Compile-time Generation of Session Types with Interaction Refinements
BEAT
Rumyana Neykova Brunel University London
File Attached
15:10
20m
Talk
Getting Rid of Null-Dereferences – Behavioural Types to the Rescue
BEAT
Hans Hüttel Department of Computer Science, Aalborg University, Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Adrian Francalanza University of Malta, Mario Bravetti Università di Bologna
File Attached
14:00 - 15:30
Program SynthesisVMCAI at Sala III
Chair(s): Nuno P. Lopes Microsoft Research
14:00
30m
Talk
Minimal Synthesis of String To String Functions From Examples
VMCAI
Jad Hamza LIAFA, Université Paris Diderot, Viktor Kunčak EPFL, Switzerland
14:30
30m
Talk
Lazy but Effective Functional Synthesis
VMCAI
Grigory Fedyukovich Princeton University, Arie Gurfinkel University of Waterloo, Aarti Gupta Princeton University
15:00
30m
Talk
Automatic Program Repair using Formal Verification and Expression Templates
VMCAI
Thanh-Toan Nguyen , Quang-Trung Ta National University of Singapore, Wei-Ngan Chin National University of Singapore
14:00 - 15:30
Session 3PriSC at Sala VI
Chair(s): Chung-Kil Hur Seoul National University
14:00
30m
Talk
Translation Validation for Security Properties
PriSC
Matteo Busi Università di Pisa - Dipartimento di Informatica, Pierpaolo Degano Università di Pisa - Dipartimento di Informatica, Letterio Galletta IMT School for Advanced Studies
Pre-print File Attached
14:30
30m
Talk
Security Witnesses for Compiler Transformations
PriSC
Kedar Namjoshi Bell Labs, Nokia, Lucas M. Tabajara Rice University
File Attached
15:00
30m
Talk
A Data Layout Description Language for Cogent
PriSC
Zilin Chen Data61, CSIRO and UNSW, Matthew Di Meglio UNSW, Liam O'Connor UNSW, Partha Susarla Data61, CSIRO, Christine Rizkallah UNSW, Gabriele Keller Utrecht University
16:00 - 17:30
Abstract Interpretation (2)VMCAI at Sala III
Chair(s): Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France
16:00
30m
Talk
Demand Control-Flow Analysis
VMCAI
Kimball Germane University of Utah, Jay McCarthy University of Massachusetts Lowell, Michael D. Adams University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School
16:30
30m
Talk
Effect-driven Flow Analysis
VMCAI
Jens Nicolay Vrije Universiteit Brussel, Belgium, Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
17:00
30m
Talk
Relatively Complete Pushdown Analysis of Escape Continuations
VMCAI
Kimball Germane University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School
16:00 - 18:00
Session 4PriSC at Sala VI
Chair(s): David Naumann Stevens Institute of Technology, Aslan Askarov Aarhus University
16:00
30m
Other
Short Talks Session
PriSC

16:30
30m
Talk
Modular Security Guarantees for Low-Level Languages with Stack Traversal
PriSC
Mathias Vorreiter Pedersen Aarhus University, Aslan Askarov Aarhus University
File Attached
17:00
30m
Talk
Confidentiality-Preserving Refinement
PriSC
File Attached
17:30
30m
Talk
(Un)Encrypted Computing and Indistinguishability Obfuscation
PriSC
Peter Breuer Hecusys LLC, Jonathan Bowen London South Bank University
File Attached
16:00 - 18:25
Session 4BEAT at Sala VII
Chair(s): Adrian Francalanza University of Malta, Jorge A. Pérez University of Groningen, The Netherlands
16:00
50m
Talk
Invited Talk: Session Types for Fault-Tolerant Distributed Algorithms
BEAT
Kirstin Peters TU Berlin
16:50
20m
Talk
Behavioral Types as a Semantic Foundation for the GDPR Notion of Purpose
BEAT
Evangelia Vanezi University of Cyprus, Dimitrios Kouzapas University of Cyprus, Anna Philippou University of Cyprus
17:10
20m
Talk
Relating Process Languages for Security and Communication Correctness
BEAT
Daniele Nantes-Sobrinho University of Brasília, Brazil, Jorge A. Pérez University of Groningen, The Netherlands
17:30
10m
Break
Short break
BEAT

17:40
20m
Talk
Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs
BEAT
Søren Debois IT University of Copenhagen, Thomas H. Hildebrandt , Hugo López IT University of Copenhagen, Denmark & DCR Solutions A/S
Media Attached
18:00
20m
Talk
Hardware Interactions as Behavioural Types
BEAT
Carlos Mão de Ferro LASIGE, Faculty of Sciences, University of Lisbon, Francisco Martins LaSIGE, University of Lisbon, Tiago Cogumbreiro University of Massachusetts Boston
File Attached
18:20
5m
Day closing
Closing
BEAT
Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. Pérez University of Groningen, The Netherlands

Mon 14 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 2VMCAI at Sala III
Chair(s): Lenore Zuck
09:00
90m
Talk
Designing Self-Certifying Software Systems
VMCAI
Kedar Namjoshi Bell Labs, Nokia
09:00 - 10:30
Tutorial 4ATutorialFest at Sala IX
09:00
90m
Talk
[T4] Programming Cyber-Physical Systems with Logic
TutorialFest
André Platzer Carnegie Mellon University
09:00 - 10:30
Tutorial 1ATutorialFest at Sala V
09:00
90m
Talk
[T1] QuickChick: Property-Based Testing in Coq
TutorialFest
Benjamin C. Pierce University of Pennsylvania, Leonidas Lampropoulos University of Pennsylvania
09:00 - 10:30
Tutorial 3ATutorialFest at Sala VI
09:00
90m
Talk
[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
TutorialFest
Dominic Orchard University of Kent, UK, Harley D. Eades III Augusta University, Vilem-Benjamin Liepelt University of Kent, UK
09:00 - 10:30
Session TypesOPCT at Sala VII
Chair(s): Ilaria Castellani INRIA Sophia Antipolis, France
09:00
15m
Day opening
Opening
OPCT

09:15
25m
Talk
A Concurrent Functional Language with Session Types and Control Effects Based on Linear Logic
OPCT
Luís Caires NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
09:40
25m
Talk
A Foundation for Runtime Enforcement
OPCT
Adrian Francalanza University of Malta
10:05
25m
Talk
Processes as Names?
OPCT
Hans Hüttel Department of Computer Science, Aalborg University
File Attached
09:00 - 10:30
Tutorial 2ATutorialFest at Sala VIII
09:00
90m
Talk
[T2] Engineering Distributed Systems via Protocols and Commitments
TutorialFest
Amit Chopra Lancaster University, UK, Munindar P. Singh North Carolina State University
09:00 - 10:30
Keynote 1 and Research PaperCPP at Sala XII
Chair(s): Magnus O. Myreen Chalmers University of Technology, Sweden
09:00
60m
Talk
A Linear Logical Framework in Hybrid
CPP
Amy Felty University of Ottawa
DOI
10:00
30m
Research paper
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
CPP
Yannick Forster Saarland University, Dominique Larchey-Wendling CNRS, LORIA
DOI
11:00 - 12:30
Decision ProceduresVMCAI at Sala III
Chair(s): Kedar Namjoshi Bell Labs, Nokia
11:00
30m
Talk
Solving and Interpolating Constant Arrays Based on Weak Equivalences
VMCAI
Jochen Hoenicke Universität Freiburg, Tanja Schindler University of Freiburg
11:30
30m
Talk
A Decidable Logic for Tree Data-Structures with Measurements
VMCAI
Xiaokang Qiu Purdue University, Yanjun Wang Purdue University
File Attached
12:00
30m
Talk
A Practical Algorithm for Structure Embedding
VMCAI
Charlie Murphy Princeton University, Zachary Kincaid Princeton University
File Attached
11:00 - 12:30
Tutorial 4BTutorialFest at Sala IX
11:00
90m
Talk
[T4] Programming Cyber-Physical Systems with Logic
TutorialFest
André Platzer Carnegie Mellon University
11:00 - 12:30
Tutorial 1BTutorialFest at Sala V
11:00
90m
Talk
[T1] QuickChick: Property-Based Testing in Coq
TutorialFest
Benjamin C. Pierce University of Pennsylvania, Leonidas Lampropoulos University of Pennsylvania
11:00 - 12:30
Tutorial 3BTutorialFest at Sala VI
11:00
90m
Talk
[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
TutorialFest
Dominic Orchard University of Kent, UK, Harley D. Eades III Augusta University, Vilem-Benjamin Liepelt University of Kent, UK
11:00 - 12:30
Tutorial 2BTutorialFest at Sala VIII
11:00
90m
Talk
[T2] Engineering Distributed Systems via Protocols and Commitments
TutorialFest
Amit Chopra Lancaster University, UK, Munindar P. Singh North Carolina State University
11:00 - 12:30
Session 1PEPM at Sala X
Chair(s): Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM)
11:00
5m
Day opening
Welcome to PEPM19
PEPM
C: Atsushi Igarashi Kyoto University, Japan, C: Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM)
11:05
55m
Talk
Applying Futamura Projections to Compose Languages and Tools in GraalVM (Invited Talk)
PEPM
Christian Humer Oracle Labs, Switzerland
File Attached
12:00
30m
Talk
A Simpler Lambda Calculus
PEPM
Barry Jay University of Technology Sydney
DOI
11:00 - 12:30
Research Papers: Proof Theory, Theory of Programming LanguagesCPP at Sala XII
Chair(s): Assia Mahboubi INRIA
11:00
30m
Research paper
A Proof-Theoretic Approach to Certifying Skolemization
CPP
Kaustuv Chaudhuri Inria, France, Matteo Manighetti Inria & École Polytechnique, Dale Miller INRIA Saclay and LIX
DOI
11:30
30m
Research paper
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
CPP
Yannick Forster Saarland University, Steven Schäfer Saarland University, Simon Spies Saarland University, Kathrin Stark Saarland University, Germany
DOI
12:00
30m
Research paper
Eliminating Reflection from Type Theory
CPP
Theo Winterhalter Gallinette / Inria / LS2N, Nicolas Tabareau Inria, Matthieu Sozeau Inria
DOI
11:15 - 12:30
Causality, ReversibilityOPCT at Sala VII
Chair(s): Thomas H. Hildebrandt
11:15
25m
Talk
Causal Reasoning for Safety
OPCT
Georgiana Caltais University of Konstanz
File Attached
11:40
25m
Talk
A Calculus of Branching Processes
OPCT
12:05
25m
Talk
An Axiomatic Approach to Reversible Computation
OPCT
Irek Ulidowski University of Leicester
12:30 - 14:00
Monday LunchWorkshops at Lunch Room
12:30
90m
Lunch
Lunch
Workshops

13:50 - 15:30
Session Types, Graph-RewritingOPCT at Sala VII
Chair(s): Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS
13:50
25m
Talk
Taming Concurrency for Verification using Multiparty Session Types
OPCT
Kirstin Peters TU Berlin
14:15
25m
Talk
From Testing Preorders to Flaky Tests
OPCT
Giovanni Bernardi Université Paris Diderot
File Attached
14:40
25m
Talk
Multiparty Reactive Sessions
OPCT
Cinzia Di Giusto Laboratoire I3S
File Attached
15:05
25m
Talk
Independence, Concurrency and Abstraction in Graph-Rewriting Processes
OPCT
14:00 - 15:30
Probabilistic SystemsVMCAI at Sala III
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
14:00
30m
Talk
Syntactic Partial Order Compression for Probabilistic Reachability
VMCAI
Gereon Fox , Daniel Stan , Holger Hermanns Saarland University
14:30
30m
Talk
Termination of Nondeterministic Probabilistic Programs
VMCAI
Hongfei Fu IST Austria, Krishnendu Chatterjee IST Austria
15:00
30m
Talk
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
VMCAI
Stefan Haar , Juraj Kolčák LSV, CNRS & ENS Cachan, University Paris Saclay, Loïc Paulevé
14:00 - 15:30
PADL Session 1PADL at Sala IV
13:50
10m
Day opening
PADL Opening and Welcome
PADL
Moa Johansson Chalmers University of Technology, José Julio Alferes NOVA LINCS -- Universidade Nova de Lisboa
14:00
30m
Talk
Natural Language Generation From Ontologies
PADL
14:30
30m
Talk
Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP
PADL
Joaquín Arias , Manuel Carro IMDEA Software Institute and T.U. of Madrid (UPM)
File Attached
15:00
30m
Talk
Improving Residuation in Declarative Programs
PADL
Michael Hanus Kiel University
File Attached
14:00 - 15:30
Tutorial 7ATutorialFest at Sala IX
14:00
90m
Talk
[T7] Higher-Order Probabilistic Programming
TutorialFest
Ugo Dal Lago University of Bologna, Italy / Inria, France
Pre-print
14:00 - 15:30
Tutorial 5ATutorialFest at Sala V
14:00
90m
Talk
[T5] Correct-by-Construction Programming in Agda
TutorialFest
Andreas Abel Gothenburg University, Jesper Cockx Chalmers | University of Gothenburg
14:00 - 15:30
Tutorial 8ATutorialFest at Sala VI
14:00
90m
Talk
[T8] Building Your Own Modular Static Analyser with Infer
TutorialFest
Jules Villard Facebook London, Ezgi Çiçek Facebook London, Mehdi Bouaziz Facebook London, Nikos Gorogiannis
14:00 - 15:30
Tutorial 6ATutorialFest at Sala VIII
14:00
90m
Talk
[T6] Session-Typed Concurrent Programming
TutorialFest
Stephanie Balzer Carnegie Mellon University, USA
14:00 - 15:30
Session 2PEPM at Sala X
Chair(s): Thomas P. Jensen INRIA Rennes
14:00
30m
Talk
Method Name Suggestion with Hierarchical Attention Networks
PEPM
Sihan Xu Nankai University, China, Sen Zhang Nankai University, China, Weijing Wang Nankai University, China, Xinya Cao Nankai University, China, Chenkai Guo Nankai University, China, Jing Xu Nankai University, China
DOI
14:30
30m
Talk
Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking
PEPM
Keiichi Watanabe University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Hiroki Oshikawa University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan
DOI
15:00
30m
Talk
Typed Parsing and Unparsing for Untyped Regular Expression Engines
PEPM
Gabriel Radanne University of Freiburg, Germany
DOI Pre-print File Attached
14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Chris Hawblitzel Microsoft Research
14:00
30m
Research paper
Formally Verified Big Step Semantics out of x86-64 Binaries
CPP
Ian Roessle Virginia Tech, USA, Freek Verbeek Open University of the Netherlands, The Netherlands, Binoy Ravindran Virginia Tech
DOI
14:30
30m
Research paper
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
CPP
Sandrine Blazy Univ Rennes- IRISA, Rémi Hutin IRISA / ENS Rennes
DOI
15:00
30m
Research paper
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
CPP
Nicolas Koh , Yao Li University of Pennsylvania, Yishuai Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Lennart Beringer Princeton University, Wolf Honore , William Mansky University of Illinois at Chicago, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI
16:00 - 17:30
PADL Session 2PADL at Sala IV
16:00
30m
Talk
Faster Coroutine Pipelines: A Reconstruction
PADL
16:30
30m
Talk
Distributed Protocol Combinators
PADL
Kristoffer Just Arndal Andersen Aarhus University, Ilya Sergey Yale-NUS College and National University of Singapore
Pre-print
17:00
30m
Talk
Classes of Arbitrary Kind
PADL
Alejandro Serrano Utrecht University, Netherlands, Victor Cacciari Miraldo Utrecht University, Netherlands
Link to publication DOI File Attached
16:00 - 17:30
Tutorial 7BTutorialFest at Sala IX
16:00
90m
Talk
[T7] Higher-Order Probabilistic Programming
TutorialFest
Ugo Dal Lago University of Bologna, Italy / Inria, France
Pre-print
16:00 - 17:30
Tutorial 5BTutorialFest at Sala V
16:00
90m
Talk
[T5] Correct-by-Construction Programming in Agda
TutorialFest
Andreas Abel Gothenburg University, Jesper Cockx Chalmers | University of Gothenburg
16:00 - 17:30
Tutorial 8BTutorialFest at Sala VI
16:00
90m
Talk
[T8] Building Your Own Modular Static Analyser with Infer
TutorialFest
Jules Villard Facebook London, Ezgi Çiçek Facebook London, Mehdi Bouaziz Facebook London, Nikos Gorogiannis
16:00 - 17:15
Concurrent Programming, Memory ModelsOPCT at Sala VII
Chair(s): Gustavo Petri IRIF, Université Paris Diderot
16:00
25m
Talk
Linearizability in the Context of Weak Memory Models
OPCT
Kirsten Winter The University of Queensland
File Attached
16:25
25m
Talk
IPA: Invariant-preserving Applications for Weakly Consistent Replicated Databases
OPCT
Carla Ferreira Universidade Nova Lisboa
16:50
25m
Talk
Compositional Reasoning for Termination of Fine-grained Concurrent Programs
OPCT
Emanuele D'Osualdo Imperial College London, UK
Pre-print File Attached
16:00 - 17:30
Tutorial 6BTutorialFest at Sala VIII
16:00
90m
Talk
[T6] Session-Typed Concurrent Programming
TutorialFest
Stephanie Balzer Carnegie Mellon University, USA
16:00 - 17:30
Session 3PEPM at Sala X
Chair(s): Atsushi Igarashi Kyoto University, Japan
16:00
60m
Talk
What Is the Type of a Partial Evaluator? (Invited Talk)
PEPM
Jens Palsberg University of California, Los Angeles (UCLA)
File Attached
17:00
30m
Talk
Combining Higher-Order Model Checking with Refinement Type Inference
PEPM
Ryosuke Sato Kyushu University, Japan, Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan
DOI
16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Georges Gonthier Inria
16:00
30m
Research paper
A Formal Proof of Hensel's Lemma over the p-adic Integers
CPP
Robert Y. Lewis Vrije Universiteit Amsterdam
DOI
16:30
30m
Research paper
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
CPP
Wenda Li University of Cambridge, Lawrence Paulson University of Cambridge
DOI
17:00
30m
Research paper
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
CPP
DOI
17:30 - 18:30
Monday Social HourWorkshops at Galeria
17:30
60m
Social Event
Social Hour
Workshops

Tue 15 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Invited Talk 3VMCAI at Sala III
Chair(s): Ruzica Piskac Yale University, USA
09:00
90m
Talk
Semantics for Compiler IRs: Undefined Behavior is not Evil!
VMCAI
Nuno P. Lopes Microsoft Research
Media Attached
09:00 - 10:30
Keynote 2 and Research PaperCPP at Sala XII
Chair(s): Assia Mahboubi INRIA
09:00
60m
Talk
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
CPP
Jasmin Blanchette Vrije Universiteit Amsterdam
DOI
10:00
30m
Research paper
A Verified Prover Based on Ordered Resolution
CPP
Anders Schlichtkrull Technical University of Denmark, Jasmin Blanchette Vrije Universiteit Amsterdam, Dmitriy Traytel ETH Zurich
DOI
11:00 - 12:30
PLMW Session 2PLMW at Sala II
11:00
30m
Talk
Research Skills: How to Choose Research Areas
PLMW
Catuscia Palamidessi INRIA and LIX
Pre-print File Attached
11:30
60m
Talk
Panel: Grad School and Beyond
PLMW
Dominic Orchard University of Kent, UK, Jorge A. Pérez University of Groningen, The Netherlands, Azalea Raad MPI-SWS, Germany, Max New Northeastern University, Stephanie Balzer Carnegie Mellon University, USA
Pre-print
11:00 - 12:30
Software Verification and SynthesisVMCAI at Sala III
Chair(s): Ori Lahav Tel Aviv University
11:00
30m
Talk
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
VMCAI
Viorel Preoteasa , Iulia Dragomir , Stavros Tripakis Aalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
11:30
30m
Talk
euforia: Complete Software Model Checking with Uninterpreted Functions
VMCAI
12:00
30m
Talk
Program Synthesis with Equivalence Reduction
VMCAI
Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison
11:00 - 12:30
BLAFI at Sala VI
Chair(s): Steven Holtzen University of California, Los Angeles
11:00
30m
Talk
The Geometry of Bayesian Programming
LAFI
Ugo Dal Lago University of Bologna, Italy / Inria, France, Naohiko Hoshino Kyoto University
11:30
30m
Talk
Model and Inference Combinators for Deep Probabilistic Programming
LAFI
Eli Sennesh Northeastern University, Adam Ścibior University of Cambridge and MPI Tuebingen, Hao Wu Northeastern University, Jan-Willem van de Meent Northeastern University
File Attached
12:00
30m
Talk
Server-side Probabilistic Programming
LAFI
Media Attached
11:00 - 12:30
Session 4PEPM at Sala X
Chair(s): Roberto Giacobazzi University of Verona and IMDEA Software Institute
11:00
60m
Talk
Making Proofs Easy: Horn Clause Transformations to the Aid of Program Verification (Invited Talk)
PEPM
File Attached
12:00
30m
Talk
Control Flow Obfuscation via CPS Transformation
PEPM
Kenny Zhuo Ming Lu Nanyang Polytechnic, Singapore
DOI
11:00 - 12:30
Research Papers: Rewriting, Automated ReasoningCPP at Sala XII
Chair(s): Andrei Popescu Middlesex University, London
11:00
30m
Research paper
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
CPP
Kathrin Stark Saarland University, Germany, Steven Schäfer Saarland University, Jonas Kaiser
DOI
11:30
30m
Research paper
Certified ACKBO
CPP
Alexander Lochmann , Christian Sternagel University of Innsbruck, Austria
DOI
12:00
30m
Research paper
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
CPP
DOI
11:15 - 12:30
Cyberphysical Systems, Hybrid SystemsOPCT at Sala VII
Chair(s): Philippa Gardner Imperial College London
11:15
25m
Talk
Hybrid Systems Reachability Analysis
OPCT
Erika Abraham RWTH Aachen University
11:40
25m
Talk
Attribute Based Communication for Collective Adaptive Systems
OPCT
12:05
25m
Talk
Designing Resilient Large Scaled CPS: Models, Languages and Tools
OPCT
Michele Loreti University of Camerino
12:30 - 14:00
Tuesday LunchWorkshops at Lunch Room
12:30
90m
Lunch
Lunch
Workshops

14:00 - 15:30
PLMW Session 3PLMW at Sala II
14:00
45m
Talk
Technical Talk: How to Think about Types
PLMW
Frank Pfenning Carnegie Mellon University, USA
Pre-print File Attached
14:45
45m
Talk
Technical Talk: What Is Programming Languages Research?
PLMW
Michael Hicks University of Maryland, College Park
Pre-print File Attached
14:00 - 15:30
Software VerificationVMCAI at Sala III
Chair(s): Grigory Fedyukovich Princeton University
14:00
30m
Talk
Type-directed Bounding of Collections in Reactive Programs
VMCAI
Tianhan Lu University of Colorado Boulder, Pavol Cerny University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder, Ashutosh Trivedi
14:30
30m
Talk
Exploiting Pointer Analysis in Memory Models for Deductive Verification
VMCAI
Quentin Bouillaguet , François Bobot CEA, Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France, Boris Yakobowski CEA - LIST
File Attached
15:00
30m
Talk
Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
VMCAI
Anja Karl Institute of Applied Information Processing and Communications, Graz University of Technology, Robert Schilling , Roderick Bloem Institute of Software Technology, Graz University of Technology , Stefan Mangard
14:00 - 15:30
PADL Session 5PADL at Sala IV
14:00
30m
Talk
Composing Syntactical Constructs to Create Domain-Specific Languages
PADL
David Broman KTH Royal Institute of Technology, Viktor Palmkvist KTH Royal Institute of Technology
DOI Media Attached
14:30
30m
Talk
Proof Carrying Plans
PADL
Christopher Schwaab University of St Andrews, Ekaterina Komendantskaya Heriot-Watt University, UK, Alasdair Hill , Frantisek Farka , Ron Petrick , Joe Wells , Kevin Hammond University of St. Andrews, UK
15:00
30m
Talk
A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers
PADL
Paul Tarau University of North Texas
14:00 - 15:30
Session 5PEPM at Sala X
Chair(s): Alberto Pettorossi University of Rome Tor Vergata, Italy
14:00
30m
Talk
Extracting a Call-by-Name Partial Evaluator from a Proof of Termination
PEPM
Kenichi Asai Ochanomizu University
DOI File Attached
14:30
30m
Talk
Futures and Promises in Haskell and Scala
PEPM
Tamino Dauth Karlsruhe University of Applied Sciences, Germany, Martin Sulzmann Karlsruhe University of Applied Sciences, Germany
DOI File Attached
15:00
28m
Talk
Generating Mutually Recursive Definitions
PEPM
Jeremy Yallop University of Cambridge, UK, Oleg Kiselyov
DOI Pre-print
15:28
2m
Poster
Advanced Futures and Promises in C++ (poster)
PEPM
Tamino Dauth Karlsruhe University of Applied Sciences, Germany, Martin Sulzmann Karlsruhe University of Applied Sciences, Germany
14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Nicolas Tabareau Inria
14:00
30m
Research paper
A Verified Protocol Buffer Compiler
CPP
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
DOI
14:30
30m
Research paper
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
CPP
Véronique Benzaken LRI, Université Paris-Sud, Evelyne Contejean
DOI
15:00
30m
Research paper
Dynamic Class Initialization Semantics: a Jinja Extension
CPP
Susannah Mansky , Elsa Gunter University of Illinois
DOI
16:00 - 17:30
PLMW Session 4PLMW at Sala II
16:00
30m
Talk
Research Skills: How to Bootstrap a Research Project
PLMW
Ilya Sergey Yale-NUS College and National University of Singapore
Pre-print File Attached
16:30
60m
Talk
Panel: How to Do Good PL Research
PLMW
Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon, Deepak Garg Max Planck Institute for Software Systems, Philippa Gardner Imperial College London, Atsushi Igarashi Kyoto University, Japan, Neel Krishnaswami Computer Laboratory, University of Cambridge
Pre-print
16:00 - 17:30
Networks and ConcurrencyVMCAI at Sala III
Chair(s): Cezara Drăgoi INRIA, ENS, CNRS
16:00
30m
Talk
On the Semantics of Snapshot Isolation
VMCAI
Azalea Raad MPI-SWS, Germany, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
16:30
30m
Talk
Fast BGP Simulation of Large Datacenters
VMCAI
Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research
Pre-print
17:00
30m
Talk
Parametric Timed Broadcast Protocols
VMCAI
Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye , Paulin Fournier , Didier Lime
File Attached
16:00 - 17:30
16:00
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
LAFI
Simon Castellan , Hugo Paquet University of Cambridge
16:30
30m
Talk
Factorized Exact Inference for Discrete Probabilistic Programs
LAFI
Steven Holtzen University of California, Los Angeles, Joe Qian University of California, Los Angeles, Todd Millstein University of California, Los Angeles, Guy Van den Broeck University of California, Los Angeles
17:00
30m
Talk
Verified Equational Reasoning on a Little Language of Measures
LAFI
Matthew Heimerdinger Indiana University, Chung-chieh Shan Indiana University, USA
16:00 - 17:20
Algebra, CoalgebraOPCT at Sala VII
Chair(s): Alexandra Silva University College London
16:00
25m
Talk
Coalgebra Learning via Duality
OPCT
Jurriaan Rot Radboud University Nijmegen
16:25
25m
Talk
A Metric Semantics for Coordination Languages
OPCT
Valentina Castiglioni Inria Saclay - Ile de France
File Attached
16:50
25m
Talk
Hybrid System Iteration
OPCT
Renato Neves University of Minho & INESC TEC
File Attached
17:15
5m
Day closing
Closing
OPCT

16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Zhong Shao Yale University
16:00
30m
Research paper
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
CPP
Yannick Forster Saarland University, Dominik Kirst Saarland University, Gert Smolka Saarland University
DOI
16:30
30m
Research paper
Verified Solving and Asymptotics of Linear Recurrences
CPP
Manuel Eberl Technische Universität München
DOI
17:00
30m
Meeting
Business Meeting
CPP
Assia Mahboubi INRIA, Magnus O. Myreen Chalmers University of Technology, Sweden
17:30 - 18:30
Tuesday Social HourWorkshops at Galeria
17:30
60m
Social Event
Social Hour
Workshops

Wed 16 Jan

Displayed time zone: Belfast change

09:00 - 10:05
Welcome & Keynote IResearch Papers at Sala I + II
Chair(s): Peter O'Hearn Facebook
09:00
5m
Day opening
Welcome
Research Papers
Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU), Stephanie Weirich University of Pennsylvania, USA
Media Attached
09:05
60m
Talk
Automated Fault-Finding and Fixing at Facebook
Research Papers
Mark Harman Facebook and University College London
Media Attached
10:35 - 12:03
Reasoning about Probabilistic ProgramsResearch Papers at Sala I
Chair(s): Jan Hoffmann Carnegie Mellon University
10:35
22m
Talk
Formal Verification of Higher-Order Probabilistic Programs
Research Papers
Tetsuya Sato University at Buffalo, SUNY, USA, Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Justin Hsu University of Wisconsin-Madison, USA
Link to publication DOI Media Attached File Attached
10:57
22m
Talk
A Separation Logic for Concurrent Randomized Programs
Research Papers
Joseph Tassarotti Carnegie Mellon University, Robert Harper
Link to publication DOI Media Attached File Attached
11:19
22m
Talk
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Research Papers
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University
Link to publication DOI Media Attached File Attached
11:41
22m
Talk
Trace Abstraction Modulo Probability
Research Papers
Calvin Smith University of Wisconsin - Madison, Justin Hsu University of Wisconsin-Madison, USA, Aws Albarghouthi University of Wisconsin-Madison
Link to publication DOI Media Attached
10:35 - 12:03
ConcurrencyResearch Papers at Sala II
Chair(s): Ori Lahav Tel Aviv University
10:35
22m
Talk
A True Positives Theorem for a Static Race Detector
Research Papers
Nikos Gorogiannis , Peter W. O'Hearn Facebook and University College London, Ilya Sergey Yale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
10:57
22m
Talk
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Research Papers
Roland Meyer , Sebastian Wolff TU Braunschweig
Link to publication DOI Pre-print Media Attached File Attached
11:19
22m
Talk
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Research Papers
Klaus v. Gleissenthall University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Alexander Bakst , Deian Stefan University of California San Diego, Ranjit Jhala University of California, San Diego
Link to publication DOI Media Attached
11:41
22m
Talk
Weak-Consistency Specification via Visibility Relaxation
Research Papers
Michael Emmi SRI International, Constantin Enea Université Paris Diderot
Link to publication DOI Media Attached File Attached
12:03 - 13:45
Wednesday LunchResearch Papers at Lunch Room
12:03
1h42m
Lunch
Lunch
Research Papers

13:45 - 14:51
Probabilistic Programming and SemanticsResearch Papers at Sala I
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
13:45
22m
Talk
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
Research Papers
Maria I. Gorinova The University of Edinburgh, Andrew D. Gordon Microsoft Research and University of Edinburgh, Charles Sutton University of Edinburgh
Link to publication DOI Pre-print Media Attached File Attached
14:07
22m
Talk
A Domain Theory for Statistical Probabilistic ProgrammingDistinguished Paper
Research Papers
Matthijs Vákár University of Oxford, Ohad Kammar University of Edinburgh, Sam Staton University of Oxford
Link to publication DOI Pre-print Media Attached File Attached
14:29
22m
Talk
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Research Papers
Feras Saad Massachusetts Institute of Technology, Marco Cusumano-Towner MIT-CSAIL, Ulrich Schaechtle Massachusetts Institute of Technology, USA, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka MIT
Link to publication DOI Media Attached File Attached
13:45 - 14:51
CategoriesResearch Papers at Sala II
Chair(s): Nicolas Tabareau Inria
13:45
22m
Talk
Familial Monads and Structural Operational Semantics
Research Papers
Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry
Link to publication DOI Media Attached File Attached
14:07
22m
Talk
Bindings as Bounded Natural Functors
Research Papers
Jasmin Blanchette Vrije Universiteit Amsterdam, Lorenzo Gheri Middlesex University London, Andrei Popescu Middlesex University, London, Dmitriy Traytel ETH Zurich
Link to publication DOI Media Attached File Attached
14:29
22m
Talk
Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Research Papers
Paul-André Melliès CNRS and University Paris Diderot
Link to publication DOI Media Attached File Attached
15:21 - 16:27
Machine Learning and Linear AlgebraResearch Papers at Sala I
Chair(s): Aws Albarghouthi University of Wisconsin-Madison
15:21
22m
Talk
code2vec: Learning Distributed Representations of Code
Research Papers
Uri Alon Technion, Meital Zilberstein Technion, Omer Levy University of Washington, USA, Eran Yahav Technion
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
An Abstract Domain for Certifying Neural Networks
Research Papers
Link to publication DOI Media Attached
16:05
22m
Talk
Closed Forms for Numerical Loops
Research Papers
Zachary Kincaid Princeton University, Jason Breck University of Wisconsin - Madison, John Cyphert University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
Link to publication DOI Media Attached File Attached
15:21 - 16:27
Capabilities and Session Types IResearch Papers at Sala II
Chair(s): Dominic Orchard University of Kent, UK
15:21
22m
Talk
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Research Papers
Lau Skorstengaard Aarhus University, Dominique Devriese Vrije Universiteit Brussel, Belgium, Lars Birkedal Aarhus University
Link to publication DOI Media Attached File Attached
15:43
22m
Talk
Two sides of the same coin: Session Types and Game Semantics
Research Papers
Simon Castellan Imperial College London, UK, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached File Attached
16:05
22m
Talk
Exceptional Asynchronous Session Types: Session Types without Tiers
Research Papers
Simon Fowler The University of Edinburgh, Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Kansas, USA, Sara Décova
Link to publication DOI Pre-print Media Attached File Attached
16:37 - 17:43
Quantum ProgrammingResearch Papers at Sala I
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
16:37
22m
Talk
Quantitative Robustness Analysis of Quantum Programs
Research Papers
Shih-Han Hung University of Maryland, Kesha Hietala University of Maryland, Shaopeng Zhu University of Maryland, Mingsheng Ying University of Technology Sydney, Michael Hicks University of Maryland, College Park, Xiaodi Wu University of Oregon, USA
Link to publication DOI Media Attached
16:59
22m
Talk
Game Semantics for Quantum Programming
Research Papers
Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon, Glynn Winskel
Link to publication DOI Media Attached
17:21
22m
Talk
Quantum Relational Hoare Logic
Research Papers
Dominique Unruh University of Tartu
Link to publication DOI Pre-print Media Attached File Attached
16:37 - 17:43
Session Types IIResearch Papers at Sala II
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
16:37
22m
Talk
Interconnectability of Session-Based Logical ProcessesTOPLAS
Research Papers
Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached
16:59
22m
Talk
Distributed Programming using Role-Parametric Session Types in Go
Research Papers
David Castro-Perez Imperial College London, Raymond Hu Imperial College London, Sung-Shik Jongmans Open University of the Netherlands, Nicholas Ng Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached File Attached
17:21
22m
Talk
Less is More: Multiparty Session Types Revisited
Research Papers
Alceste Scalas Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Pre-print Media Attached File Attached
18:00 - 18:30
Wednesday Evening Program IResearch Papers at Sala I
18:00
30m
Talk
Microsoft Research: Engage, Verify, Open
Research Papers
Thomas Ball Microsoft Research
Media Attached
18:30 - 19:30
Wednesday Evening Program IIStudent Research Competition at Galeria
18:30
60m
Social Event
Student Research Competition and Reception supported by Microsoft Research
Student Research Competition

Thu 17 Jan

Displayed time zone: Belfast change

09:00 - 10:06
Type Abstraction and EffectsResearch Papers at Sala I
Chair(s): Benjamin Delaware Purdue University
09:00
22m
Talk
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Yizhou Zhang Cornell University, Andrew C. Myers Cornell University
Link to publication DOI Media Attached
09:22
22m
Talk
Abstracting Algebraic Effects
Research Papers
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław
Link to publication DOI Media Attached
09:44
22m
Talk
Fully Abstract Module Compilation
Research Papers
Karl Crary Carnegie Mellon University
Link to publication DOI Media Attached File Attached
09:00 - 10:06
SynthesisResearch Papers at Sala II
Chair(s): Robbert Krebbers Delft University of Technology
09:00
22m
Talk
Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper
Research Papers
Nadia Polikarpova University of California, San Diego, Ilya Sergey Yale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
09:22
22m
Talk
FrAngel: Component-Based Synthesis with Control Structures
Research Papers
Kensen Shi Stanford University, Jacob Steinhardt Stanford University, Percy Liang Stanford University
Link to publication DOI Pre-print Media Attached File Attached
09:44
22m
Talk
Hamsaz: Replication Coordination Analysis and Synthesis
Research Papers
Farzin Houshmand University of California, Riverside, Mohsen Lesani University of California, Riverside
Link to publication DOI Media Attached
10:30 - 12:30
Finalist Poster PresentationsStudent Research Competition at Sala III
10:36 - 12:04
Gradual TypesResearch Papers at Sala I
Chair(s): Nikhil Swamy Microsoft Research
10:36
22m
Talk
Type-Driven Gradual Security with ReferencesTOPLAS
Research Papers
Matías Toro University of Chile, Ronald Garcia University of British Columbia, Éric Tanter University of Chile & Inria Paris
DOI Media Attached File Attached
10:58
22m
Talk
Gradual Type Theory
Research Papers
Max New Northeastern University, Dan Licata Wesleyan University, Amal Ahmed Northeastern University, USA
Link to publication DOI Media Attached File Attached
11:20
22m
Talk
Gradual Parametricity, RevisitedDistinguished Paper
Research Papers
Matías Toro University of Chile, Elizabeth Labrada University of Chile, Éric Tanter University of Chile & Inria Paris
Link to publication DOI Pre-print Media Attached File Attached
11:42
22m
Talk
Live Functional Programming with Typed Holes
Research Papers
Cyrus Omar University of Chicago, Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago, Matthew Hammer None
Link to publication DOI Pre-print Media Attached File Attached
10:36 - 12:04
Separation Logic and Memory SemanticsResearch Papers at Sala II
Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore
10:36
22m
Talk
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Research Papers
Aleš Bizjak Aarhus University, Daniel Gratzer , Robbert Krebbers Delft University of Technology, Lars Birkedal Aarhus University
Link to publication DOI Media Attached File Attached
10:58
22m
Talk
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
Research Papers
José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela Sampaio Imperial College London, UK, Philippa Gardner Imperial College London
Link to publication DOI Media Attached File Attached
11:20
22m
Talk
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Research Papers
Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Arm Ltd, Kathryn E. Gray University of Cambridge, Robert M. Norton University of Cambridge, Prashanth Mundkur SRI International, Mark Wassell University of Cambridge, Jon French University of Cambridge, Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of Cambridge
Link to publication DOI Media Attached File Attached
11:42
22m
Talk
Exploring C Semantics and Pointer Provenance
Research Papers
Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Brooks Davis SRI International, Stephen Kell University of Kent, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge
Link to publication DOI Media Attached File Attached
12:04 - 13:45
Thursday LunchResearch Papers at Lunch Room
12:04
1h41m
Lunch
Lunch
Research Papers

13:45 - 14:51
Type Inference IResearch Papers at Sala I
Chair(s): Michael Hicks University of Maryland, College Park
13:45
22m
Talk
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Research Papers
Jana Dunfield Queen's University, Kingston, Ontario, Neel Krishnaswami Computer Laboratory, University of Cambridge
Link to publication DOI Media Attached
14:07
22m
Talk
Abstracting Extensible Data Types; Or, Rows By Any Other Name
Research Papers
J. Garrett Morris University of Kansas, USA, James McKinna
Link to publication DOI Media Attached
14:29
22m
Talk
Polymorphic Symmetric Multiple Dispatch with Variance
Research Papers
Gyunghee Park KAIST, Oracle Labs, Jaemin Hong KAIST, South Korea, Guy L. Steele Jr. Oracle Labs, Sukyoung Ryu KAIST, South Korea
Link to publication DOI Media Attached File Attached
13:45 - 14:51
Weak MemoryResearch Papers at Sala II
Chair(s): Scott Owens University of Kent, UK
13:45
22m
Talk
On Library Correctness under Weak Memory Consistency
Research Papers
Azalea Raad MPI-SWS, Germany, Marko Doko MPI-SWS, Germany, Lovro Rožić MPI-SWS, Germany, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Pre-print Media Attached File Attached
14:07
22m
Talk
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
Research Papers
Anton Podkopaev Higher School of Economics, JetBrains Research, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Pre-print Media Attached File Attached
14:29
22m
Talk
Grounding Thin-Air Reads with Event Structures
Research Papers
Soham Chakraborty Max Planck Institute for Software Systems, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Media Attached File Attached
15:21 - 16:49
Type Inference IIResearch Papers at Sala I
Chair(s): Niki Vazou IMDEA Software Institute
15:21
22m
Talk
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
Yusuke Miyazaki Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
Gradual Typing: A New Perspective
Research Papers
Giuseppe Castagna CNRS - Université Paris Diderot, France, Victor Lanvin IRIF, Université Paris Diderot, France, Tommaso Petrucciani DIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. Siek Indiana University, USA
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Intersection Types and Runtime Errors in the Pi-Calculus
Research Papers
Ugo Dal Lago University of Bologna, Italy / Inria, France, Marc De Visme ENS Lyon, Damiano Mazza CNRS, Akira Yoshimizu INRIA
Link to publication DOI Media Attached File Attached
16:27
22m
Talk
Principality and Approximation under Dimensional Bound
Research Papers
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
Link to publication DOI Media Attached File Attached
15:21 - 16:49
TimeResearch Papers at Sala II
Chair(s): Andrew C. Myers Cornell University
15:21
22m
Talk
Type-Guided Worst-Case Input Generation
Research Papers
Di Wang Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Research Papers
Conrad Watt University of Cambridge, John Renner University of California, San Diego, Natalie Popescu University of California San Diego, Sunjay Cauligi UCSD, Deian Stefan University of California San Diego
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Modular Quantitative Monitoring
Research Papers
Rajeev Alur University of Pennsylvania, Konstantinos Mamouras University of Pennsylvania, Caleb Stanford University of Pennsylvania
Link to publication DOI Media Attached File Attached
16:27
22m
Talk
CSS Minification via Constraint SolvingTOPLAS
Research Papers
Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Chih-Duo Hong University of Oxford
Media Attached File Attached
17:00 - 18:00
Business MeetingResearch Papers at Sala I + II
17:00
15m
Other
PC Chair Report
Research Papers
Stephanie Weirich University of Pennsylvania, USA
Media Attached
17:15
10m
Awards
SIGPLAN Awards
Research Papers
Benjamin C. Pierce University of Pennsylvania
Media Attached
17:25
5m
Other
POPL 2020 Announcement
Research Papers
Brigitte Pientka McGill University, Lars Birkedal Aarhus University
Media Attached
17:30
10m
Other
NSF funding for PL
Research Papers
Rance Cleaveland University of Maryland
Media Attached
17:40
10m
Other
SIGPLAN Climate Committee Report
Research Papers
Benjamin C. Pierce University of Pennsylvania
Media Attached
17:50
10m
Other
State of SIGPLAN
Research Papers
Jens Palsberg University of California, Los Angeles (UCLA)
Media Attached
18:15 - 19:15
Reception supported by FacebookResearch Papers at Galeria
18:15
60m
Social Event
Reception supported by Facebook
Research Papers

Fri 18 Jan

Displayed time zone: Belfast change

09:00 - 10:05
SRC Announcement & Keynote IIStudent Research Competition / Research Papers at Sala I + II
Chair(s): Stephanie Weirich University of Pennsylvania, USA
09:00
5m
Awards
SRC Announcement
Student Research Competition
Niki Vazou IMDEA Software Institute
Media Attached
09:05
60m
Talk
Mechanized Metatheory - The Next Chapter
Research Papers
Brigitte Pientka McGill University
Media Attached File Attached
10:35 - 12:03
Abstract InterpretationResearch Papers at Sala II
Chair(s): David Naumann Stevens Institute of Technology
10:35
22m
Talk
A^2 I: Abstract^2 InterpretationDistinguished Paper
Research Papers
Patrick Cousot , Roberto Giacobazzi University of Verona and IMDEA Software Institute, Francesco Ranzato University of Padova
Link to publication DOI Media Attached File Attached
10:57
22m
Talk
Concerto: A Framework for Combined Concrete and Abstract Interpretation
Research Papers
John Toman University of Washington, Seattle, Dan Grossman University of Washington
Link to publication DOI Media Attached
11:19
22m
Talk
Skeletal Semantics and their Interpretations
Research Papers
Martin Bodin Imperial College London, Philippa Gardner Imperial College London, Thomas P. Jensen INRIA Rennes, Alan Schmitt Inria
Link to publication DOI Pre-print Media Attached File Attached
11:41
22m
Talk
Refinement of Path Expressions for Static Analysis
Research Papers
John Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
Link to publication DOI Media Attached File Attached
12:03 - 13:45
12:03
1h42m
Lunch
Lunch
Research Papers

13:45 - 14:51
SemanticsResearch Papers at Sala I
Chair(s): Noam Zeilberger University of Birmingham, UK
13:45
22m
Talk
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Research Papers
Wen Kokke University of Edinburgh, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark
Link to publication DOI Media Attached
14:07
22m
Talk
Diagrammatic Algebra: From Linear to Concurrent Systems
Research Papers
Filippo Bonchi University of Pisa, Joshua Holland University of Southampton, Robin Piedeleu University of Oxford, Pawel Sobocinski University of Southampton, Fabio Zanasi University College London
Link to publication DOI Media Attached
14:29
22m
Talk
Fixpoint Games on Continuous Lattices
Research Papers
Paolo Baldan University of Padova, Barbara König University of Duisburg-Essen, Christina Mika-Michalski University of Duisburg-Essen, Tommaso Padoan University of Padova
Link to publication DOI Media Attached File Attached
13:45 - 14:51
Model CheckingResearch Papers at Sala II
Chair(s): P. Madhusudan University of Illinois at Urbana-Champaign
13:45
22m
Talk
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Research Papers
Taolue Chen Birkbeck, University of London, Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Philipp Ruemmer Uppsala University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Link to publication DOI Media Attached File Attached
14:07
22m
Talk
Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation
Research Papers
Kyungmin Bae Pohang University of Science and Technology (POSTECH), Jia Lee Pohang University of Science and Technology (POSTECH)
Link to publication DOI Media Attached File Attached
14:29
22m
Talk
Adventures in Monitorability: From Branching to Linear Time and Back Again
Research Papers
Luca Aceto Reykjavik University, Antonis Achilleos Reykjavik University, Adrian Francalanza University of Malta, Anna Ingolfsdottir Reykjavik University, Karoliina Lehtinen University of Kiel and University of Liverpool
Link to publication DOI Media Attached
15:21 - 16:27
Security and Information FlowResearch Papers at Sala I
Chair(s): David Walker Princeton University
15:21
22m
Talk
LWeb: Information Flow Security for Multi-Tier Web Applications
Research Papers
James Parker University of Maryland, Niki Vazou IMDEA Software Institute, Michael Hicks University of Maryland, College Park
Link to publication DOI Media Attached File Attached
15:43
22m
Talk
From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper
Research Papers
Marco Vassena Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden, Deepak Garg Max Planck Institute for Software Systems, Vineet Rajani MPI-SWS, Deian Stefan University of California San Diego
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Modalities, Cohesion, and Information Flow
Research Papers
Alex Kavvos Wesleyan University
Link to publication DOI Pre-print File Attached
15:21 - 16:27
Program Analysis IResearch Papers at Sala II
Chair(s): Michael D. Adams University of Utah
15:21
22m
Talk
Decidable Verification of Uninterpreted Programs
Research Papers
Umang Mathur 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
15:43
22m
Talk
Inferring Frame Conditions with Static Correlation Analysis
Research Papers
Oana-Fabiana Andreescu Internet of Trust, Thomas P. Jensen INRIA Rennes, Stéphane Lescuyer Prove & Run, Benoît Montagu Prove & Run
Link to publication DOI Pre-print Media Attached File Attached
16:05
22m
Talk
Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown SystemsDistinguished Paper
Research Papers
Johannes Späth Fraunhofer IEM, Karim Ali University of Alberta, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
Link to publication DOI Pre-print Media Attached File Attached
16:37 - 17:43
Verified Compilation and ConcurrencyResearch Papers at Sala I
Chair(s): Michael Greenberg Pomona College
16:37
22m
Talk
A Calculus for Esterel: If can, can. If no can, no can.
Research Papers
Spencer P. Florence Northwestern University, USA, Shu-Hung You Northwestern University, USA, Jesse A. Tov Northwestern University, Department of Electrical Engineering and Computer Science, Robby Findler Northwestern University, USA
Link to publication DOI Media Attached File Attached
16:59
22m
Talk
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Research Papers
Yuting Wang Yale University, Pierre Wilke Yale University, Zhong Shao Yale University
Link to publication DOI Media Attached File Attached
17:21
22m
Talk
A Verified, Efficient Embedding of a Verifiable Assembly Language
Research Papers
Aymeric Fromherz Carnegie Mellon University, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Bryan Parno , Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
Link to publication DOI Media Attached File Attached
16:37 - 17:43
Program Analysis IIResearch Papers at Sala II
Chair(s): Michael Emmi SRI International
16:37
22m
Talk
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Research Papers
Xin Yi National University of Defense Technology, Liqian Chen National University of Defense Technology, Xiaoguang Mao National University of Defense Technology, Tao Ji National University of Defense Technology
Link to publication DOI Media Attached File Attached
16:59
22m
Talk
Efficient Parameterized Algorithms for Data Packing
Research Papers
Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady IST Austria, Nastaran Okati Ferdowsi University of Mashhad, Andreas Pavlogiannis EPFL, Switzerland
Link to publication DOI Pre-print Media Attached File Attached
17:21
22m
Talk
Fast and exact analysis for LRU caches
Research Papers
Valentin Touzeau Univ. Grenoble Alpes, Claire Maiza Verimag, France, David Monniaux CNRS, VERIMAG, Jan Reineke Saarland University
Link to publication DOI Media Attached File Attached
17:45 - 18:45
Friday Social HourResearch Papers at Galeria
17:45
60m
Social Event
Social Hour
Research Papers

Sat 19 Jan

Displayed time zone: Belfast change

09:00 - 10:30
Keynote & Contributed Talks 1CoqPL at Sala VI
Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore
09:00
5m
Day opening
Opening
CoqPL

09:05
60m
Talk
Coq User Interfaces: Past, Present, and Future (Keynote)
CoqPL
10:05
25m
Talk
Counterexamples for Coq Conjectures
CoqPL
Samuel Gruetter Massachusetts Institute of Technology
File Attached
09:00 - 10:30
09:30
60m
Talk
De-escalating Software (Keynote)
Off the Beaten Track
Stephen Kell University of Kent
11:15 - 12:30
Contributed Talks 2CoqPL at Sala VI
Chair(s): Enrico Tassi INRIA
11:15
25m
Talk
Towards Mechanising Probabilistic Properties of a Blockchain
CoqPL
Kiran Gopinathan University College London, Ilya Sergey Yale-NUS College and National University of Singapore
File Attached
11:40
25m
Talk
Verifying Finality for Blockchain Systems
CoqPL
Karl Palmskog University of Texas at Austin, Milos Gligoric University of Texas at Austin, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
File Attached
12:05
25m
Talk
WIP: Formalizing the Concordium Consensus Protocol in Coq
CoqPL
Thomas Dinsdale-Young , Bas Spitters Aarhus University, Søren Eller Thomsen Aarhus University, Daniel Tschudi Aarhus University
File Attached
12:30 - 14:00
Saturday LunchWorkshops at Lunch Room
12:30
90m
Lunch
Lunch
Workshops

14:00 - 15:30
Contributed Talks 3 & Coq DevelopersCoqPL at Sala VI
Chair(s): Qinxiang Cao Shanghai Jiao Tong University
14:00
25m
Talk
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
CoqPL
Vadim Zaliva Carnegie Mellon University, USA, Matthieu Sozeau Inria
File Attached
14:25
25m
Talk
Reifying and Translating a Monadic Fragment of Gallina
CoqPL
File Attached
14:50
40m
Demonstration
Session with the Coq Development Team
CoqPL
14:00 - 15:30
Afternoon TalksOff the Beaten Track at Sala VII
Chair(s): Luke Church
14:00
45m
Other
Design Critique and Discussion
Off the Beaten Track
14:45
45m
Talk
F a Language for Music Composition
Off the Beaten Track
Joachim Kristensen DIKU, University of Copenhagen, Ken Friis Larsen DIKU, University of Copenhagen
File Attached
16:00 - 17:30
Informal + Business MeetingOff the Beaten Track at Sala VII
16:00
90m
Meeting
Informal + Business Meeting
Off the Beaten Track