Program - POPL 2016

Write a Blog >>

Wed 20 - Sat 23 January 2016 St. Petersburg, Florida, United States

Filter

Sun 17 Jan

08:50 - 09:00: VMCAI - Welcome at Room St Petersburg I
Chair(s): K. Rustan M. Leino

09:00 - 10:00: VMCAI - Invited Talk I at Room St Petersburg I
Chair(s): Sharon Shoham

09:00 - 10:00
Talk

Automating Abstract Interpretation

10:30 - 12:00: VMCAI - Abstract Interpretation at Room St Petersburg I
Chair(s): Peter Müller

10:30 - 11:00
Talk

An Abstract Domain of Uninterpreted Functions

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard, Peter Stuckey

11:00 - 11:30
Talk

Predicate Abstraction for Linked Data Structures

Alexander Bakst, Ranjit Jhala

11:30 - 12:00
Talk

Property Directed Abstract Interpretation

Noam Rinetzky, Sharon Shoham

14:00 - 15:30: VMCAI - Abstraction I at Room St Petersburg I
Chair(s): Eva Darulova

14:00 - 14:30
Talk

Program Analysis with Local Policy Iteration

Egor Karpenkov, David Monniaux, Philipp Wendler

14:30 - 15:00
Talk

Lazy Constrained Monotonic Abstraction

Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng

15:00 - 15:30
Talk

Polyhedral Approximation of Multivariate Polynomials using Handelman’s Theorem

Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michael Perin

16:00 - 17:00: VMCAI - Abstraction II at Room St Petersburg I
Chair(s): David Pichardie

16:00 - 16:30
Talk

D3 : Data-Driven Disjunctive Abstraction

Hila Peleg, Sharon Shoham, Eran Yahav

16:30 - 17:00
Talk

Exact Heap Summaries for Symbolic Execution

Benjamin Hillery, Eric Mercer, Neha Rungta, Suzette Person

Mon 18 Jan

08:30 - 10:00: Invited Talks - Invited talks 0 & 1 at Room Demens

08:30 - 09:15
Talk

Invited Talk: Learning from Big Code: Probabilistic Models, Program Analysis and Synthesis

09:15 - 10:00
Talk

Invited Talk: Tracing JITs for Functional Languages

Sam Tobin-Hochstadt

08:30 - 10:00: Tutorials - T1: An Introduction to Redex with Abstracting Abstract Machines at Room HTC 1

08:30 - 10:00
Talk

T1: An Introduction to Redex with Abstracting Abstract Machines

Link to publication

08:30 - 10:00: Tutorials - T3: Syntax-Guided Synthesis (SyGuS) at Room HTC 2

08:30 - 10:00
Talk

T3: Syntax-Guided Synthesis (SyGuS)

Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama

Link to publication

08:30 - 10:00: Tutorials - T5: Higher-Order Model Checking at Room HTC 3

08:30 - 10:00
Talk

T5: Higher-Order Model Checking

Naoki Kobayashi, C.-H. Luke Ong

08:45 - 09:00: PADL - Welcome at Room Bayboro
Chair(s): John Reppy

09:00 - 10:00: PADL - Invited Talk at Room Bayboro

09:00 - 10:00
Talk

Program Synthesis for Direct Manipulation Interfaces

09:00 - 10:00: VMCAI - Invited Talk II at Room St Petersburg I
Chair(s): K. Rustan M. Leino

09:00 - 10:00
Talk

Ironclad - Full Verification of Complex Systems

09:00 - 10:00: CPP - Session 1: Invited talk by Harvey Friedman at Room St Petersburg II

09:00 - 10:00
Talk

Perspectives on Formal Verfication

Harvey Friedman

10:30 - 12:00: PADL - Functional Programming I at Room Bayboro

10:30 - 11:00
Talk

Simplifying Probabilistic Programs Using Computer Algebra

Jacques Carette, Chung-chieh Shan

11:00 - 11:30
Talk

Haskino: A Remote Monad for Programming the Arduino

Mark Grebe, Andy Gill

11:30 - 12:00
Talk

From Monads to Effects and Back

Niki Vazou, Daan Leijen

10:30 - 12:00: VMCAI - Hybrid and Timed Systems at Room St Petersburg I
Chair(s): David Monniaux

10:30 - 11:00
Talk

Abstract Interpretation with Infinitesimals

Kengo Kido, Swarat Chaudhuri, Ichiro Hasuo

11:00 - 11:30
Talk

Lipschitz Robustness of Timed I/O Systems

Thomas A. Henzinger, Jan Otop, Roopsha Samanta

11:30 - 12:00
Talk

A method for invariant generation for polynomial continuous systems

Andrew Sogokon, Khalil Ghorbal, Paul Jackson, André Platzer

10:30 - 12:00: Invited Talks - Invited talks 2 & 3 at Room Demens

10:30 - 11:15
Talk

Invited Talk: Using Formal Methods to Eliminate Exploitable Bugs

Kathleen Fisher

11:15 - 12:00
Talk

Invited Talk: Automated Reasoning about Type Systems by Compilation to First-Order Logic

Sebastian Erdweg

10:30 - 12:00: CPP - Session 2: Verifying Imperative Programs at Room St Petersburg II

10:30 - 11:00
Talk

Higher-order Representation Predicates in Separation Logic

Arthur Charguéraud

11:00 - 11:30
Talk

A Unified Coq Framework for Verifying C Programs with Floating-Point Computations

Tahina Ramananandro, Paul Mountcastle, Benoit Meister, Richard Lethin

11:30 - 12:00
Talk

Refinement Based Verification of Imperative Data Structures

10:30 - 12:00: Tutorials - T2: Declare Your Language: Part 1 at Room HTC 1

10:30 - 12:00
Talk

T2: Declare Your Language (Part 1): Hands-On Spoofax Tutorial

10:30 - 12:00: Tutorials - T3: Syntax-Guided Synthesis (SyGuS) at Room HTC 2

10:30 - 12:00
Talk

T3: Syntax-Guided Synthesis (SyGuS) (Advanced Material)

Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama

Link to publication

10:30 - 12:00: Tutorials - T4: Programs and Proofs in the Coq Proof Assistant at Room HTC 3

10:30 - 12:00
Talk

T4: Programs and Proofs in the Coq Proof Assistant

Robert Rand, Arthur Azevedo de Amorim

Link to publication

10:30 - 12:00: Tutorials - T6: Security and Privacy by Typing in Cryptographic Systems at Room HTC 4

10:30 - 12:00
Talk

T6: Security and Privacy by Typing in Cryptographic Systems

14:00 - 15:30: Tutorials - T6: Security and Privacy by Typing in Cryptographic Systems at Room HTC 4

14:00 - 15:30
Talk

T6: Security and Privacy by Typing in Cryptographic Systems

14:00 - 15:30: PADL - Constraints at Room Bayboro

14:00 - 14:30
Talk

A GPU implementation of the ASP computation

Agostino Dovier, Andrea Formisano, Enrico Pontelli, Flavio Vella

14:30 - 15:00
Talk

Using Constraint Logic Programming to Schedule Solar Array Operations on the International Space Station

Jan Jelínek, Roman Barták

15:00 - 15:30
Talk

The Picat-SAT Compiler

Neng-Fa Zhou, Håkan Kjellerstrand

14:00 - 15:30: VMCAI - Dynamic and Static Verification at Room St Petersburg I
Chair(s): Aarti Gupta

14:00 - 14:30
Talk

Hybrid Analysis for Partial Order Reduction of Programs with Arrays

14:30 - 15:00
Talk

Cloud-Based Verification of Concurrent Software

Gerald Holzmann

15:00 - 15:30
Talk

Abstraction-driven Concolic Testing

Przemyslaw Daca, Ashutosh Gupta, Thomas A. Henzinger

14:00 - 15:30: Invited Talks - Invited talks 4 & 5 at Room Demens

14:00 - 14:45
Talk

Invited Talk: Program Synthesis: Opportunities for the next Decade

Rastislav Bodik

14:45 - 15:30
Talk

Invited Talk: LMS: a Perspective on Generative Programming

14:00 - 15:30: CPP - Session 3: Design and Implementation of Theorem Provers at Room St Petersburg II

14:00 - 14:30
Talk

The Vampire and the FOOL

Evgenii Kotelnikov, Laura Kovacs, Giles Reger, Andrei Voronkov

14:30 - 15:00
Talk

Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions

15:00 - 15:30
Talk

Mizar Environment for Isabelle

Cezary Kaliszyk, Karol Pąk, Josef Urban

14:00 - 15:30: Tutorials - T1: An Introduction to Redex with Abstracting Abstract Machines at Room HTC 1

14:00 - 15:30
Talk

T1: An Introduction to Redex with Abstracting Abstract Machines(Advanced Material)

Link to publication

14:00 - 15:30: Tutorials - T4: Programs and Proofs in the Coq Proof Assistant at Room HTC 3

14:00 - 15:30
Talk

T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material)

Robert Rand, Arthur Azevedo de Amorim

Link to publication

14:00 - 15:30: Tutorials - T7: Trace-based Synchronization Synthesis for Concurrent Programs at Room HTC 2

14:00 - 15:30
Talk

T7: Trace-based Synchronization Synthesis for Concurrent Programs

Arjun Radhakrishna, Roopsha Samanta

16:00 - 17:30: Invited Talks - Invited talks 6 & 7 at Room Demens

16:00 - 16:45
Talk

Invited Talk: Fiat: Extensible Code Generation with Proofs

16:45 - 17:30
Talk

Invited Talk: The Promise of Relational Programming

William E. Byrd

16:00 - 17:00: PADL - Logic Programming at Room Bayboro

16:00 - 16:30
Talk

The KB paradigm and its application to interactive configuration

Pieter Van Hertum, Ingmar Dasseville, Gerda Janssens, Marc Denecker

16:30 - 17:00
Talk

Default Rules for Curry

Sergio Antoy, Michael Hanus

16:00 - 17:00: VMCAI - Probabilistic Systems at Room St Petersburg I
Chair(s): Paul Jackson

16:00 - 16:30
Talk

Reward-Bounded Reachability Probability for Uncertain Weighted MDPs

Vahid Hashemi, Holger Hermanns, Lei Song

16:30 - 17:00
Talk

Parameter Synthesis for Parametric Interval Markov Chains

Benoit Delahaye, Didier Lime, Laure Petrucci

16:00 - 18:00: CPP - Session 4: Mathematics at Room St Petersburg II

16:00 - 16:30
Talk

A Modular, Efficient Formalisation of Real Algebraic Numbers

Wenda Li, Lawrence Paulson

16:30 - 17:00
Talk

Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials

Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub

17:00 - 17:30
Talk

Formalizing Jordan Normal Forms in Isabelle/HOL

René Thiemann, Akihisa Yamada

17:30 - 18:00
Talk

Formalization of a Newton series representation of polynomials

Cyril Cohen, Boris Djalal

16:00 - 17:30: Tutorials - T2: Declare Your Language: Part 2 at Room HTC 1

16:00 - 17:30
Talk

T2: Declare Your Language (Part 2): Name Binding with Scope Graphs

Link to publication DOI Media Attached

16:00 - 17:30: Tutorials - T5: Higher-Order Model Checking at Room HTC 3

16:00 - 17:30
Talk

T5: Higher-Order Model Checking

Naoki Kobayashi, C.-H. Luke Ong

16:00 - 17:30: Tutorials - T7: Trace-based Synchronization Synthesis for Concurrent Programs at Room HTC 2

16:00 - 17:30
Talk

T7: Trace-based Synchronization Synthesis for Concurrent Programs

Arjun Radhakrishna, Roopsha Samanta

Tue 19 Jan

08:50 - 09:00: PLMW - Welcome Session at Room St Petersburg III

09:00 - 10:00: VMCAI - Invited Talk III at Room St Petersburg I
Chair(s): Bor-Yuh Evan Chang

09:00 - 10:00
Talk

Viper - A Verification Infrastructure for Permission-based Reasoning

09:00 - 10:00: Invited Talks - Keynote at Room Demens

09:00 - 10:00
Talk

Invited Keynote: Building Languages in Racket: Syntax Objects as an Intermediate Representation

09:00 - 10:00: CPP - Session 5: Invited talk by Leonardo de Moura at Room St Petersburg II

09:00 - 10:00
Talk

Dependent Type Practice

Leonardo De Moura

09:00 - 10:00: PLMW - Session I at Room St Petersburg III

09:00 - 09:30
Talk

Grad School: A Survival Guide

09:30 - 10:00
Talk

Theorem Provers are a PL Researcher's Best Friend

10:30 - 12:00: VMCAI - Concurrent Programs at Room St Petersburg I
Chair(s): Noam Rinetzky

10:30 - 11:00
Talk

Pointer Race Freedom

Frédéric Haziza, Lukas Holik, Roland Meyer, Sebastian Wolff

11:00 - 11:30
Talk

A program logic for C11 memory fences

Marko Doko, Viktor Vafeiadis

11:30 - 12:00
Talk

From Low Level Pointers to High Level Containers

Kamil Dudka, Lukas Holik, Petr Peringer, Tomas Vojnar

10:30 - 12:00: PADL - Functional Programming II at Room Bayboro

10:30 - 11:00
Talk

Computing with Catalan Families, Generically

11:00 - 11:30
Talk

A Size-proportionate Bijective Encoding of Lambda Terms as Catalan Objects endowed with Arithmetic Operations

11:30 - 12:00
Talk

Generic Matching of Tree Regular Expressions over Haskell Data Types

Alejandro Serrano, Jurriaan Hage

10:30 - 12:00: PEPM - Parsing & Domain-Specific Languages I at Room Harbor View
Chair(s): Kenichi Asai

10:30 - 11:00
Talk

Practical, General Parser Combinators

Anastasia Izmaylova, Ali Afroozeh, Tijs van der Storm

11:00 - 11:30
Talk

Operator Precedence for Data-Dependent Grammars

Ali Afroozeh, Anastasia Izmaylova

11:30 - 12:00
Talk

Everything Old Is New Again: Quoted Domain-Specific Languages

Shayan Najd, Sam Lindley, Josef Svenningsson, Philip Wadler

10:30 - 12:00: CPP - Session 6: Foundations at Room St Petersburg II

10:30 - 11:00
Talk

A Logic of Proofs for Differential Dynamic Logic

Nathan Fulton, André Platzer

11:00 - 11:30
Talk

Constructing the Propositional Truncation using Non-recursive HITs

Floris van Doorn

11:30 - 12:00
Talk

A Nominal Exploration of Intuitionism

Vincent Rahli, Mark Bickford

10:30 - 12:00: PLMW - Session II at Room St Petersburg III

10:30 - 11:00
Talk

Academia or Industry?

11:00 - 11:30
Talk

Refining Types with SMT

11:30 - 12:00
Talk

How to Write Papers So People Can Read Them

14:00 - 15:30: PEPM - Domain-Specific Languages II at Room Harbor View
Chair(s): Sebastian Erdweg

14:00 - 14:30
Talk

BiGUL: A Formally Verified Core Language for Putback-Based Bidirectional Programming

Hsiang-Shang ‘Josh’ Ko, Tao Zan, Zhenjiang Hu

14:30 - 15:00
Talk

A Constraint Language for Static Semantic Analysis Based on Scope Graphs

Hendrik van Antwerpen, Pierre Neron, Andrew Tolmach, Eelco Visser, Guido Wachsmuth

Link to publication DOI Pre-print

15:00 - 15:30
Talk

Finally, Safely-Extensible and Efficient Language-Integrated Query

Kenichi Suzuki, Oleg Kiselyov, Yukiyoshi Kameyama

14:00 - 15:30: VMCAI - Parameterized and Component-Based Systems at Room St Petersburg I
Chair(s): Arie Gurfinkel

14:00 - 14:30
Talk

Regular Symmetry Patterns

Anthony Widjaja Lin, Truong Khanh Nguyen, Philipp Ruemmer, Jun Sun

14:30 - 15:00
Talk

Tight Cutoffs for Guarded Protocols with Fairness

Simon Außerlechner, Swen Jacobs, Ayrat Khalimov

15:00 - 15:30
Talk

A General Modular Synthesis Problem for Pushdown Systems

Ilaria De Crescenzo, Salvatore La Torre

14:00 - 15:30: CPP - Session 7: Verification for Concurrent and Distributed Systems at Room St Petersburg II

14:00 - 14:30
Talk

Bisimulation Up-to Techniques for Psi-calculi

Johannes Å. Pohjola, Joachim Parrow

14:30 - 15:00
Talk

Planning for Change in a Formal Verification of the Raft Consensus Protocol

Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas Anderson

15:00 - 15:30
Talk

A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules

Michel St-Martin, Amy Felty

14:00 - 15:30: PLMW - Session III at Room St Petersburg III

14:00 - 14:30
Talk

Student Interaction Activity

Isil Dillig, Ross Tate

14:30 - 15:00
Talk

Automata and Coinduction

Alexandra Silva

15:00 - 15:30
Talk

Unaccustomed As I Am to Public Speaking

16:00 - 17:00: CPP - Session 8: Compiler Verification at Room St Petersburg II

16:00 - 16:30
Talk

Formal Verification of Control-flow Graph Flattening

Sandrine Blazy, Alix Trieu

16:30 - 17:00
Talk

Axiomatic Semantics for Compiler Verification

Steven Schäfer, Sigurd Schneider, Gert Smolka

16:00 - 17:00: PLMW - Session IV at Room St Petersburg III

16:00 - 16:30
Talk

Two Notions of Beauty in Programming

16:30 - 17:00
Talk

Highs and Lows of a Language Researcher

16:00 - 17:00: VMCAI - Solver Improvements at Room St Petersburg I
Chair(s): Roopsha Samanta

16:00 - 16:30
Talk

Model Checking with Multi-Threaded IC3 Portfolios

Sagar Chaki, Derrick Karimi

16:30 - 17:00
Talk

Automatic Generation of Propagation Complete SAT Encodings

Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins

16:00 - 17:40: PEPM - Staging at Room Harbor View
Chair(s): Jacques Carette

16:00 - 16:30
Talk

Staging Generic Programming

16:30 - 17:00
Talk

Removing Runtime Overhead for Optimized Object Queries

Jon Brandvein, Yanhong A. Liu

17:00 - 17:20
Talk

Toward Introducing Binding-Time Analysis to MetaOCaml

17:20 - 17:40
Talk

Staging beyond Terms: Prospects and Challenges

Jun Inoue, Oleg Kiselyov, Yukiyoshi Kameyama

17:00 - 17:45: PLMW - Session V at Room St Petersburg III

17:00 - 17:45
Talk

Young Researcher Panel Session, with panelists: Mark Batty (Kent), Mike Carbin (MIT), Lindsey Kuper (Intel), Ilya Sergey (UCL)

Dimitrios Vytiniotis

18:00 - 21:00: CPP - CPP Reception, sponsored by the DeepSpec project at Room St Petersburg I

18:00 - 21:00
Social Event

CPP Reception, sponsored by the DeepSpec project

Wed 20 Jan

09:00 - 10:00: Invited Speakers - Invited Wed at Grand Bay Ballroom
Chair(s): Rastislav Bodik

09:00 - 10:00
Talk

Programming the World of Uncertain Things

Kathryn S McKinley

10:30 - 12:10: Research Papers - Track 1: Algorithmic Verification at Grand Bay North
Chair(s): Arie Gurfinkel

10:30 - 10:55
Talk

Temporal Verification of Higher-order Functional Programs

Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

10:55 - 11:20
Talk

Scaling Network Verification using Symmetry and Surgery

Gordon Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese

11:20 - 11:45
Talk

Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates

James Brotherston, Nikos Gorogiannis, Max Kanovich, Reuben Rowe

11:45 - 12:10
Talk

Reducing Crash Recoverability to Reachability

Eric Koskinen, Junfeng Yang

10:30 - 12:10: Research Papers - Track 2: Types and Foundations at Grand Bay South
Chair(s): Bob Atkey

10:30 - 10:55
Talk

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

Matt Brown, Jens Palsberg

Media Attached File Attached

10:55 - 11:20
Talk

Type Theory in Type Theory using Quotient Inductive Types

Thorsten Altenkirch, Ambrus Kaposi

Media Attached File Attached

11:20 - 11:45
Talk

System Fω with Equirecursive Types for Datatype-generic Programming

Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann

11:45 - 12:10
Talk

A Theory of Effects and Resources: Adjunction Models and Polarised Calculi

Pierre-Louis Curien, Marcelo Fiore, Guillaume Munch-Maccagnoni

14:20 - 16:00: Research Papers - Track 1: Decision Procedures at Grand Bay North
Chair(s): Loris D'Antoni

14:20 - 14:45
Talk

Query-Guided Maximum Satisfiability

Xin Zhang, Ravi Mangal, Aditya Nori, Mayur Naik

14:45 - 15:10
Talk

String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS

Anthony Widjaja Lin, Pablo Barcelo

15:10 - 15:35
Talk

Symbolic Computation of Differential Equivalences

Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin

15:35 - 16:00
Talk

Unboundedness and Downward Closures of Higher-Order Pushdown Automata

Matthew Hague, Jonathan Kochems, C.-H. Luke Ong

14:20 - 16:00: Research Papers - Track 2: Correct Compilation at Grand Bay South
Chair(s): Jens Palsberg

14:20 - 14:45
Talk

Fully-Abstract Compilation by Approximate Back-Translation

Dominique Devriese, Marco Patrignani, Frank Piessens

Pre-print Media Attached

14:45 - 15:10
Talk

Lightweight Verification of Separate Compilation

Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis

Media Attached File Attached

15:10 - 15:35
Talk

From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes

Ed Robbins, Andy King, Tom Schrijvers

15:35 - 16:00
Talk

Sound Type-dependent Syntactic Language Extension

Florian Lorenzen, Sebastian Erdweg

Pre-print Media Attached File Attached

16:30 - 17:45: Research Papers - Track 1: Language Design at Grand Bay North
Chair(s): David Walker

16:30 - 16:55
Talk

Dependent Types and Multi-Monadic Effects in F*

Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, Santiago Zanella-Béguelin

Pre-print Media Attached

16:55 - 17:20
Talk

Fabular: Regression Formulas as Probabilistic Programming

Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio Russo, Adam Ścibior, Marcin Szymczak

17:20 - 17:45
Talk

Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers

Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm

16:30 - 17:45: Research Papers - Track 2: Decidability and complexity at Grand Bay South
Chair(s): C.-H. Luke Ong

16:30 - 16:55
Talk

Decidability of Inferring Inductive Invariants

Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv

16:55 - 17:20
Talk

The Hardness of Data Packing

Rahman Lavaee, Chen Ding

17:20 - 17:45
Talk

The Complexity of Interaction

Stéphane Gimenez, Georg Moser

19:00 - 22:00: Research Papers - Banquet at Dali Museum

Thu 21 Jan

09:00 - 10:00: Invited Speakers - Invited Speaker Thu at Grand Bay Ballroom
Chair(s): Rupak Majumdar

09:00 - 10:00
Talk

Synthesis of Reactive Controllers for Hybrid Systems

Richard M. Murray

10:30 - 12:10: Research Papers - Track 1: Foundations of distributed systems at Grand Bay North
Chair(s): Mooly Sagiv

10:30 - 10:55
Talk

Certified Causally Consistent Distributed Key-Value Stores

Mohsen Lesani, Christian J. Bell, Adam Chlipala

10:55 - 11:20
Talk

'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems

Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro

11:20 - 11:45
Talk

A Program Logic for Concurrent Objects under Fair Scheduling

Hongjin Liang, Xinyu Feng

11:45 - 12:10
Talk

PSync: a partially synchronous language for fault-tolerant distributed algorithms

Cezara Drăgoi, Thomas A. Henzinger, Damien Zufferey

Link to publication DOI Pre-print Media Attached File Attached

10:30 - 12:10: Research Papers - Track 2: Probabilistic and statistical analysis at Grand Bay South
Chair(s): Aditya Nori

10:30 - 10:55
Talk

Prophet: Automatic Patch Generation via Learning from Successful Patches

Fan Long, Martin Rinard

10:55 - 11:20
Talk

Estimating types in binaries using predictive modeling

Omer Katz, Ran El-Yaniv, Eran Yahav

Media Attached File Attached

11:20 - 11:45
Talk

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

Krishnendu Chatterjee, Hongfei Fu, Rouzbeh Hasheminezhad, Petr Novotny

11:45 - 12:10
Talk

Transforming Spreadsheet Data Types using Examples

Rishabh Singh, Sumit Gulwani

14:20 - 16:00: Research Papers - Track 1: Learning and verification at Grand Bay North
Chair(s): David Monniaux

14:20 - 14:45
Talk

Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis

Damien Octeau, Somesh Jha, Matthew Dering, Patrick McDaniel, Alexandre Bartel, Hongyu Li, Jacques Klein, Yves Le Traon

14:45 - 15:10
Talk

Abstraction Refinement Guided by a Learnt Probabilistic Model

Radu Grigore, Hongseok Yang

15:10 - 15:35
Talk

Learning Invariants using Decision Trees and Implication Counterexamples

Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth

15:35 - 16:00
Talk

Symbolic Abstract Data Type Inference

Michael Emmi, Constantin Enea

14:20 - 16:00: Research Papers - Track 2: Types, Generally or Gradually at Grand Bay South
Chair(s): Tiark Rompf

14:20 - 14:45
Talk

Principal Type Inference for GADTs

Sheng Chen, Martin Erwig

14:45 - 15:10
Talk

Abstracting Gradual Typing

Ronald Garcia, Alison M. Clark, Éric Tanter

Link to publication Media Attached

15:10 - 15:35
Talk

The Gradualizer: a methodology and algorithm for generating gradual type systems

Matteo Cimini, Jeremy G. Siek

15:35 - 16:00
Talk

Is Sound Gradual Typing Dead?

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, Matthias Felleisen

Pre-print Media Attached File Attached

16:30 - 17:45: Research Papers - Track 1: Optimization at Grand Bay North
Chair(s): Mayur Naik

16:30 - 16:55
Talk

SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization

Somashekaracharya G Bhaskaracharya, Uday Bondhugula, Albert Cohen

Media Attached File Attached

16:55 - 17:20
Talk

PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs

Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, Fabrice Rastello, P. Sadayappan

17:20 - 17:45
Talk

Printing Floating-Point Numbers: A Faster, Always Correct Method

Marc Andrysco, Ranjit Jhala, Sorin Lerner

16:30 - 17:45: Research Papers - Track 2: Sessions and processes at Grand Bay South
Chair(s): Matteo Maffei

16:30 - 16:55
Talk

Effects as sessions, sessions as effects

Dominic Orchard, Nobuko Yoshida

Pre-print Media Attached

16:55 - 17:20
Talk

Monitors and Blame Assignment for Higher-Order Session Types

Limin Jia, Hannah Gommerstadt, Frank Pfenning

Media Attached File Attached

17:20 - 17:45
Talk

Environmental Bisimulations for Probabilistic Higher-Order Languages

Davide Sangiorgi, Valeria Vignudelli

18:00 - 19:00: Research Papers - SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business Meeting at Grand Bay North
Chair(s): Michael Hicks

19:00 - 20:00: SRC - POPL SRC Posters and Reception at Lobby III
Chair(s): Zachary Tatlock

Fri 22 Jan

09:00 - 10:00: Invited Speakers - Invited Speaker Fri at Grand Bay Ballroom
Chair(s): Steve Zdancewic

09:00 - 10:00
Talk

Confluences in Programming Languages Research

10:30 - 12:10: Research Papers - Track 1: Program Design and Analysis at Grand Bay North
Chair(s): Manu Sridharan

10:30 - 10:55
Talk

Newtonian Program Analysis via Tensor Product

Thomas Reps, Emma Turetsky, Prathmesh Prabhu

10:55 - 11:20
Talk

Casper: An Efficient Approach to Call Trace Collection

Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang

11:20 - 11:45
Talk

Pushdown Control-flow Analysis for Free

Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn

Pre-print Media Attached

11:45 - 12:10
Talk

Binding as Sets of Scopes

Pre-print Media Attached

10:30 - 12:10: Research Papers - Track 2: Semantics and memory models at Grand Bay South
Chair(s): Alexey Gotsman

10:30 - 10:55
Talk

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA

Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Luc Maranget, Ali Sezgin, Will Deacon, Peter Sewell

Media Attached File Attached

10:55 - 11:20
Talk

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

Jean Pichon-Pharabod, Peter Sewell

11:20 - 11:45
Talk

Overhauling SC atomics in C11 and OpenCL

John Wickerson, Mark Batty, Alastair Donaldson

Pre-print File Attached

11:45 - 12:10
Talk

Taming Release-Acquire Consistency

Ori Lahav, Nick Giannarakis, Viktor Vafeiadis

Pre-print Media Attached File Attached

14:20 - 16:00: Research Papers - Track 1: Synthesis at Grand Bay North
Chair(s): Roberto Giacobazzi

14:20 - 14:45
Talk

Learning Programs from Noisy Data

Veselin Raychev, Pavol Bielik, Martin Vechev, Andreas Krause

Link to publication DOI Pre-print Media Attached File Attached

14:45 - 15:10
Talk

Optimizing Synthesis with Metasketches

James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze

Pre-print Media Attached

15:10 - 15:35
Talk

Maximal Specification Synthesis

Aws Albarghouthi, Isil Dillig, Arie Gurfinkel

Pre-print Media Attached

15:35 - 16:00
Talk

Example-Directed Synthesis: A Type-Theoretic Interpretation

Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic

Pre-print Media Attached File Attached

14:20 - 15:35: Research Papers - Track 2: Foundations of Model Checking at Grand Bay South
Chair(s): Alexandra Silva

14:20 - 14:45
Talk

Lattice-Theoretic Progress Measures and Coalgebraic Model Checking

Ichiro Hasuo, Shunsuke Shimizu, Corina Cirstea

14:45 - 15:10
Talk

Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components

Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis

15:10 - 15:35
Talk

Memoryful Geometry of Interaction II: Recursion and Adequacy

Koko Muroya, Naohiko Hoshino, Ichiro Hasuo

Sat 23 Jan

09:00 - 10:00: PPS 2016 - Session 1 at Room St Petersburg II
Chair(s): Cameron Freer

09:00 - 09:20
Talk

All You Need is the Monad... What Monad Was That Again?

09:20 - 09:30
Meeting

09:30 - 09:50
Talk

An Interface for Black Box Learning in Probabilistic Programs

Jan-Willem van de Meent, Brooks Paige, David Tolpin, Frank Wood

09:50 - 10:00
Meeting

09:00 - 10:00: CoqPL - Session I at Room St Petersburg III

09:00 - 10:00
Talk

Coq 8.5 at work and the future of Coq

Matthieu Sozeau

09:00 - 10:00: Off the Beaten Track - Session One at Room St Petersburg I
Chair(s): Lindsey Kuper

09:00 - 09:15
Day opening

Opening remarks and program chair's report

09:15 - 10:00
Talk

Keynote Talk: Operationalizing Creative Theories

10:30 - 12:15: PPS 2016 - Session 2 at Room St Petersburg II
Chair(s): Chad Scherrer

10:30 - 10:50
Talk

Models for Probabilistic Programs with an Adversary

Robert Rand, Steve Zdancewic

10:50 - 11:00
Meeting

11:00 - 11:20
Talk

The Semantics of Figaro, an Embedded Probabilistic Programming Language

Avi Pfeffer, Brian Ruttenberg

11:20 - 11:30
Meeting

11:30 - 12:15
Meeting

Implementor Panel: What can semantics do for probabilistic programming and what can probabilistic programming do for semantics?

Angelika Kimmig, Oleg Kiselyov, Jan-Willem van de Meent, Avi Pfeffer, Frank Wood

10:30 - 12:05: CoqPL - Session II at Room St Petersburg III

10:30 - 10:55
Talk

A Coq Library for Binary Logical Relations

Jérémie Koenig

Link to publication

10:55 - 11:20
Talk

A Coinduction Proof Rule for Hoare Doubles

Christian J. Bell

Link to publication

11:20 - 11:45
Talk

Formalizing Simple Refinements in Coq

Nicolás Lehmann, Éric Tanter

Link to publication

11:45 - 12:05
Talk

Company-Coq: Taking Proof General one step closer to a real IDE

Clément Pit-Claudel, Pierre Courtieu

Link to publication

10:30 - 12:10: Off the Beaten Track - Session Two at Room St Petersburg I
Chair(s): Suresh Jagannathan

10:30 - 10:55
Talk

Chanakya: Computer-Aided Strategic Reasoning

Suguman Bansal, Swarat Chaudhuri

10:55 - 11:20
Talk

Programming Interactivity Requires Both Semantics and Semiotics

Joseph Osborn, Michael Mateas

11:20 - 11:45
Talk

Correct-by-Construction Interactive Software: From Declarative Specifications to Efficient Implementations

Kyle Headley, Matthew Hammer

11:45 - 12:10
Talk

Challenges Facing a High-Level Language for Machine Knitting

Lea Albaugh, James McCann

14:00 - 15:30: PPS 2016 - Session 3 at Room St Petersburg II
Chair(s): Mitchell Wand

14:00 - 14:20
Talk

A Lambda-Calculus Foundation for Universal Probabilistic Programming

Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak

14:20 - 14:30
Meeting

14:30 - 14:50
Talk

Making our Own Luck: A Language for Random Generators

Leonidas Lampropoulos, Benjamin C. Pierce, Cătălin Hriţcu, John Hughes, Zoe Paraskevopoulou, Li-yao Xia

14:50 - 15:00
Meeting

15:00 - 15:20
Talk

Semantics of Higher-order Probabilistic Programs

Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, Frank Wood

15:20 - 15:30
Meeting

14:00 - 15:25: CoqPL - Session III at Room St Petersburg III

14:00 - 15:00
Talk

A Tutorial on using the Paco Library for coinductive reasoning

15:00 - 15:25
Talk

Certified Desugaring of Javascript Programs using Coq

Link to publication

14:00 - 15:35: Off the Beaten Track - Session Three at Room St Petersburg I
Chair(s): Limin Jia

14:00 - 14:45
Talk

Keynote Talk: Generalising Abstraction

14:45 - 15:10
Talk

The Semantics of Syntax: Applying Denotational Semantics to Hygienic Macro Systems

Neelakantan R. Krishnaswami

15:10 - 15:35
Talk

Affine Functional Programs as Higher-order Boolean Circuits

15:30 - 16:30: PPS 2016 - Poster Session at Room St Petersburg II

15:30 - 16:30
Meeting

Insomnia: Types and Modules for Probabilistic Programming

Aleksey Kliger, Sean Stromsten

15:30 - 16:30
Meeting

Finite-depth Higher-order Abstract Syntax Trees for Reasoning about Probabilistic Programs

Theophilos Giannakopoulos, Mitchell Wand, Andrew Cobb

15:30 - 16:30
Meeting

Coalgebraic Trace Semantics for Probabilistic Processes: Preliminary Proposal

Larry Moss, Chung-chieh Shan, Alexandra Silva

15:30 - 16:30
Meeting

Reasoning about Probability and Nondeterminism

Faris Abou-Saleh, Kwok-Ho Cheung, Jeremy Gibbons

15:30 - 16:30
Meeting

Fixed Points for Markov Decision Processes

Johannes Hölzl

15:30 - 16:30
Meeting

A Denotational Semantics of a Probabilistic Stream-Processing Language

Yohei Miyamoto, Kohei Suenaga, Koji Nakazawa

15:30 - 16:30
Meeting

Observation Propagation for Importance Sampling with Likelihood Weighting

15:30 - 16:30
Meeting

Problems of the Lightweight Implementation of Probabilistic Programming

15:30 - 16:30
Meeting

Parameterized Probability Monad

Adam Ścibior, Andrew D. Gordon

15:30 - 16:30
Meeting

Reproducing Kernel Hilbert Space Semantics for Probabilistic Programs

Adam Ścibior, Bernhard Schölkopf

16:00 - 17:30: Off the Beaten Track - Session Four at Room St Petersburg I
Chair(s): Nada Amin

16:00 - 16:25
Talk

Declarative, Secure, Convergent Edge Computation

Christopher Meiklejohn

16:25 - 16:50
Talk

Starting from a Clean Slate: Creating a Top-down Parseable Runtime

Randolph Langley

16:50 - 17:15
Talk

New Tools and Practices for Online Collaboration in Teaching, Learning, and Research of Programming Languages

William E. Byrd

17:15 - 17:30
Day closing

Closing remarks

16:00 - 18:00: CoqPL - Session IV at Room St Petersburg III

16:00 - 16:25
Talk

The Category-theoretic Solution of Recursive Ultra-metric Space Equations

Amin Timany, Bart Jacobs

Link to publication

16:25 - 16:50
Talk

A Case for Tactics with (Limited) Side Effects

Benjamin Delaware

16:50 - 17:15
Talk

Formal Verification of Stability Properties of Cyber-Physical Systems

Matthew Chan, Daniel Ricketts, Sorin Lerner, Gregory Malecha

Link to publication

17:15 - 17:45
Talk

The Science of Deep Specification

17:45 - 18:00
Talk

16:30 - 18:00: PPS 2016 - Session 5 at Room St Petersburg II
Chair(s): Chung-chieh Shan

16:30 - 16:50
Talk

eXchangeable Random Primitives

Nathanael L. Ackerman, Cameron Freer, Daniel Roy

16:50 - 17:00
Meeting

17:00 - 17:20
Talk

An Application of Computable Distributions to the Semantics of Probabilistic Programs

Daniel Huang, Greg Morrisett

17:20 - 17:30
Meeting

17:30 - 17:50
Talk

On The Semantic Intricacies of Conditioning

Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo

17:50 - 18:00
Meeting

Sun 17 Jan 2016


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Room St Petersburg I											VMCAI Welcome 08:50 - 09:00		VMCAI Invited Talk I 09:00 - 10:00																		VMCAI Abstract Interpretation 10:30 - 12:00																																										VMCAI Abstraction I 14:00 - 15:30																								VMCAI Abstraction II 16:00 - 17:00

Mon 18 Jan 2016


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Room Bayboro										PADL Welcome 08:45 - 09:00			PADL Invited Talk 09:00 - 10:00																		PADL Functional Programming I 10:30 - 12:00																																										PADL Constraints 14:00 - 15:30																								PADL Logic Programming 16:00 - 17:00
Room Demens							Invited Talks Invited talks 0 & 1 08:30 - 10:00																								Invited Talks Invited talks 2 & 3 10:30 - 12:00																																										Invited Talks Invited talks 4 & 5 14:00 - 15:30																								Invited Talks Invited talks 6 & 7 16:00 - 17:30
Room HTC 1							Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines 08:30 - 10:00																								Tutorials T2: Declare Your Language: Part 1 10:30 - 12:00																																										Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines 14:00 - 15:30																								Tutorials T2: Declare Your Language: Part 2 16:00 - 17:30
Room HTC 2							Tutorials T3: Syntax-Guided Synthesis (SyGuS) 08:30 - 10:00																								Tutorials T3: Syntax-Guided Synthesis (SyGuS) 10:30 - 12:00																																										Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 14:00 - 15:30																								Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 16:00 - 17:30
Room HTC 3							Tutorials T5: Higher-Order Model Checking 08:30 - 10:00																								Tutorials T4: Programs and Proofs in the Coq Proof Assistant 10:30 - 12:00																																										Tutorials T4: Programs and Proofs in the Coq Proof Assistant 14:00 - 15:30																								Tutorials T5: Higher-Order Model Checking 16:00 - 17:30
Room HTC 4																															Tutorials T6: Security and Privacy by Typing in Cryptographic Systems 10:30 - 12:00																																										Tutorials T6: Security and Privacy by Typing in Cryptographic Systems 14:00 - 15:30
Room St Petersburg I													VMCAI Invited Talk II 09:00 - 10:00																		VMCAI Hybrid and Timed Systems 10:30 - 12:00																																										VMCAI Dynamic and Static Verification 14:00 - 15:30																								VMCAI Probabilistic Systems 16:00 - 17:00
Room St Petersburg II													CPP Session 1: Invited talk by Harvey Friedman 09:00 - 10:00																		CPP Session 2: Verifying Imperative Programs 10:30 - 12:00																																										CPP Session 3: Design and Implementation of Theorem Provers 14:00 - 15:30																								CPP Session 4: Mathematics 16:00 - 18:00

Tue 19 Jan 2016


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30						21:00						30
Room Bayboro																															PADL Functional Programming II 10:30 - 12:00
Room Demens													Invited Talks Keynote 09:00 - 10:00																		PEPM 10:30 - 12:00																																										PEPM 14:00 - 15:30																								PEPM 16:00 - 17:40
Room Harbor View																															PEPM Parsing & Domain-Specific Languages I 10:30 - 12:00																																										PEPM Domain-Specific Languages II 14:00 - 15:30																								PEPM Staging 16:00 - 17:40
Room St Petersburg I													PADL VMCAI Invited Talk III 09:00 - 10:00																		VMCAI Concurrent Programs 10:30 - 12:00																																										VMCAI Parameterized and Component-Based Systems 14:00 - 15:30																								VMCAI Solver Improvements 16:00 - 17:00																								CPP CPP Reception, sponsored by the DeepSpec project 18:00 - 21:00
Room St Petersburg II													CPP Session 5: Invited talk by Leonardo de Moura 09:00 - 10:00																		CPP Session 6: Foundations 10:30 - 12:00																																										CPP Session 7: Verification for Concurrent and Distributed Systems 14:00 - 15:30																								CPP Session 8: Compiler Verification 16:00 - 17:00
Room St Petersburg III											PLMW Welcome Session 08:50 - 09:00		PLMW Session I 09:00 - 10:00																		PLMW Session II 10:30 - 12:00																																										PLMW Session III 14:00 - 15:30																								PLMW Session IV 16:00 - 17:00												PLMW Session V 17:00 - 17:45

Wed 20 Jan 2016


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30						21:00						30						22:00						30
Dali Museum																																																																	Research Papers Banquet 19:00 - 22:00
Grand Bay Ballroom	Invited Speakers Invited Wed 09:00 - 10:00
Grand Bay North																			Research Papers Track 1: Algorithmic Verification 10:30 - 12:10																																														Research Papers Track 1: Decision Procedures 14:20 - 16:00																										Research Papers Track 1: Language Design 16:30 - 17:45
Grand Bay South																			Research Papers Track 2: Types and Foundations 10:30 - 12:10																																														Research Papers Track 2: Correct Compilation 14:20 - 16:00																										Research Papers Track 2: Decidability and complexity 16:30 - 17:45

Thu 21 Jan 2016


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30
Grand Bay Ballroom	Invited Speakers Invited Speaker Thu 09:00 - 10:00
Grand Bay North																			Research Papers Track 1: Foundations of distributed systems 10:30 - 12:10																																														Research Papers Track 1: Learning and verification 14:20 - 16:00																										Research Papers Track 1: Optimization 16:30 - 17:45																		Research Papers SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business Meeting 18:00 - 19:00
Grand Bay South																			Research Papers Track 2: Probabilistic and statistical analysis 10:30 - 12:10																																														Research Papers Track 2: Types, Generally or Gradually 14:20 - 16:00																										Research Papers Track 2: Sessions and processes 16:30 - 17:45
Lobby III																																																																	SRC POPL SRC Posters and Reception 19:00 - 20:00

Fri 22 Jan 2016


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30
Grand Bay Ballroom	Invited Speakers Invited Speaker Fri 09:00 - 10:00
Grand Bay North																			Research Papers Track 1: Program Design and Analysis 10:30 - 12:10																																														Research Papers Track 1: Synthesis 14:20 - 16:00
Grand Bay South																			Research Papers Track 2: Semantics and memory models 10:30 - 12:10																																														Research Papers Track 2: Foundations of Model Checking 14:20 - 15:35

Sat 23 Jan 2016


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Room St Petersburg I	Off the Beaten Track Session One 09:00 - 10:00																		Off the Beaten Track Session Two 10:30 - 12:10																																										Off the Beaten Track Session Three 14:00 - 15:35																								Off the Beaten Track Session Four 16:00 - 17:30
Room St Petersburg II	PPS 2016 Session 1 09:00 - 10:00																		PPS 2016 Session 2 10:30 - 12:15																																										PPS 2016 Session 3 14:00 - 15:30																		PPS 2016 Poster Session 15:30 - 16:30												PPS 2016 Session 5 16:30 - 18:00
Room St Petersburg III	CoqPL Session I 09:00 - 10:00																		CoqPL Session II 10:30 - 12:05																																										CoqPL Session III 14:00 - 15:25																								CoqPL Session IV 16:00 - 18:00

Sun 17 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Room St Petersburg I	VMCAI Automating Abstract Interpretation 09:00 - 10:00																		VMCAI An Abstract Domain of Uninterpreted Functions 10:30 - 11:00						VMCAI Predicate Abstraction for Linked Data Structures 11:00 - 11:30						VMCAI Property Directed Abstract Interpretation 11:30 - 12:00																														VMCAI Program Analysis with Local Policy Iteration 14:00 - 14:30						VMCAI Lazy Constrained Monotonic Abstraction 14:30 - 15:00						VMCAI Polyhedral Approximation of Multivariate Polynomials using Handelman’s ... 15:00 - 15:30												VMCAI D3 : Data-Driven Disjunctive Abstraction 16:00 - 16:30						VMCAI Exact Heap Summaries for Symbolic Execution 16:30 - 17:00

Mon 18 Jan 2016


Room	8:00			15			30			45			9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
Room Bayboro													PADL Program Synthesis for Direct Manipulation Interfaces 09:00 - 10:00																		PADL Simplifying Probabilistic Programs Using Computer Algebra 10:30 - 11:00						PADL Haskino: A Remote Monad for Programming the Arduino 11:00 - 11:30						PADL From Monads to Effects and Back 11:30 - 12:00																														PADL A GPU implementation of the ASP computation 14:00 - 14:30						PADL Using Constraint Logic Programming to Schedule Solar Array Operations o ... 14:30 - 15:00						PADL The Picat-SAT Compiler 15:00 - 15:30												PADL The KB paradigm and its application to interactive configuration 16:00 - 16:30						PADL Default Rules for Curry 16:30 - 17:00
Room Demens							PEPM 2016 Invited Talks Invited Talk: Learning from Big Code: Probabilistic Models, Program Ana ... 08:30 - 09:15									PEPM 2016 Invited Talks Invited Talk: Tracing JITs for Functional Languages 09:15 - 10:00															PEPM 2016 Invited Talks Invited Talk: Using Formal Methods to Eliminate Exploitable Bugs 10:30 - 11:15									PEPM 2016 Invited Talks Invited Talk: Automated Reasoning about Type Systems by Compilation to ... 11:15 - 12:00																																	PEPM 2016 Invited Talks Invited Talk: Program Synthesis: Opportunities for the next Decade 14:00 - 14:45									PEPM 2016 Invited Talks Invited Talk: LMS: a Perspective on Generative Programming 14:45 - 15:30															PEPM 2016 Invited Talks Invited Talk: Fiat: Extensible Code Generation with Proofs 16:00 - 16:45									PEPM 2016 Invited Talks Invited Talk: The Promise of Relational Programming 16:45 - 17:30
Room HTC 1							POPL 2016 Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines 08:30 - 10:00																								POPL 2016 Tutorials T2: Declare Your Language (Part 1): Hands-On Spoofax Tutorial 10:30 - 12:00																																										POPL 2016 Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines(Advance ... 14:00 - 15:30																								POPL 2016 Tutorials T2: Declare Your Language (Part 2): Name Binding with Scope Graphs 16:00 - 17:30
Room HTC 2							POPL 2016 Tutorials T3: Syntax-Guided Synthesis (SyGuS) 08:30 - 10:00																								POPL 2016 Tutorials T3: Syntax-Guided Synthesis (SyGuS) (Advanced Material) 10:30 - 12:00																																										POPL 2016 Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 14:00 - 15:30																								POPL 2016 Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 16:00 - 17:30
Room HTC 3							POPL 2016 Tutorials T5: Higher-Order Model Checking 08:30 - 10:00																								POPL 2016 Tutorials T4: Programs and Proofs in the Coq Proof Assistant 10:30 - 12:00																																										POPL 2016 Tutorials T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material) 14:00 - 15:30																								POPL 2016 Tutorials T5: Higher-Order Model Checking 16:00 - 17:30
Room HTC 4																															POPL 2016 Tutorials T6: Security and Privacy by Typing in Cryptographic Systems 10:30 - 12:00																																										POPL 2016 Tutorials T6: Security and Privacy by Typing in Cryptographic Systems 14:00 - 15:30
Room St Petersburg I													VMCAI Ironclad - Full Verification of Complex Systems 09:00 - 10:00																		VMCAI Abstract Interpretation with Infinitesimals 10:30 - 11:00						VMCAI Lipschitz Robustness of Timed I/O Systems 11:00 - 11:30						VMCAI A method for invariant generation for polynomial continuous systems 11:30 - 12:00																														VMCAI Hybrid Analysis for Partial Order Reduction of Programs with Arrays 14:00 - 14:30						VMCAI Cloud-Based Verification of Concurrent Software 14:30 - 15:00						VMCAI Abstraction-driven Concolic Testing 15:00 - 15:30												VMCAI Reward-Bounded Reachability Probability for Uncertain Weighted MDPs 16:00 - 16:30						VMCAI Parameter Synthesis for Parametric Interval Markov Chains 16:30 - 17:00
Room St Petersburg II													CPP 2016 Perspectives on Formal Verfication 09:00 - 10:00																		CPP 2016 Higher-order Representation Predicates in Separation Logic 10:30 - 11:00						CPP 2016 A Unified Coq Framework for Verifying C Programs with Floating-Point Co ... 11:00 - 11:30						CPP 2016 Refinement Based Verification of Imperative Data Structures 11:30 - 12:00																														CPP 2016 The Vampire and the FOOL 14:00 - 14:30						CPP 2016 Improving automation in interactive theorem provers by efficient encodi ... 14:30 - 15:00						CPP 2016 Mizar Environment for Isabelle 15:00 - 15:30												CPP 2016 A Modular, Efficient Formalisation of Real Algebraic Numbers 16:00 - 16:30						CPP 2016 Formal proofs of transcendence for e and pi as an application of multiv ... 16:30 - 17:00						CPP 2016 Formalizing Jordan Normal Forms in Isabelle/HOL 17:00 - 17:30						CPP 2016 Formalization of a Newton series representation of polynomials 17:30 - 18:00

Tue 19 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45			19:00			15			30			45			20:00			15			30			45			21:00			15			30			45
Room Bayboro																			PADL Computing with Catalan Families, Generically 10:30 - 11:00						PADL A Size-proportionate Bijective Encoding of Lambda Terms as Catalan Obje ... 11:00 - 11:30						PADL Generic Matching of Tree Regular Expressions over Haskell Data Types 11:30 - 12:00
Room Demens	PEPM 2016 Invited Talks Invited Keynote: Building Languages in Racket: Syntax Objects as an Int ... 09:00 - 10:00
Room Harbor View																			PEPM 2016 Practical, General Parser Combinators 10:30 - 11:00						PEPM 2016 Operator Precedence for Data-Dependent Grammars 11:00 - 11:30						PEPM 2016 Everything Old Is New Again: Quoted Domain-Specific Languages 11:30 - 12:00																														PEPM 2016 BiGUL: A Formally Verified Core Language for Putback-Based Bidirectiona ... 14:00 - 14:30						PEPM 2016 A Constraint Language for Static Semantic Analysis Based on Scope Graphs 14:30 - 15:00						PEPM 2016 Finally, Safely-Extensible and Efficient Language-Integrated Query 15:00 - 15:30												PEPM 2016 Staging Generic Programming 16:00 - 16:30						PEPM 2016 Removing Runtime Overhead for Optimized Object Queries 16:30 - 17:00						PEPM 2016 Toward Introducing Binding-Time Analysis to MetaOCaml 17:00 - 17:20				PEPM 2016 Staging beyond Terms: Prospects and Challenges 17:20 - 17:40
Room St Petersburg I	VMCAI Viper - A Verification Infrastructure for Permission-based Reasoning 09:00 - 10:00																		VMCAI Pointer Race Freedom 10:30 - 11:00						VMCAI A program logic for C11 memory fences 11:00 - 11:30						VMCAI From Low Level Pointers to High Level Containers 11:30 - 12:00																														VMCAI Regular Symmetry Patterns 14:00 - 14:30						VMCAI Tight Cutoffs for Guarded Protocols with Fairness 14:30 - 15:00						VMCAI A General Modular Synthesis Problem for Pushdown Systems 15:00 - 15:30												VMCAI Model Checking with Multi-Threaded IC3 Portfolios 16:00 - 16:30						VMCAI Automatic Generation of Propagation Complete SAT Encodings 16:30 - 17:00																		CPP 2016 CPP Reception, sponsored by the DeepSpec project 18:00 - 21:00
Room St Petersburg II	CPP 2016 Dependent Type Practice 09:00 - 10:00																		CPP 2016 A Logic of Proofs for Differential Dynamic Logic 10:30 - 11:00						CPP 2016 Constructing the Propositional Truncation using Non-recursive HITs 11:00 - 11:30						CPP 2016 A Nominal Exploration of Intuitionism 11:30 - 12:00																														CPP 2016 Bisimulation Up-to Techniques for Psi-calculi 14:00 - 14:30						CPP 2016 Planning for Change in a Formal Verification of the Raft Consensus Protocol 14:30 - 15:00						CPP 2016 A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules 15:00 - 15:30												CPP 2016 Formal Verification of Control-flow Graph Flattening 16:00 - 16:30						CPP 2016 Axiomatic Semantics for Compiler Verification 16:30 - 17:00
Room St Petersburg III	PLMW Grad School: A Survival Guide 09:00 - 09:30						PLMW Theorem Provers are a PL Researcher's Best Friend 09:30 - 10:00												PLMW Academia or Industry? 10:30 - 11:00						PLMW Refining Types with SMT 11:00 - 11:30						PLMW How to Write Papers So People Can Read Them 11:30 - 12:00																														PLMW Student Interaction Activity 14:00 - 14:30						PLMW Automata and Coinduction 14:30 - 15:00						PLMW Unaccustomed As I Am to Public Speaking 15:00 - 15:30												PLMW Two Notions of Beauty in Programming 16:00 - 16:30						PLMW Highs and Lows of a Language Researcher 16:30 - 17:00						PLMW Young Researcher Panel Session, with panelists: Mark Batty (Kent), Mike ... 17:00 - 17:45

Wed 20 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Grand Bay Ballroom	POPL 2016 Invited Speakers Programming the World of Uncertain Things 09:00 - 10:00
Grand Bay North																			POPL 2016 Research Papers Temporal Verification of Higher-order Functional Programs 10:30 - 10:55					POPL 2016 Research Papers Scaling Network Verification using Symmetry and Surgery 10:55 - 11:20					POPL 2016 Research Papers Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates 11:20 - 11:45					POPL 2016 Research Papers Reducing Crash Recoverability to Reachability 11:45 - 12:10																															POPL 2016 Research Papers Query-Guided Maximum Satisfiability 14:20 - 14:45					POPL 2016 Research Papers String Solving with Word Equations and Transducers: Decidability and Ap ... 14:45 - 15:10					POPL 2016 Research Papers Symbolic Computation of Differential Equivalences 15:10 - 15:35					POPL 2016 Research Papers Unboundedness and Downward Closures of Higher-Order Pushdown Automata 15:35 - 16:00											POPL 2016 Research Papers Dependent Types and Multi-Monadic Effects in F* 16:30 - 16:55					POPL 2016 Research Papers Fabular: Regression Formulas as Probabilistic Programming 16:55 - 17:20					POPL 2016 Research Papers Kleenex: Compiling Nondeterministic Transducers to Deterministic Stream ... 17:20 - 17:45
Grand Bay South																			POPL 2016 Research Papers Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega 10:30 - 10:55					POPL 2016 Research Papers Type Theory in Type Theory using Quotient Inductive Types 10:55 - 11:20					POPL 2016 Research Papers System Fω with Equirecursive Types for Datatype-generic Programming 11:20 - 11:45					POPL 2016 Research Papers A Theory of Effects and Resources: Adjunction Models and Polarised Calculi 11:45 - 12:10																															POPL 2016 Research Papers Fully-Abstract Compilation by Approximate Back-Translation 14:20 - 14:45					POPL 2016 Research Papers Lightweight Verification of Separate Compilation 14:45 - 15:10					POPL 2016 Research Papers From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes 15:10 - 15:35					POPL 2016 Research Papers Sound Type-dependent Syntactic Language Extension 15:35 - 16:00											POPL 2016 Research Papers Decidability of Inferring Inductive Invariants 16:30 - 16:55					POPL 2016 Research Papers The Hardness of Data Packing 16:55 - 17:20					POPL 2016 Research Papers The Complexity of Interaction 17:20 - 17:45

Thu 21 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
Grand Bay Ballroom	POPL 2016 Invited Speakers Synthesis of Reactive Controllers for Hybrid Systems 09:00 - 10:00
Grand Bay North																			POPL 2016 Research Papers Certified Causally Consistent Distributed Key-Value Stores 10:30 - 10:55					POPL 2016 Research Papers 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distri ... 10:55 - 11:20					POPL 2016 Research Papers A Program Logic for Concurrent Objects under Fair Scheduling 11:20 - 11:45					POPL 2016 Research Papers PSync: a partially synchronous language for fault-tolerant distributed ... 11:45 - 12:10																															POPL 2016 Research Papers Combining Static Analysis with Probabilistic Models to Enable Market-Sc ... 14:20 - 14:45					POPL 2016 Research Papers Abstraction Refinement Guided by a Learnt Probabilistic Model 14:45 - 15:10					POPL 2016 Research Papers Learning Invariants using Decision Trees and Implication Counterexamples 15:10 - 15:35					POPL 2016 Research Papers Symbolic Abstract Data Type Inference 15:35 - 16:00											POPL 2016 Research Papers SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Opti ... 16:30 - 16:55					POPL 2016 Research Papers PolyCheck: Dynamic Verification of Iteration Space Transformations on A ... 16:55 - 17:20					POPL 2016 Research Papers Printing Floating-Point Numbers: A Faster, Always Correct Method 17:20 - 17:45
Grand Bay South																			POPL 2016 Research Papers Prophet: Automatic Patch Generation via Learning from Successful Patches 10:30 - 10:55					POPL 2016 Research Papers Estimating types in binaries using predictive modeling 10:55 - 11:20					POPL 2016 Research Papers Algorithmic Analysis of Qualitative and Quantitative Termination Proble ... 11:20 - 11:45					POPL 2016 Research Papers Transforming Spreadsheet Data Types using Examples 11:45 - 12:10																															POPL 2016 Research Papers Principal Type Inference for GADTs 14:20 - 14:45					POPL 2016 Research Papers Abstracting Gradual Typing 14:45 - 15:10					POPL 2016 Research Papers The Gradualizer: a methodology and algorithm for generating gradual typ ... 15:10 - 15:35					POPL 2016 Research Papers Is Sound Gradual Typing Dead? 15:35 - 16:00											POPL 2016 Research Papers Effects as sessions, sessions as effects 16:30 - 16:55					POPL 2016 Research Papers Monitors and Blame Assignment for Higher-Order Session Types 16:55 - 17:20					POPL 2016 Research Papers Environmental Bisimulations for Probabilistic Higher-Order Languages 17:20 - 17:45

Fri 22 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45
Grand Bay Ballroom	POPL 2016 Invited Speakers Confluences in Programming Languages Research 09:00 - 10:00
Grand Bay North																			POPL 2016 Research Papers Newtonian Program Analysis via Tensor Product 10:30 - 10:55					POPL 2016 Research Papers Casper: An Efficient Approach to Call Trace Collection 10:55 - 11:20					POPL 2016 Research Papers Pushdown Control-flow Analysis for Free 11:20 - 11:45					POPL 2016 Research Papers Binding as Sets of Scopes 11:45 - 12:10																															POPL 2016 Research Papers Learning Programs from Noisy Data 14:20 - 14:45					POPL 2016 Research Papers Optimizing Synthesis with Metasketches 14:45 - 15:10					POPL 2016 Research Papers Maximal Specification Synthesis 15:10 - 15:35					POPL 2016 Research Papers Example-Directed Synthesis: A Type-Theoretic Interpretation 15:35 - 16:00
Grand Bay South																			POPL 2016 Research Papers Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA 10:30 - 10:55					POPL 2016 Research Papers A concurrency semantics for relaxed atomics that permits optimisation a ... 10:55 - 11:20					POPL 2016 Research Papers Overhauling SC atomics in C11 and OpenCL 11:20 - 11:45					POPL 2016 Research Papers Taming Release-Acquire Consistency 11:45 - 12:10																															POPL 2016 Research Papers Lattice-Theoretic Progress Measures and Coalgebraic Model Checking 14:20 - 14:45					POPL 2016 Research Papers Algorithms for Algebraic Path Properties in Concurrent Systems of Const ... 14:45 - 15:10					POPL 2016 Research Papers Memoryful Geometry of Interaction II: Recursion and Adequacy 15:10 - 15:35

Sat 23 Jan 2016


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
Room St Petersburg I	Off the Beaten Track 2016 Opening remarks and program chair's report 09:00 - 09:15			Off the Beaten Track 2016 Keynote Talk: Operationalizing Creative Theories 09:15 - 10:00															Off the Beaten Track 2016 Chanakya: Computer-Aided Strategic Reasoning 10:30 - 10:55					Off the Beaten Track 2016 Programming Interactivity Requires Both Semantics and Semiotics 10:55 - 11:20