Write a Blog >>

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 17 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:50 - 09:00
WelcomeVMCAI at Room St Petersburg I
Chair(s): K. Rustan M. Leino Microsoft Research
09:00 - 10:00
Invited Talk IVMCAI at Room St Petersburg I
Chair(s): Sharon Shoham
09:00
60m
Talk
Automating Abstract Interpretation
VMCAI
Thomas Reps University of Wisconsin - Madison and Grammatech Inc.

Mon 18 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:30 - 10:00
T1: An Introduction to Redex with Abstracting Abstract MachinesTutorials at Room HTC 1
08:30
90m
Talk
T1: An Introduction to Redex with Abstracting Abstract Machines
Tutorials
David Van Horn University of Maryland, College Park
Link to publication
08:30 - 10:00
T3: Syntax-Guided Synthesis (SyGuS)Tutorials at Room HTC 2
08:30
90m
Talk
T3: Syntax-Guided Synthesis (SyGuS)
Tutorials
Rajeev Alur University of Pennsylvania, Dana Fisman University of Pennsylvania, Rishabh Singh Microsoft Research, Armando Solar-Lezama MIT
Link to publication
08:30 - 10:00
T5: Higher-Order Model CheckingTutorials at Room HTC 3
08:30
90m
Talk
T5: Higher-Order Model Checking
Tutorials
Naoki Kobayashi University of Tokyo, C.-H. Luke Ong University of Oxford, UK
08:45 - 09:00
WelcomePADL at Room Bayboro
Chair(s): John Reppy University of Chicago
09:00 - 10:00
Invited TalkPADL at Room Bayboro
09:00
60m
Talk
Program Synthesis for Direct Manipulation Interfaces
PADL
Ravi Chugh University of Chicago
09:00 - 10:00
Invited Talk IIVMCAI at Room St Petersburg I
Chair(s): K. Rustan M. Leino Microsoft Research
09:00
60m
Talk
Ironclad - Full Verification of Complex Systems
VMCAI
Bryan Parno Microsoft Research
09:00 - 10:00
Session 1: Invited talk by Harvey FriedmanCPP at Room St Petersburg II
09:00
60m
Talk
Perspectives on Formal Verfication
CPP
Harvey Friedman Ohio State University
10:30 - 12:00
Functional Programming IPADL at Room Bayboro
10:30
30m
Talk
Simplifying Probabilistic Programs Using Computer Algebra
PADL
Jacques Carette McMaster University, Chung-chieh Shan Indiana University
11:00
30m
Talk
Haskino: A Remote Monad for Programming the Arduino
PADL
Mark Grebe University of Kansas, Andy Gill University of Kansas
11:30
30m
Talk
From Monads to Effects and Back
PADL
Niki Vazou UC San Diego, Daan Leijen Microsoft Research
10:30 - 12:00
T2: Declare Your Language: Part 1Tutorials at Room HTC 1
10:30
90m
Talk
T2: Declare Your Language (Part 1): Hands-On Spoofax Tutorial
Tutorials
Eelco Visser Delft University of Technology
10:30 - 12:00
T3: Syntax-Guided Synthesis (SyGuS)Tutorials at Room HTC 2
10:30
90m
Talk
T3: Syntax-Guided Synthesis (SyGuS) (Advanced Material)
Tutorials
Rajeev Alur University of Pennsylvania, Dana Fisman University of Pennsylvania, Rishabh Singh Microsoft Research, Armando Solar-Lezama MIT
Link to publication
10:30 - 12:00
T4: Programs and Proofs in the Coq Proof AssistantTutorials at Room HTC 3
10:30
90m
Talk
T4: Programs and Proofs in the Coq Proof Assistant
Tutorials
Robert Rand University of Pennsylvania, Arthur Azevedo de Amorim University of Pennsylvania
Link to publication
10:30 - 12:00
T6: Security and Privacy by Typing in Cryptographic SystemsTutorials at Room HTC 4
10:30
90m
Talk
T6: Security and Privacy by Typing in Cryptographic Systems
Tutorials
Matteo Maffei Saarland University
10:30 - 12:00
Hybrid and Timed SystemsVMCAI at Room St Petersburg I
Chair(s): David Monniaux CNRS, VERIMAG
10:30
30m
Talk
Abstract Interpretation with Infinitesimals
VMCAI
Kengo Kido , Swarat Chaudhuri Rice University, Ichiro Hasuo University of Tokyo
11:00
30m
Talk
Lipschitz Robustness of Timed I/O Systems
VMCAI
Thomas A. Henzinger IST Austria, Jan Otop University of Wrocław, Roopsha Samanta IST Austria
11:30
30m
Talk
A method for invariant generation for polynomial continuous systems
VMCAI
Andrew Sogokon , Khalil Ghorbal Carnegie Mellon University, Paul Jackson , André Platzer
14:00 - 15:30
ConstraintsPADL at Room Bayboro
14:00
30m
Talk
A GPU implementation of the ASP computation
PADL
Agostino Dovier University of Udine, Andrea Formisano Università di Perugia , Enrico Pontelli New Mexico State University, Flavio Vella Sapienza University of Rome, Italy
14:30
30m
Talk
Using Constraint Logic Programming to Schedule Solar Array Operations on the International Space Station
PADL
Jan Jelínek Charles University in Prague, Roman Barták Charles University in Prague
15:00
30m
Talk
The Picat-SAT Compiler
PADL
Neng-Fa Zhou CUNY Brooklyn College and Graduate Center, Håkan Kjellerstrand CUNY Brooklyn College and Graduate Center
14:00 - 15:30
Invited talks 4 & 5PEPM Invited Talks at Room Demens
14:00
45m
Talk
Invited Talk: Program Synthesis: Opportunities for the next Decade
PEPM Invited Talks
I: Rastislav Bodik University of Washington, USA
14:45
45m
Talk
Invited Talk: LMS: a Perspective on Generative Programming
PEPM Invited Talks
I: Nada Amin EPFL
14:00 - 15:30
T1: An Introduction to Redex with Abstracting Abstract MachinesTutorials at Room HTC 1
14:00
90m
Talk
T1: An Introduction to Redex with Abstracting Abstract Machines(Advanced Material)
Tutorials
David Van Horn University of Maryland, College Park
Link to publication
14:00 - 15:30
T7: Trace-based Synchronization Synthesis for Concurrent ProgramsTutorials at Room HTC 2
14:00
90m
Talk
T7: Trace-based Synchronization Synthesis for Concurrent Programs
Tutorials
Arjun Radhakrishna Microsoft, Roopsha Samanta IST Austria
14:00 - 15:30
T4: Programs and Proofs in the Coq Proof AssistantTutorials at Room HTC 3
14:00
90m
Talk
T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material)
Tutorials
Robert Rand University of Pennsylvania, Arthur Azevedo de Amorim University of Pennsylvania
Link to publication
14:00 - 15:30
T6: Security and Privacy by Typing in Cryptographic SystemsTutorials at Room HTC 4
14:00
90m
Talk
T6: Security and Privacy by Typing in Cryptographic Systems
Tutorials
Matteo Maffei Saarland University
14:00 - 15:30
Dynamic and Static VerificationVMCAI at Room St Petersburg I
Chair(s): Aarti Gupta Princeton University
14:00
30m
Talk
Hybrid Analysis for Partial Order Reduction of Programs with Arrays
VMCAI
Pavel Parizek Charles University in Prague
14:30
30m
Talk
Cloud-Based Verification of Concurrent Software
VMCAI
15:00
30m
Talk
Abstraction-driven Concolic Testing
VMCAI
14:00 - 15:30
Session 3: Design and Implementation of Theorem ProversCPP at Room St Petersburg II
14:00
30m
Talk
The Vampire and the FOOL
CPP
Evgenii Kotelnikov Chalmers University of Technology, Laura Kovacs Chalmers University of Technology, Giles Reger University of Manchester, Andrei Voronkov University of Manchester
14:30
30m
Talk
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
CPP
Lukasz Czajka University of Innsbruck
15:00
30m
Talk
Mizar Environment for Isabelle
CPP
Cezary Kaliszyk University of Innsbruck, Karol Pąk University of Bialystok, Institute of Computer Science, Josef Urban
16:00 - 17:00
Logic ProgrammingPADL at Room Bayboro
16:00
30m
Talk
The KB paradigm and its application to interactive configuration
PADL
Pieter Van Hertum KU Leuven, Ingmar Dasseville KU Leuven, Gerda Janssens KU Leuven, Marc Denecker KU Leuven
16:30
30m
Talk
Default Rules for Curry
PADL
Sergio Antoy Kiel University, Michael Hanus Kiel University
16:00 - 17:30
Invited talks 6 & 7PEPM Invited Talks at Room Demens
16:00
45m
Talk
Invited Talk: Fiat: Extensible Code Generation with Proofs
PEPM Invited Talks
16:45
45m
Talk
Invited Talk: The Promise of Relational Programming
PEPM Invited Talks
I: William E. Byrd University of Utah
16:00 - 17:30
T2: Declare Your Language: Part 2Tutorials at Room HTC 1
16:00
90m
Talk
T2: Declare Your Language (Part 2): Name Binding with Scope Graphs
Tutorials
Eelco Visser Delft University of Technology
Link to publication DOI Media Attached
16:00 - 17:30
T7: Trace-based Synchronization Synthesis for Concurrent ProgramsTutorials at Room HTC 2
16:00
90m
Talk
T7: Trace-based Synchronization Synthesis for Concurrent Programs
Tutorials
Arjun Radhakrishna Microsoft, Roopsha Samanta IST Austria
16:00 - 17:30
T5: Higher-Order Model CheckingTutorials at Room HTC 3
16:00
90m
Talk
T5: Higher-Order Model Checking
Tutorials
Naoki Kobayashi University of Tokyo, C.-H. Luke Ong University of Oxford, UK

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

08:50 - 09:00
Welcome SessionPLMW at Room St Petersburg III
09:00 - 10:00
Invited Talk IIIVMCAI at Room St Petersburg I
Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder
09:00
60m
Talk
Viper - A Verification Infrastructure for Permission-based Reasoning
VMCAI
Peter Müller ETH Zurich
09:00 - 10:00
Session 5: Invited talk by Leonardo de MouraCPP at Room St Petersburg II
09:00
60m
Talk
Dependent Type Practice
CPP
Leonardo de Moura Microsoft Research, Redmond
10:30 - 12:00
Parsing & Domain-Specific Languages IPEPM at Room Harbor View
Chair(s): Kenichi Asai Ochanomizu University
10:30
30m
Talk
Practical, General Parser Combinators
PEPM
Anastasia Izmaylova Centrum Wiskunde & Informatica, Ali Afroozeh Centrum Wiskunde & Informatica, Tijs van der Storm CWI
DOI Pre-print
11:00
30m
Talk
Operator Precedence for Data-Dependent Grammars
PEPM
Ali Afroozeh Centrum Wiskunde & Informatica, Anastasia Izmaylova Centrum Wiskunde & Informatica
DOI Pre-print
11:30
30m
Talk
Everything Old Is New Again: Quoted Domain-Specific Languages
PEPM
Shayan Najd , Sam Lindley University of Edinburgh, Josef Svenningsson Chalmers University of Technology, Sweden, Philip Wadler University of Edinburgh
DOI
10:30 - 12:00
Concurrent ProgramsVMCAI at Room St Petersburg I
Chair(s): Noam Rinetzky
10:30
30m
Talk
Pointer Race Freedom
VMCAI
Frédéric Haziza , Lukáš Holík , Roland Meyer , Sebastian Wolff Fraunhofer ITWM and TU Kaiserslautern
11:00
30m
Talk
A program logic for C11 memory fences
VMCAI
Marko Doko MPI-SWS, Germany, Viktor Vafeiadis MPI-SWS, Germany
11:30
30m
Talk
From Low Level Pointers to High Level Containers
VMCAI
Kamil Dudka , Lukáš Holík , Petr Peringer , Tomáš Vojnar Brno University of Technology
10:30 - 12:00
Session 6: FoundationsCPP at Room St Petersburg II
10:30
30m
Talk
A Logic of Proofs for Differential Dynamic Logic
CPP
Nathan Fulton Carnegie Mellon University, André Platzer
11:00
30m
Talk
Constructing the Propositional Truncation using Non-recursive HITs
CPP
Floris van Doorn Carnegie Mellon University
11:30
30m
Talk
A Nominal Exploration of Intuitionism
CPP
Vincent Rahli SnT, Mark Bickford Cornell University
10:30 - 12:00
10:30
30m
Talk
Academia or Industry?
PLMW
Aarti Gupta Princeton University
Media Attached
11:00
30m
Talk
Refining Types with SMT
PLMW
Ranjit Jhala University of California, San Diego
Media Attached
11:30
30m
Talk
How to Write Papers So People Can Read Them
PLMW
Derek Dreyer MPI-SWS
Media Attached
14:00 - 15:30
Domain-Specific Languages IIPEPM at Room Harbor View
Chair(s): Sebastian Erdweg TU Darmstadt, Germany
14:00
30m
Talk
BiGUL: A Formally Verified Core Language for Putback-Based Bidirectional Programming
PEPM
Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Tao Zan Sokendai, Japan, Zhenjiang Hu National Institute of Informatics
DOI Pre-print
14:30
30m
Talk
A Constraint Language for Static Semantic Analysis Based on Scope Graphs
PEPM
Hendrik van Antwerpen Delft University of Technology, Netherlands, Pierre Neron TU Delft, Andrew Tolmach Portland State University, Eelco Visser Delft University of Technology, Guido Wachsmuth Delft University of Technology
Link to publication DOI Pre-print
15:00
30m
Talk
Finally, Safely-Extensible and Efficient Language-Integrated Query
PEPM
Kenichi Suzuki University of Tsukuba, Japan, Oleg Kiselyov , Yukiyoshi Kameyama
DOI
14:00 - 15:30
Parameterized and Component-Based SystemsVMCAI at Room St Petersburg I
Chair(s): Arie Gurfinkel Carnegie Mellon University
14:00
30m
Talk
Regular Symmetry Patterns
VMCAI
Anthony Widjaja Lin Yale-NUS College, Singapore, Truong Khanh Nguyen , Philipp Ruemmer Uppsala University, Jun Sun
14:30
30m
Talk
Tight Cutoffs for Guarded Protocols with Fairness
VMCAI
15:00
30m
Talk
A General Modular Synthesis Problem for Pushdown Systems
VMCAI
14:00 - 15:30
Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II
14:00
30m
Talk
Bisimulation Up-to Techniques for Psi-calculi
CPP
Johannes Å. Pohjola Uppsala University, Joachim Parrow Uppsala University
14:30
30m
Talk
Planning for Change in a Formal Verification of the Raft Consensus Protocol
CPP
Doug Woos University of Washington, James R. Wilcox University of Washington, Steve Anton University of Washington, Zachary Tatlock University of Washington, Seattle, Michael D. Ernst University of Washington, Thomas Anderson University of Washington
Pre-print
15:00
30m
Talk
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Michel St-Martin University of Ottawa, Amy Felty University of Ottawa
14:00 - 15:30
14:00
30m
Talk
Student Interaction Activity
PLMW
Isil Dillig University of Texas, Austin, Ross Tate Cornell University
14:30
30m
Talk
Automata and Coinduction
PLMW
Alexandra Silva Radboud University Nijmegen
Media Attached
15:00
30m
Talk
Unaccustomed As I Am to Public Speaking
PLMW
John Hughes Chalmers University of Technology
Media Attached
16:00 - 17:40
StagingPEPM at Room Harbor View
Chair(s): Jacques Carette McMaster University
16:00
30m
Talk
Staging Generic Programming
PEPM
Jeremy Yallop University of Cambridge, UK
DOI
16:30
30m
Talk
Removing Runtime Overhead for Optimized Object Queries
PEPM
Jon Brandvein , Yanhong A. Liu Stony Brook University, USA
DOI
17:00
20m
Talk
Toward Introducing Binding-Time Analysis to MetaOCaml
PEPM
Kenichi Asai Ochanomizu University
DOI
17:20
20m
Talk
Staging beyond Terms: Prospects and Challenges
PEPM
Jun Inoue National Institute of Advanced Industrial Science and Technology, Japan, Oleg Kiselyov , Yukiyoshi Kameyama
DOI
16:00 - 17:00
Session 8: Compiler VerificationCPP at Room St Petersburg II
16:00
30m
Talk
Formal Verification of Control-flow Graph Flattening
CPP
Sandrine Blazy IRISA / University of Rennes 1, Alix Trieu ENS Rennes
16:30
30m
Talk
Axiomatic Semantics for Compiler Verification
CPP
Steven Schäfer , Sigurd Schneider Saarland University, Gert Smolka Saarland University
18:00 - 21:00
CPP Reception, sponsored by the DeepSpec projectCPP at Room St Petersburg I
18:00
3h
Social Event
CPP Reception, sponsored by the DeepSpec project
CPP

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Invited WedInvited Speakers at Grand Bay Ballroom
Chair(s): Rastislav Bodik University of Washington, USA
09:00
60m
Talk
Programming the World of Uncertain Things
Invited Speakers
Kathryn S McKinley Microsoft Research
10:30 - 12:10
Track 1: Algorithmic VerificationResearch Papers at Grand Bay North
Chair(s): Arie Gurfinkel Carnegie Mellon University
10:30
25m
Talk
Temporal Verification of Higher-order Functional Programs
Research Papers
Akihiro Murase , Tachio Terauchi JAIST, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo, Hiroshi Unno University of Tsukuba
10:55
25m
Talk
Scaling Network Verification using Symmetry and Surgery
Research Papers
Gordon Plotkin , Nikolaj Bjørner Microsoft Research, Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research, George Varghese Microsoft Research
Pre-print
11:20
25m
Talk
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Research Papers
11:45
25m
Talk
Reducing Crash Recoverability to Reachability
Research Papers
Eric Koskinen Yale University, Junfeng Yang Columbia University
10:30 - 12:10
Track 2: Types and FoundationsResearch Papers at Grand Bay South
Chair(s): Robert Atkey University of Strathclyde
10:30
25m
Talk
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
Research Papers
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles
Media Attached File Attached
10:55
25m
Talk
Type Theory in Type Theory using Quotient Inductive Types
Research Papers
Thorsten Altenkirch University of Nottingham, Ambrus Kaposi University of Nottingham
Media Attached File Attached
11:20
25m
Talk
System Fω with Equirecursive Types for Datatype-generic Programming
Research Papers
Yufei Cai University of Tübingen, Germany, Paolo G. Giarrusso University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
Media Attached
11:45
25m
Talk
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Research Papers
Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo Fiore Computer Laboratory, University of Cambridge, Guillaume Munch-Maccagnoni Computer Laboratory, University of Cambridge
14:20 - 16:00
Track 1: Decision ProceduresResearch Papers at Grand Bay North
Chair(s): Loris D'Antoni University of Pennsylvania
14:20
25m
Talk
Query-Guided Maximum Satisfiability
Research Papers
Xin Zhang Georgia Tech, Ravi Mangal Georgia Institute of Technology, Aditya Nori Microsoft Research, UK, Mayur Naik Georgia Tech
File Attached
14:45
25m
Talk
String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
Research Papers
Anthony Widjaja Lin Yale-NUS College, Singapore, Pablo Barcelo University of Chile, Chile
Media Attached
15:10
25m
Talk
Symbolic Computation of Differential Equivalences
Research Papers
Luca Cardelli Microsoft Research and University of Oxford, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin IMT Institute for Advanced Studies Lucca, Italy
Media Attached
15:35
25m
Talk
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
Research Papers
Matthew Hague Royal Holloway University of London, UK, Jonathan Kochems Department of Computer Science, University of Oxford, C.-H. Luke Ong University of Oxford, UK
Media Attached
14:20 - 16:00
Track 2: Correct CompilationResearch Papers at Grand Bay South
Chair(s): Jens Palsberg University of California, Los Angeles
14:20
25m
Talk
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Dominique Devriese iMinds - Distrinet, KU Leuven, Marco Patrignani KU Leuven, Frank Piessens iMinds - Distrinet, KU Leuven
Pre-print Media Attached
14:45
25m
Talk
Lightweight Verification of Separate Compilation
Research Papers
Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Chung-Kil Hur Seoul National University, Derek Dreyer MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Media Attached File Attached
15:10
25m
Talk
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Ed Robbins Kent, Andy King Kent, Tom Schrijvers KU Leuven
Media Attached
15:35
25m
Talk
Sound Type-dependent Syntactic Language Extension
Research Papers
Florian Lorenzen TU Berlin, Sebastian Erdweg TU Darmstadt, Germany
Pre-print Media Attached File Attached
16:30 - 17:45
Track 1: Language DesignResearch Papers at Grand Bay North
Chair(s): David Walker Princeton University
16:30
25m
Talk
Dependent Types and Multi-Monadic Effects in F*
Research Papers
Nikhil Swamy Microsoft Research, Cătălin Hriţcu INRIA Paris, Chantal Keller MSR-INRIA, Aseem Rastogi University of Maryland, College Park, Antoine Delignat-Lavaud INRIA, Simon Forest ENS, Karthikeyan Bhargavan INRIA, Cédric Fournet Microsoft Research, Pierre-Yves Strub IMDEA Software Institute, Markulf Kohlweiss Microsoft Research, Jean-Karim Zinzindohoué INRIA, Santiago Zanella-Béguelin Microsoft Research
Pre-print Media Attached
16:55
25m
Talk
Fabular: Regression Formulas as Probabilistic Programming
Research Papers
Johannes Borgström Uppsala University, Andrew D. Gordon Microsoft Research and University of Edinburgh, Long Ouyang Stanford University, Claudio Russo Microsoft Research, Adam Ścibior University of Cambridge, Marcin Szymczak University of Edinburgh
Media Attached
17:20
25m
Talk
Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Research Papers
Bjørn Bugge Grathwohl DIKU, University of Copenhagen, Fritz Henglein DIKU, Denmark, Ulrik Terp Rasmussen DIKU, University of Copenhagen, Kristoffer Aalund Søholm Jobindex, Denmark, Sebastian Paaske Tørholm Jobindex, Denmark
Media Attached
16:30 - 17:45
Track 2: Decidability and complexityResearch Papers at Grand Bay South
Chair(s): C.-H. Luke Ong University of Oxford, UK
16:30
25m
Talk
Decidability of Inferring Inductive Invariants
Research Papers
Oded Padon Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Sharon Shoham , Aleksandr Karbyshev Tel Aviv University, Mooly Sagiv Tel Aviv University
Media Attached
16:55
25m
Talk
The Hardness of Data Packing
Research Papers
Rahman Lavaee , Chen Ding University of Rochester
Media Attached
17:20
25m
Talk
The Complexity of Interaction
Research Papers
Stéphane Gimenez University of Innsbruck, Georg Moser University of Innsbruck
Media Attached
19:00 - 22:00

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Invited Speaker ThuInvited Speakers at Grand Bay Ballroom
Chair(s): Rupak Majumdar MPI-SWS
09:00
60m
Talk
Synthesis of Reactive Controllers for Hybrid Systems
Invited Speakers
Richard M. Murray California Institute of Technology
Media Attached
10:30 - 12:10
Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North
Chair(s): Mooly Sagiv Tel Aviv University
10:30
25m
Talk
Certified Causally Consistent Distributed Key-Value Stores
Research Papers
Media Attached
10:55
25m
Talk
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Research Papers
Alexey Gotsman IMDEA, Hongseok Yang University of Oxford, UK, Carla Ferreira Universidade Nova Lisboa, Mahsa Najafzadeh UPMC & INRIA, Marc Shapiro Inria & LIP6
Media Attached
11:20
25m
Talk
A Program Logic for Concurrent Objects under Fair Scheduling
Research Papers
Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China
Media Attached
11:45
25m
Talk
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Research Papers
Cezara Drăgoi INRIA, ENS, CNRS, Thomas A. Henzinger IST Austria, Damien Zufferey MIT
Link to publication DOI Pre-print Media Attached File Attached
10:30 - 12:10
Track 2: Probabilistic and statistical analysisResearch Papers at Grand Bay South
Chair(s): Aditya Nori Microsoft Research, UK
10:30
25m
Talk
Prophet: Automatic Patch Generation via Learning from Successful Patches
Research Papers
Fan Long MIT CSAIL, Martin C. Rinard Massachusetts Institute of Technology, USA
Media Attached
10:55
25m
Talk
Estimating types in binaries using predictive modeling
Research Papers
Omer Katz Technion, Israel Institute of Technology, Ran El-Yaniv Technion, Israel Institute of Technology, Eran Yahav Technion
Media Attached File Attached
11:20
25m
Talk
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
Research Papers
Krishnendu Chatterjee IST Austria, Hongfei Fu IST Austria, Rouzbeh Hasheminezhad Sharif University, Petr Novotný IST Austria
Media Attached
11:45
25m
Talk
Transforming Spreadsheet Data Types using Examples
Research Papers
Rishabh Singh Microsoft Research, Sumit Gulwani Microsoft Research
Media Attached
14:20 - 16:00
Track 1: Learning and verificationResearch Papers at Grand Bay North
Chair(s): David Monniaux CNRS, VERIMAG
14:20
25m
Talk
Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
Research Papers
Damien Octeau University of Wisconsin and Pennsylvania State University, Somesh Jha University of Wisconsin, Madison, Matthew Dering Pennsylvania State University, Patrick McDaniel Pennsylvania State University, Alexandre Bartel Technical University Darmstadt, Hongyu Li Rice University, Jacques Klein University of Luxembourg, Yves Le Traon University of Luxembourg
Media Attached
14:45
25m
Talk
Abstraction Refinement Guided by a Learnt Probabilistic Model
Research Papers
Radu Grigore University of Oxford, Hongseok Yang University of Oxford, UK
Media Attached
15:10
25m
Talk
Learning Invariants using Decision Trees and Implication Counterexamples
Research Papers
Pranav Garg University of Illinois at Urbana-Champaign, Daniel Neider University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Dan Roth University of Illinois at Urbana-Champaign
Media Attached
15:35
25m
Talk
Symbolic Abstract Data Type Inference
Research Papers
Michael Emmi IMDEA Software Institute, Constantin Enea LIAFA, Université Paris Diderot
Media Attached
14:20 - 16:00
Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South
Chair(s): Tiark Rompf Purdue & Oracle Labs
14:20
25m
Talk
Principal Type Inference for GADTs
Research Papers
Sheng Chen University of louisiana at Lafayette, Martin Erwig Oregon State University
Media Attached
14:45
25m
Talk
Abstracting Gradual Typing
Research Papers
Ronald Garcia University of British Columbia, Alison M. Clark , Éric Tanter University of Chile, Chile
Link to publication Media Attached
15:10
25m
Talk
The Gradualizer: a methodology and algorithm for generating gradual type systems
Research Papers
Matteo Cimini Indiana University, Jeremy G. Siek Indiana University
Media Attached
15:35
25m
Talk
Is Sound Gradual Typing Dead?
Research Papers
Asumu Takikawa Northeastern University, Daniel Feltey Northeastern University, Ben Greenman Northeastern University, Max New , Jan Vitek Northeastern University, Matthias Felleisen Northeastern University
Pre-print Media Attached File Attached
16:30 - 17:45
Track 1: OptimizationResearch Papers at Grand Bay North
Chair(s): Mayur Naik Georgia Tech
16:30
25m
Talk
SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization
Research Papers
Somashekaracharya G Bhaskaracharya Indian Institute of Science and National Instruments, Uday Bondhugula Indian Institute of Science, Albert Cohen INRIA
Media Attached File Attached
16:55
25m
Talk
PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs
Research Papers
Wenlei Bao , Sriram Krishnamoorthy Pacific Northwest National Laboratories, Louis-Noël Pouchet Ohio State University, Fabrice Rastello INRIA, France, P. Sadayappan Ohio State University
Media Attached
17:20
25m
Talk
Printing Floating-Point Numbers: A Faster, Always Correct Method
Research Papers
Marc Andrysco University of California, San Diego, Ranjit Jhala University of California, San Diego, Sorin Lerner University of California, San Diego
Media Attached
16:30 - 17:45
Track 2: Sessions and processesResearch Papers at Grand Bay South
Chair(s): Matteo Maffei Saarland University
16:30
25m
Talk
Effects as sessions, sessions as effects
Research Papers
Dominic Orchard Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print Media Attached
16:55
25m
Talk
Monitors and Blame Assignment for Higher-Order Session Types
Research Papers
Limin Jia Carnegie Mellon University, Hannah Gommerstadt Carnegie Mellon University, Frank Pfenning Carnegie Mellon University
Media Attached File Attached
17:20
25m
Talk
Environmental Bisimulations for Probabilistic Higher-Order Languages
Research Papers
Davide Sangiorgi University of Bologna, Valeria Vignudelli University of Bologna/INRIA
Media Attached
18:00 - 19:00
SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business MeetingResearch Papers at Grand Bay North
Chair(s): Michael Hicks University of Maryland at College Park, USA
19:00 - 20:00
POPL SRC Posters and ReceptionSRC at Lobby III
Chair(s): Zachary Tatlock University of Washington, Seattle

Fri 22 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Invited Speaker FriInvited Speakers at Grand Bay Ballroom
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
60m
Talk
Confluences in Programming Languages Research
Invited Speakers
David Walker Princeton University
Media Attached
10:30 - 12:10
Track 1: Program Design and AnalysisResearch Papers at Grand Bay North
Chair(s): Manu Sridharan Samsung Research America
10:30
25m
Talk
Newtonian Program Analysis via Tensor Product
Research Papers
Thomas Reps University of Wisconsin - Madison and Grammatech Inc., Emma Turetsky CS Dept., Univ. of Wisconsin-Madison, Prathmesh Prabhu Google
Media Attached
10:55
25m
Talk
Casper: An Efficient Approach to Call Trace Collection
Research Papers
Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao Xiao The Hong Kong University of Science and Technology, Shing-Chi Cheung Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu Zhang Microsoft Research, Charles Zhang HKUST
Media Attached
11:20
25m
Talk
Pushdown Control-flow Analysis for Free
Research Papers
Thomas Gilray University of Utah, Steven Lyde , Michael D. Adams University of Utah, Matthew Might University of Utah, USA, David Van Horn University of Maryland, College Park
Pre-print Media Attached
11:45
25m
Talk
Binding as Sets of Scopes
Research Papers
Matthew Flatt University of Utah
Pre-print Media Attached
10:30 - 12:10
Track 2: Semantics and memory modelsResearch Papers at Grand Bay South
Chair(s): Alexey Gotsman IMDEA
10:30
25m
Talk
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Research Papers
Shaked Flur University of Cambridge, Kathryn E. Gray University of Cambridge, Christopher Pulte University of Cambridge, Susmit Sarkar University of St Andrews, Luc Maranget INRIA Rocquencourt, Ali Sezgin University of Cambridge, Will Deacon ARM Ltd., Peter Sewell University of Cambridge
Media Attached File Attached
10:55
25m
Talk
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Research Papers
Jean Pichon-Pharabod University of Cambridge, Peter Sewell University of Cambridge
File Attached
11:20
25m
Talk
Overhauling SC atomics in C11 and OpenCL
Research Papers
John Wickerson Imperial College London, Mark Batty University of Cambridge, Alastair F. Donaldson Imperial College London
Pre-print File Attached
11:45
25m
Talk
Taming Release-Acquire Consistency
Research Papers
Ori Lahav MPI-SWS, Nick Giannarakis MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Pre-print Media Attached File Attached
14:20 - 16:00
Track 1: SynthesisResearch Papers at Grand Bay North
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:20
25m
Talk
Learning Programs from Noisy Data
Research Papers
Veselin Raychev ETH Zurich, Pavol Bielik ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Andreas Krause ETH Zurich
Link to publication DOI Pre-print Media Attached File Attached
14:45
25m
Talk
Optimizing Synthesis with Metasketches
Research Papers
James Bornholt University of Washington, Emina Torlak University of Washington, Dan Grossman University of Washington, USA, Luis Ceze University of Washington, USA
Pre-print Media Attached
15:10
25m
Talk
Maximal Specification Synthesis
Research Papers
Aws Albarghouthi University of Wisconsin–Madison, Isil Dillig University of Texas, Austin, Arie Gurfinkel Carnegie Mellon University
Pre-print Media Attached
15:35
25m
Talk
Example-Directed Synthesis: A Type-Theoretic Interpretation
Research Papers
Jonathan Frankle Princeton University, Peter-Michael Osera Grinnell College, David Walker Princeton University, Steve Zdancewic University of Pennsylvania
Pre-print Media Attached File Attached
14:20 - 15:35
Track 2: Foundations of Model CheckingResearch Papers at Grand Bay South
Chair(s): Alexandra Silva Radboud University Nijmegen
14:20
25m
Talk
Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
Research Papers
Ichiro Hasuo University of Tokyo, Shunsuke Shimizu University of Tokyo, Corina Cirstea University of Southampton
Media Attached
14:45
25m
Talk
Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
Research Papers
Media Attached
15:10
25m
Talk
Memoryful Geometry of Interaction II: Recursion and Adequacy
Research Papers
Koko Muroya University of Tokyo, Naohiko Hoshino Kyoto University, Ichiro Hasuo University of Tokyo
Media Attached

Sat 23 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Session OneOff the Beaten Track at Room St Petersburg I
Chair(s): Lindsey Kuper Intel Labs
09:00
15m
Day opening
Opening remarks and program chair's report
Off the Beaten Track
Lindsey Kuper Intel Labs
09:15
45m
Talk
Keynote Talk: Operationalizing Creative Theories
Off the Beaten Track
K: Chris Martens Carnegie Mellon University
09:00 - 10:00
Session 1PPS at Room St Petersburg II
Chair(s): Cameron Freer Gamalon
09:00
20m
Talk
All You Need is the Monad... What Monad Was That Again?
PPS
Pre-print
09:20
10m
Meeting
Discussion 1
PPS

09:30
20m
Talk
An Interface for Black Box Learning in Probabilistic Programs
PPS
Jan-Willem van de Meent University of Oxford, Brooks Paige University of Oxford, David Tolpin University of Oxford, Frank Wood University of Oxford
Pre-print
09:50
10m
Meeting
Discussion 2
PPS

10:30 - 12:15
Session 2PPS at Room St Petersburg II
Chair(s): Chad Scherrer Galois, Inc.
10:30
20m
Talk
Models for Probabilistic Programs with an Adversary
PPS
Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania
Pre-print
10:50
10m
Meeting
DIscussion 3
PPS

11:00
20m
Talk
The Semantics of Figaro, an Embedded Probabilistic Programming Language
PPS
Avi Pfeffer Charles River Analytics, Brian Ruttenberg Charles River Analytics
Pre-print
11:20
10m
Meeting
Discussion 4
PPS

11:30
45m
Meeting
Implementor Panel: What can semantics do for probabilistic programming and what can probabilistic programming do for semantics?
PPS
Angelika Kimmig KU Leuven, Oleg Kiselyov , Jan-Willem van de Meent University of Oxford, Avi Pfeffer Charles River Analytics, M: Frank Wood University of Oxford
14:00 - 15:35
Session ThreeOff the Beaten Track at Room St Petersburg I
Chair(s): Limin Jia Carnegie Mellon University
14:00
45m
Talk
Keynote Talk: Generalising Abstraction
Off the Beaten Track
K: Robert Atkey University of Strathclyde
14:45
25m
Talk
The Semantics of Syntax: Applying Denotational Semantics to Hygienic Macro Systems
Off the Beaten Track
Pre-print
15:10
25m
Talk
Affine Functional Programs as Higher-order Boolean Circuits
Off the Beaten Track
Pre-print
14:00 - 15:30
Session 3PPS at Room St Petersburg II
Chair(s): Mitchell Wand Northeastern University
14:00
20m
Talk
A Lambda-Calculus Foundation for Universal Probabilistic Programming
PPS
Johannes Borgström Uppsala University, Ugo Dal Lago University of Bologna, Andrew D. Gordon Microsoft Research and University of Edinburgh, Marcin Szymczak University of Edinburgh
Pre-print
14:20
10m
Meeting
Discussion 5
PPS

14:30
20m
Talk
Making our Own Luck: A Language for Random Generators
PPS
Leonidas Lampropoulos University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Cătălin Hriţcu INRIA Paris, John Hughes Chalmers University of Technology, Zoe Paraskevopoulou Princeton University, Li-yao Xia ENS Paris
Pre-print
14:50
10m
Meeting
Discussion 6
PPS

15:00
20m
Talk
Semantics of Higher-order Probabilistic Programs
PPS
Sam Staton University of Oxford, Hongseok Yang University of Oxford, UK, Chris Heunen University of Edinburgh, Ohad Kammar University of Cambridge, Frank Wood University of Oxford
Pre-print
15:20
10m
Meeting
Discussion 7
PPS

15:30 - 16:30
Poster SessionPPS at Room St Petersburg II
15:30
60m
Meeting
Insomnia: Types and Modules for Probabilistic Programming
PPS
Aleksey Kliger Xamarin, Inc., Sean Stromsten BAE Systems, Inc.
Pre-print
15:30
60m
Meeting
Finite-depth Higher-order Abstract Syntax Trees for Reasoning about Probabilistic Programs
PPS
Theophilos Giannakopoulos BAE Systems, Inc., Mitchell Wand Northeastern University, Andrew Cobb Northeastern University
Pre-print
15:30
60m
Meeting
Coalgebraic Trace Semantics for Probabilistic Processes: Preliminary Proposal
PPS
Larry Moss Indiana University, Chung-chieh Shan Indiana University, Alexandra Silva Radboud University Nijmegen
Pre-print
15:30
60m
Meeting
Reasoning about Probability and Nondeterminism
PPS
Faris Abou-Saleh University of Oxford, Kwok-Ho Cheung University of Oxford, Jeremy Gibbons University of Oxford, UK
Pre-print
15:30
60m
Meeting
Fixed Points for Markov Decision Processes
PPS
Johannes Hölzl Technische Universität München
Pre-print
15:30
60m
Meeting
A Denotational Semantics of a Probabilistic Stream-Processing Language
PPS
Yohei Miyamoto Graduate School of Informatics, Kyoto University, Kohei Suenaga , Koji Nakazawa Graduate School of Information Science, Nagoya University
Pre-print
15:30
60m
Meeting
Observation Propagation for Importance Sampling with Likelihood Weighting
PPS
Ryan Culpepper Northeastern University
Pre-print
15:30
60m
Meeting
Problems of the Lightweight Implementation of Probabilistic Programming
PPS
Pre-print
15:30
60m
Meeting
Parameterized Probability Monad
PPS
Adam Ścibior University of Cambridge, Andrew D. Gordon Microsoft Research and University of Edinburgh
Pre-print
15:30
60m
Meeting
Reproducing Kernel Hilbert Space Semantics for Probabilistic Programs
PPS
Adam Ścibior University of Cambridge, Bernhard Schölkopf MPI Tuebingen
Pre-print
16:30 - 18:00
Session 5PPS at Room St Petersburg II
Chair(s): Chung-chieh Shan Indiana University
16:30
20m
Talk
eXchangeable Random Primitives
PPS
Nathanael L. Ackerman Harvard University, Cameron Freer Gamalon, Daniel Roy University of Toronto
Pre-print
16:50
10m
Meeting
Discussion 8
PPS

17:00
20m
Talk
An Application of Computable Distributions to the Semantics of Probabilistic Programs
PPS
Daniel Huang Harvard University, Greg Morrisett Cornell University
Pre-print
17:20
10m
Meeting
Discussion 9
PPS

17:30
20m
Talk
On The Semantic Intricacies of Conditioning
PPS
Friedrich Gretz RWTH Aachen University, Nils Jansen RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Federico Olmedo RWTH Aachen University
Pre-print
17:50
10m
Meeting
Discussion 10
PPS