Program - POPL 2016

Agostino DovierUniversity of Udine, Andrea FormisanoUniversità di Perugia , Enrico PontelliNew Mexico State University, Flavio VellaSapienza University of Rome, Italy

14:30 - 15:00
Talk

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

Jan JelínekCharles University in Prague, Roman BartákCharles University in Prague

15:00 - 15:30
Talk

The Picat-SAT Compiler

Neng-Fa ZhouCUNY Brooklyn College and Graduate Center, Håkan KjellerstrandCUNY Brooklyn College and Graduate Center

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

14:00 - 14:30
Talk

Hybrid Analysis for Partial Order Reduction of Programs with Arrays

Pavel ParizekCharles University in Prague

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. HenzingerIST Austria

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 BodikUniversity of Washington, USA

14:45 - 15:30
Talk

Invited Talk: LMS: a Perspective on Generative Programming

Nada AminEPFL

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 KotelnikovChalmers University of Technology, Laura KovacsChalmers University of Technology, Giles RegerUniversity of Manchester, Andrei VoronkovUniversity of Manchester

14:30 - 15:00
Talk

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

Lukasz CzajkaUniversity of Innsbruck

15:00 - 15:30
Talk

Mizar Environment for Isabelle

Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity of Bialystok, Institute of Computer Science, 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)

David Van HornUniversity of Maryland, College Park

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 RandUniversity of Pennsylvania, Arthur Azevedo de AmorimUniversity of Pennsylvania

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 RadhakrishnaMicrosoft, Roopsha SamantaIST Austria

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

Adam ChlipalaMIT

16:45 - 17:30
Talk

Invited Talk: The Promise of Relational Programming

William E. ByrdUniversity of Utah

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 HertumKU Leuven, Ingmar DassevilleKU Leuven, Gerda JanssensKU Leuven, Marc DeneckerKU Leuven

16:30 - 17:00
Talk

Default Rules for Curry

Sergio AntoyKiel University, Michael HanusKiel University

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 LiUniversity of Cambridge, Lawrence PaulsonCambridge University

16:30 - 17:00
Talk

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

Sophie BernardINRIA, Yves BertotINRIA, Laurence RideauINRIA, Pierre-Yves StrubIMDEA Software Institute

17:00 - 17:30
Talk

Formalizing Jordan Normal Forms in Isabelle/HOL

René ThiemannUniversity of Innsbruck, Akihisa Yamada

17:30 - 18:00
Talk

Formalization of a Newton series representation of polynomials

Cyril Cohen, Boris DjalalINRIA

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

Eelco VisserDelft University of Technology

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 KobayashiUniversity of Tokyo, C.-H. Luke OngUniversity of Oxford, UK

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 RadhakrishnaMicrosoft, Roopsha SamantaIST Austria

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 ChangUniversity of Colorado Boulder

09:00 - 10:00
Talk

Viper - A Verification Infrastructure for Permission-based Reasoning

Peter MüllerETH Zurich

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

Matthew FlattUniversity of Utah

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 MouraMicrosoft Research, Redmond

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

09:00 - 09:30
Talk

Grad School: A Survival Guide

Matthew MightUniversity of Utah, USA

Media Attached

09:30 - 10:00
Talk

Theorem Provers are a PL Researcher's Best Friend

Xavier LeroyInria

Media Attached

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 WolffFraunhofer ITWM and TU Kaiserslautern

11:00 - 11:30
Talk

A program logic for C11 memory fences

Marko DokoMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany

11:30 - 12:00
Talk

From Low Level Pointers to High Level Containers

Kamil Dudka, Lukas Holik, Petr Peringer, Tomas VojnarBrno University of Technology

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

10:30 - 11:00
Talk

Computing with Catalan Families, Generically

Paul TarauUniversity of North Texas

11:00 - 11:30
Talk

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

Paul TarauUniversity of North Texas

11:30 - 12:00
Talk

Generic Matching of Tree Regular Expressions over Haskell Data Types

Alejandro SerranoUtrecht University, Jurriaan HageUtrecht University

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

10:30 - 11:00
Talk

Practical, General Parser Combinators

Anastasia IzmaylovaCentrum Wiskunde & Informatica, Ali AfroozehCentrum Wiskunde & Informatica, Tijs van der StormCWI

DOI Pre-print

11:00 - 11:30
Talk

Operator Precedence for Data-Dependent Grammars

Ali AfroozehCentrum Wiskunde & Informatica, Anastasia IzmaylovaCentrum Wiskunde & Informatica

DOI Pre-print

11:30 - 12:00
Talk

Everything Old Is New Again: Quoted Domain-Specific Languages

Shayan Najd, Sam LindleyUniversity of Edinburgh, Josef SvenningssonChalmers University of Technology, Sweden, Philip WadlerUniversity of Edinburgh

DOI

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 FultonCarnegie Mellon University, André Platzer

11:00 - 11:30
Talk

Constructing the Propositional Truncation using Non-recursive HITs

Floris van DoornCarnegie Mellon University

11:30 - 12:00
Talk

A Nominal Exploration of Intuitionism

Vincent RahliSnT, Mark BickfordCornell University

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

10:30 - 11:00
Talk

Academia or Industry?

Aarti GuptaPrinceton University

Media Attached

11:00 - 11:30
Talk

Refining Types with SMT

Ranjit JhalaUniversity of California, San Diego

Media Attached

11:30 - 12:00
Talk

How to Write Papers So People Can Read Them

Derek DreyerMPI-SWS

Media Attached

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

14:00 - 14:30
Talk

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

Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Tao ZanSokendai, Japan, Zhenjiang HuNational Institute of Informatics

DOI Pre-print

14:30 - 15:00
Talk

A Constraint Language for Static Semantic Analysis Based on Scope Graphs

Hendrik van AntwerpenDelft University of Technology, Netherlands, Pierre NeronTU Delft, Andrew TolmachPortland State University, Eelco VisserDelft University of Technology, Guido WachsmuthDelft University of Technology

Link to publication DOI Pre-print

15:00 - 15:30
Talk

Finally, Safely-Extensible and Efficient Language-Integrated Query

Kenichi SuzukiUniversity of Tsukuba, Japan, Oleg Kiselyov, Yukiyoshi Kameyama

DOI

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

14:00 - 14:30
Talk

Regular Symmetry Patterns

Anthony Widjaja LinYale-NUS College, Singapore, Truong Khanh Nguyen, Philipp RuemmerUppsala University, 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 Å. PohjolaUppsala University, Joachim ParrowUppsala University

14:30 - 15:00
Talk

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

Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of Washington

Pre-print

15:00 - 15:30
Talk

A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules

Michel St-MartinUniversity of Ottawa, Amy FeltyUniversity of Ottawa

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

14:00 - 14:30
Talk

Student Interaction Activity

Isil DilligUniversity of Texas, Austin, Ross TateCornell University

14:30 - 15:00
Talk

Automata and Coinduction

Alexandra SilvaRadboud University Nijmegen

Media Attached

15:00 - 15:30
Talk

Unaccustomed As I Am to Public Speaking

John HughesChalmers University of Technology

Media Attached

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 BlazyIRISA / University of Rennes 1, Alix TrieuENS Rennes

16:30 - 17:00
Talk

Axiomatic Semantics for Compiler Verification

Steven Schäfer, Sigurd SchneiderSaarland University, Gert SmolkaSaarland University

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

16:00 - 16:30
Talk

Two Notions of Beauty in Programming

Robert HarperCarnegie Mellon University

Media Attached

16:30 - 17:00
Talk

Highs and Lows of a Language Researcher

Greg MorrisettCornell University

Media Attached

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

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 KroeningUniversity of Oxford, Ruben Martins

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

16:00 - 16:30
Talk

Staging Generic Programming

Jeremy YallopUniversity of Cambridge, UK

DOI

16:30 - 17:00
Talk

Removing Runtime Overhead for Optimized Object Queries

Jon Brandvein, Yanhong A. LiuStony Brook University, USA

DOI

17:00 - 17:20
Talk

Toward Introducing Binding-Time Analysis to MetaOCaml

Kenichi AsaiOchanomizu University

DOI

17:20 - 17:40
Talk

Staging beyond Terms: Prospects and Challenges

Jun InoueNational Institute of Advanced Industrial Science and Technology, Japan, Oleg Kiselyov, Yukiyoshi Kameyama

DOI

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 VytiniotisMicrosoft Research, Cambridge

Media Attached

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 BodikUniversity of Washington, USA

09:00 - 10:00
Talk

Programming the World of Uncertain Things

Kathryn S McKinleyMicrosoft Research

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

10:30 - 10:55
Talk

Temporal Verification of Higher-order Functional Programs

Akihiro Murase, Tachio TerauchiJAIST, Naoki KobayashiUniversity of Tokyo, Ryosuke SatoUniversity of Tokyo, Hiroshi UnnoUniversity of Tsukuba

10:55 - 11:20
Talk

Scaling Network Verification using Symmetry and Surgery

Gordon Plotkin, Nikolaj BjørnerMicrosoft Research, Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research, George VargheseMicrosoft Research

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 KoskinenYale University, Junfeng YangColumbia University

10:30 - 12:10: Research Papers - Track 2: Types and Foundations at Grand Bay South
Chair(s): Robert AtkeyUniversity of Strathclyde

10:30 - 10:55
Talk

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

Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles

Media Attached File Attached

10:55 - 11:20
Talk

Type Theory in Type Theory using Quotient Inductive Types

Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham

Media Attached File Attached

11:20 - 11:45
Talk

System Fω with Equirecursive Types for Datatype-generic Programming

Yufei CaiUniversity of Tübingen, Germany, Paolo G. GiarrussoUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany

Media Attached

11:45 - 12:10
Talk

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

Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo FioreComputer Laboratory, University of Cambridge, Guillaume Munch-MaccagnoniComputer Laboratory, University of Cambridge

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

14:20 - 14:45
Talk

Query-Guided Maximum Satisfiability

Xin ZhangGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Aditya NoriMicrosoft Research, UK, Mayur NaikGeorgia Tech

File Attached

14:45 - 15:10
Talk

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

Anthony Widjaja LinYale-NUS College, Singapore, Pablo BarceloUniversity of Chile, Chile

Media Attached

15:10 - 15:35
Talk

Symbolic Computation of Differential Equivalences

Luca CardelliMicrosoft Research and University of Oxford, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinIMT Institute for Advanced Studies Lucca, Italy

Media Attached

15:35 - 16:00
Talk

Unboundedness and Downward Closures of Higher-Order Pushdown Automata

Matthew HagueRoyal Holloway University of London, UK, Jonathan KochemsDepartment of Computer Science, University of Oxford, C.-H. Luke OngUniversity of Oxford, UK

Media Attached

14:20 - 16:00: Research Papers - Track 2: Correct Compilation at Grand Bay South
Chair(s): Jens PalsbergUniversity of California, Los Angeles

14:20 - 14:45
Talk

Fully-Abstract Compilation by Approximate Back-Translation

Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven

Pre-print Media Attached

14:45 - 15:10
Talk

Lightweight Verification of Separate Compilation

Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany

Media Attached File Attached

15:10 - 15:35
Talk

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

Ed RobbinsKent, Andy KingKent, Tom SchrijversKU Leuven

Media Attached

15:35 - 16:00
Talk

Sound Type-dependent Syntactic Language Extension

Florian LorenzenTU Berlin, Sebastian ErdwegTU Darmstadt, Germany

Pre-print Media Attached File Attached

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

16:30 - 16:55
Talk

Dependent Types and Multi-Monadic Effects in F*

Nikhil SwamyMicrosoft Research, Cătălin HriţcuINRIA Paris, Chantal KellerMSR-INRIA, Aseem RastogiUniversity of Maryland, College Park, Antoine Delignat-LavaudINRIA, Simon ForestENS, Karthikeyan BhargavanINRIA, Cédric FournetMicrosoft Research, Pierre-Yves StrubIMDEA Software Institute, Markulf KohlweissMicrosoft Research, Jean-Karim ZinzindohouéINRIA, Santiago Zanella-BéguelinMicrosoft Research

Pre-print Media Attached

16:55 - 17:20
Talk

Fabular: Regression Formulas as Probabilistic Programming

Johannes BorgströmUppsala University, Andrew D. GordonMicrosoft Research and University of Edinburgh, Long OuyangStanford University, Claudio RussoMicrosoft Research, Adam ŚcibiorUniversity of Cambridge, Marcin SzymczakUniversity of Edinburgh

Media Attached

17:20 - 17:45
Talk

Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers

Bjørn Bugge GrathwohlDIKU, University of Copenhagen, Fritz HengleinDIKU, Denmark, Ulrik Terp RasmussenDIKU, University of Copenhagen, Kristoffer Aalund SøholmJobindex, Denmark, Sebastian Paaske TørholmJobindex, Denmark

Media Attached

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

16:30 - 16:55
Talk

Decidability of Inferring Inductive Invariants

Oded PadonTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Sharon Shoham, Aleksandr KarbyshevTel Aviv University, Mooly SagivTel Aviv University

Media Attached

16:55 - 17:20
Talk

The Hardness of Data Packing

Rahman Lavaee, Chen DingUniversity of Rochester

Media Attached

17:20 - 17:45
Talk

The Complexity of Interaction

Stéphane GimenezUniversity of Innsbruck, Georg MoserUniversity of Innsbruck

Media Attached

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 MajumdarMPI-SWS

09:00 - 10:00
Talk

Synthesis of Reactive Controllers for Hybrid Systems

Richard M. MurrayCalifornia Institute of Technology

Media Attached

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

10:30 - 10:55
Talk

Certified Causally Consistent Distributed Key-Value Stores

Mohsen LesaniMIT, Christian J. BellMIT CSAIL, Adam ChlipalaMIT

Media Attached

10:55 - 11:20
Talk

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

Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6

Media Attached

11:20 - 11:45
Talk

A Program Logic for Concurrent Objects under Fair Scheduling

Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China

Media Attached

11:45 - 12:10
Talk

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

Cezara DrăgoiINRIA, ENS, CNRS, Thomas A. HenzingerIST Austria, Damien ZuffereyMIT

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 NoriMicrosoft Research, UK

10:30 - 10:55
Talk

Prophet: Automatic Patch Generation via Learning from Successful Patches

Fan LongMIT CSAIL, Martin RinardMassachusetts Institute of Technology, USA

Media Attached

10:55 - 11:20
Talk

Estimating types in binaries using predictive modeling

Omer KatzTechnion, Israel Institute of Technology, Ran El-YanivTechnion, Israel Institute of Technology, Eran YahavTechnion

Media Attached File Attached

11:20 - 11:45
Talk

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

Krishnendu ChatterjeeIST Austria, Hongfei FuIST Austria, Rouzbeh HasheminezhadSharif University, Petr NovotnyIST Austria

Media Attached

11:45 - 12:10
Talk

Transforming Spreadsheet Data Types using Examples

Rishabh SinghMicrosoft Research, Sumit GulwaniMicrosoft Research

Media Attached

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

14:20 - 14:45
Talk

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

Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg

Media Attached

14:45 - 15:10
Talk

Abstraction Refinement Guided by a Learnt Probabilistic Model

Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK

Media Attached

15:10 - 15:35
Talk

Learning Invariants using Decision Trees and Implication Counterexamples

Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity of Illinois at Urbana-Champaign

Media Attached

15:35 - 16:00
Talk

Symbolic Abstract Data Type Inference

Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot

Media Attached

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

14:20 - 14:45
Talk

Principal Type Inference for GADTs

Sheng ChenUniversity of louisiana at Lafayette, Martin ErwigOregon State University

Media Attached

14:45 - 15:10
Talk

Abstracting Gradual Typing

Ronald GarciaUniversity of British Columbia, Alison M. Clark, Éric TanterUniversity of Chile, Chile

Link to publication Media Attached

15:10 - 15:35
Talk

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

Matteo CiminiIndiana University, Jeremy G. SiekIndiana University

Media Attached

15:35 - 16:00
Talk

Is Sound Gradual Typing Dead?

Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern University

Pre-print Media Attached File Attached

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

16:30 - 16:55
Talk

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

Somashekaracharya G BhaskaracharyaIndian Institute of Science and National Instruments, Uday BondhugulaIndian Institute of Science, Albert CohenINRIA

Media Attached File Attached

16:55 - 17:20
Talk

PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs

Wenlei Bao, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noel PouchetOhio State University, Fabrice RastelloINRIA, France, P. SadayappanOhio State University

Media Attached

17:20 - 17:45
Talk

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

Marc AndryscoUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego

Media Attached

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

16:30 - 16:55
Talk

Effects as sessions, sessions as effects

Dominic OrchardImperial College London, Nobuko YoshidaImperial College London, UK

Pre-print Media Attached

16:55 - 17:20
Talk

Monitors and Blame Assignment for Higher-Order Session Types

Limin JiaCarnegie Mellon University, Hannah GommerstadtCarnegie Mellon University, Frank PfenningCarnegie Mellon University

Media Attached File Attached

17:20 - 17:45
Talk

Environmental Bisimulations for Probabilistic Higher-Order Languages

Davide SangiorgiUniversity of Bologna, Valeria VignudelliUniversity of Bologna/INRIA

Media Attached

18:00 - 19:00: Research Papers - SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business Meeting at Grand Bay North
Chair(s): Michael HicksUniversity of Maryland at College Park, USA

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

Fri 22 Jan

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

09:00 - 10:00
Talk

Confluences in Programming Languages Research

David WalkerPrinceton University

Media Attached

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

10:30 - 10:55
Talk

Newtonian Program Analysis via Tensor Product

Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogle

Media Attached

10:55 - 11:20
Talk

Casper: An Efficient Approach to Call Trace Collection

Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao XiaoThe Hong Kong University of Science and Technology, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu ZhangMicrosoft Research, Charles ZhangHKUST

Media Attached

11:20 - 11:45
Talk

Pushdown Control-flow Analysis for Free

Thomas GilrayUniversity of Utah, Steven Lyde, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland, College Park

Pre-print Media Attached

11:45 - 12:10
Talk

Binding as Sets of Scopes

Matthew FlattUniversity of Utah

Pre-print Media Attached

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

10:30 - 10:55
Talk

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA

Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity of Cambridge

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-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge

File Attached

11:20 - 11:45
Talk

Overhauling SC atomics in C11 and OpenCL

John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London

Pre-print File Attached

11:45 - 12:10
Talk

Taming Release-Acquire Consistency

Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany

Pre-print Media Attached File Attached

14:20 - 16:00: Research Papers - Track 1: Synthesis at Grand Bay North
Chair(s): Roberto GiacobazziUniversity of Verona, Italy

14:20 - 14:45
Talk

Learning Programs from Noisy Data

Veselin RaychevETH Zurich, Pavol BielikETH Zurich, Switzerland, Martin VechevETH Zurich, Andreas KrauseETH Zurich

Link to publication DOI Pre-print Media Attached File Attached

14:45 - 15:10
Talk

Optimizing Synthesis with Metasketches

James BornholtUniversity of Washington, Emina TorlakUniversity of Washington, Dan GrossmanUniversity of Washington, USA, Luis CezeUniversity of Washington, USA

Pre-print Media Attached

15:10 - 15:35
Talk

Maximal Specification Synthesis

Aws AlbarghouthiUniversity of Wisconsin–Madison, Isil DilligUniversity of Texas, Austin, Arie GurfinkelCarnegie Mellon University

Pre-print Media Attached

15:35 - 16:00
Talk

Example-Directed Synthesis: A Type-Theoretic Interpretation

Jonathan FranklePrinceton University, Peter-Michael OseraGrinnell College, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania

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 SilvaRadboud University Nijmegen

14:20 - 14:45
Talk

Lattice-Theoretic Progress Measures and Coalgebraic Model Checking

Ichiro HasuoUniversity of Tokyo, Shunsuke ShimizuUniversity of Tokyo, Corina CirsteaUniversity of Southampton

Media Attached

14:45 - 15:10
Talk

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

Krishnendu ChatterjeeIST Austria, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis

Media Attached

15:10 - 15:35
Talk

Memoryful Geometry of Interaction II: Recursion and Adequacy

Koko MuroyaUniversity of Tokyo, Naohiko HoshinoKyoto University, Ichiro HasuoUniversity of Tokyo

Media Attached

Sat 23 Jan

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

09:00 - 09:20
Talk

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

Norman Ramsey

Pre-print

09:20 - 09:30
Meeting

Discussion 1

09:30 - 09:50
Talk

An Interface for Black Box Learning in Probabilistic Programs

Jan-Willem van de MeentUniversity of Oxford, Brooks PaigeUniversity of Oxford, David TolpinUniversity of Oxford, Frank WoodUniversity of Oxford

Pre-print

09:50 - 10:00
Meeting

Discussion 2

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 SozeauInria

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

09:00 - 09:15
Day opening

Opening remarks and program chair's report

Lindsey KuperIntel Labs

09:15 - 10:00
Talk

Keynote Talk: Operationalizing Creative Theories

Chris MartensCarnegie Mellon University

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

10:30 - 10:50
Talk

Models for Probabilistic Programs with an Adversary

Robert RandUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania

Pre-print

10:50 - 11:00
Meeting

DIscussion 3

11:00 - 11:20
Talk

The Semantics of Figaro, an Embedded Probabilistic Programming Language

Avi PfefferCharles River Analytics, Brian RuttenbergCharles River Analytics

Pre-print

11:20 - 11:30
Meeting

Discussion 4

11:30 - 12:15
Meeting

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

Angelika KimmigKU Leuven, Oleg Kiselyov, Jan-Willem van de MeentUniversity of Oxford, Avi PfefferCharles River Analytics, Frank WoodUniversity of Oxford

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. BellMIT CSAIL

Link to publication

11:20 - 11:45
Talk

Formalizing Simple Refinements in Coq

Nicolás Lehmann, Éric TanterUniversity of Chile, Chile

Link to publication

11:45 - 12:05
Talk

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

Clément Pit-ClaudelMIT CSAIL, Pierre Courtieu

Link to publication

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

10:30 - 10:55
Talk

Chanakya: Computer-Aided Strategic Reasoning

Suguman BansalRice University, USA, Swarat ChaudhuriRice University

Pre-print

10:55 - 11:20
Talk

Programming Interactivity Requires Both Semantics and Semiotics

Joseph Osborn, Michael Mateas

Pre-print

11:20 - 11:45
Talk

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

Kyle Headley, Matthew HammerUniversity of Colorado, Boulder

Pre-print

11:45 - 12:10
Talk

Challenges Facing a High-Level Language for Machine Knitting

Lea Albaugh, James McCann

Pre-print

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

14:00 - 14:20
Talk

A Lambda-Calculus Foundation for Universal Probabilistic Programming

Johannes BorgströmUppsala University, Ugo Dal LagoUniversity of Bologna, Andrew D. GordonMicrosoft Research and University of Edinburgh, Marcin SzymczakUniversity of Edinburgh

Pre-print

14:20 - 14:30
Meeting

Discussion 5

14:30 - 14:50
Talk

Making our Own Luck: A Language for Random Generators

Leonidas LampropoulosUniversity of Pennsylvania, Benjamin C. PierceUniversity of Pennsylvania, Cătălin HriţcuINRIA Paris, John HughesChalmers University of Technology, Zoe ParaskevopoulouPrinceton University, Li-yao XiaENS Paris

Pre-print

14:50 - 15:00
Meeting

Discussion 6

15:00 - 15:20
Talk

Semantics of Higher-order Probabilistic Programs

Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, UK, Chris HeunenUniversity of Edinburgh, Ohad KammarUniversity of Cambridge, Frank WoodUniversity of Oxford

Pre-print

15:20 - 15:30
Meeting

Discussion 7

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

Chung-Kil HurSeoul National University

15:00 - 15:25
Talk

Certified Desugaring of Javascript Programs using Coq

Marek MaterzokUniversity of Wroclaw

Link to publication

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

14:00 - 14:45
Talk

Keynote Talk: Generalising Abstraction

Robert AtkeyUniversity of Strathclyde

14:45 - 15:10
Talk

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

Neelakantan R. Krishnaswami

Pre-print

15:10 - 15:35
Talk

Affine Functional Programs as Higher-order Boolean Circuits

Damiano Mazza

Pre-print

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 KligerXamarin, Inc., Sean StromstenBAE Systems, Inc.

Pre-print

15:30 - 16:30
Meeting

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

Theophilos GiannakopoulosBAE Systems, Inc., Mitchell WandNortheastern University, Andrew CobbNortheastern University

Pre-print

15:30 - 16:30
Meeting

Coalgebraic Trace Semantics for Probabilistic Processes: Preliminary Proposal

Larry MossIndiana University, Chung-chieh ShanIndiana University, Alexandra SilvaRadboud University Nijmegen

Pre-print

15:30 - 16:30
Meeting

Reasoning about Probability and Nondeterminism

Faris Abou-SalehUniversity of Oxford, Kwok-Ho CheungUniversity of Oxford, Jeremy GibbonsUniversity of Oxford, UK

Pre-print

15:30 - 16:30
Meeting

Fixed Points for Markov Decision Processes

Johannes HölzlTechnische Universität München

Pre-print

15:30 - 16:30
Meeting

A Denotational Semantics of a Probabilistic Stream-Processing Language

Yohei MiyamotoGraduate School of Informatics, Kyoto University, Kohei Suenaga, Koji NakazawaGraduate School of Information Science, Nagoya University

Pre-print

15:30 - 16:30
Meeting

Observation Propagation for Importance Sampling with Likelihood Weighting

Ryan CulpepperNortheastern University

Pre-print

15:30 - 16:30
Meeting

Problems of the Lightweight Implementation of Probabilistic Programming

Oleg Kiselyov

Pre-print

15:30 - 16:30
Meeting

Parameterized Probability Monad

Adam ŚcibiorUniversity of Cambridge, Andrew D. GordonMicrosoft Research and University of Edinburgh

Pre-print

15:30 - 16:30
Meeting

Reproducing Kernel Hilbert Space Semantics for Probabilistic Programs

Adam ŚcibiorUniversity of Cambridge, Bernhard SchölkopfMPI Tuebingen

Pre-print

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

16:00 - 16:25
Talk

Declarative, Secure, Convergent Edge Computation

Christopher Meiklejohn

Pre-print

16:25 - 16:50
Talk

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

Randolph Langley

Pre-print

16:50 - 17:15
Talk

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

William E. ByrdUniversity of Utah

Pre-print

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 JacobsiMinds - Distrinet, KU Leuven

Link to publication

16:25 - 16:50
Talk

A Case for Tactics with (Limited) Side Effects

Benjamin Delaware

Pre-print

16:50 - 17:15
Talk

Formal Verification of Stability Properties of Cyber-Physical Systems

Matthew Chan, Daniel RickettsUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego, Gregory MalechaUCSD

Link to publication

17:15 - 17:45
Talk

The Science of Deep Specification

Andrew AppelPrinceton

17:45 - 18:00
Talk

Discussion

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

16:30 - 16:50
Talk

eXchangeable Random Primitives

Nathanael L. AckermanHarvard University, Cameron FreerGamalon, Daniel RoyUniversity of Toronto

Pre-print

16:50 - 17:00
Meeting

Discussion 8

17:00 - 17:20
Talk

An Application of Computable Distributions to the Semantics of Probabilistic Programs

Daniel HuangHarvard University, Greg MorrisettCornell University

Pre-print

17:20 - 17:30
Meeting

Discussion 9

17:30 - 17:50
Talk

On The Semantic Intricacies of Conditioning

Friedrich GretzRWTH Aachen University, Nils JansenRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University, Federico OlmedoRWTH Aachen University

Pre-print

17:50 - 18:00
Meeting

Discussion 10

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		PEPM Invited Talks Invited talks 0 & 1 08:30 - 10:00					PEPM Invited Talks Invited talks 2 & 3 10:30 - 12:00							PEPM Invited Talks Invited talks 4 & 5 14:00 - 15:30				PEPM Invited Talks Invited talks 6 & 7 16:00 - 17:30
Room HTC 1		POPL Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines 08:30 - 10:00					POPL Tutorials T2: Declare Your Language: Part 1 10:30 - 12:00							POPL Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines 14:00 - 15:30				POPL Tutorials T2: Declare Your Language: Part 2 16:00 - 17:30
Room HTC 2		POPL Tutorials T3: Syntax-Guided Synthesis (SyGuS) 08:30 - 10:00					POPL Tutorials T3: Syntax-Guided Synthesis (SyGuS) 10:30 - 12:00							POPL Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 14:00 - 15:30				POPL Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 16:00 - 17:30
Room HTC 3		POPL Tutorials T5: Higher-Order Model Checking 08:30 - 10:00					POPL Tutorials T4: Programs and Proofs in the Coq Proof Assistant 10:30 - 12:00							POPL Tutorials T4: Programs and Proofs in the Coq Proof Assistant 14:00 - 15:30				POPL Tutorials T5: Higher-Order Model Checking 16:00 - 17:30
Room HTC 4							POPL Tutorials T6: Security and Privacy by Typing in Cryptographic Systems 10:30 - 12:00							POPL 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				PEPM 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												POPL Research Papers Banquet 19:00 - 22:00
Grand Bay Ballroom	POPL Invited Speakers Invited Wed 09:00 - 10:00
Grand Bay North				POPL Research Papers Track 1: Algorithmic Verification 10:30 - 12:10								POPL Research Papers Track 1: Decision Procedures 14:20 - 16:00					POPL Research Papers Track 1: Language Design 16:30 - 17:45
Grand Bay South				POPL Research Papers Track 2: Types and Foundations 10:30 - 12:10								POPL Research Papers Track 2: Correct Compilation 14:20 - 16:00					POPL 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	POPL Invited Speakers Invited Speaker Thu 09:00 - 10:00
Grand Bay North				POPL Research Papers Track 1: Foundations of distributed systems 10:30 - 12:10								POPL Research Papers Track 1: Learning and verification 14:20 - 16:00					POPL Research Papers Track 1: Optimization 16:30 - 17:45			POPL Research Papers SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business Meeting 18:00 - 19:00
Grand Bay South				POPL Research Papers Track 2: Probabilistic and statistical analysis 10:30 - 12:10								POPL Research Papers Track 2: Types, Generally or Gradually 14:20 - 16:00					POPL Research Papers Track 2: Sessions and processes 16:30 - 17:45
Lobby III												POPL 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	POPL Invited Speakers Invited Speaker Fri 09:00 - 10:00
Grand Bay North				POPL Research Papers Track 1: Program Design and Analysis 10:30 - 12:10								POPL Research Papers Track 1: Synthesis 14:20 - 16:00
Grand Bay South				POPL Research Papers Track 2: Semantics and memory models 10:30 - 12:10								POPL 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 Session 1 09:00 - 10:00			PPS Session 2 10:30 - 12:15							PPS Session 3 14:00 - 15:30			PPS Poster Session 15:30 - 16:30		PPS 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 Invited Talks Invited Talk: Learning from Big Code: Probabilistic Models, Program Ana ... 08:30 - 09:15			PEPM Invited Talks Invited Talk: Tracing JITs for Functional Languages 09:15 - 10:00					PEPM Invited Talks Invited Talk: Using Formal Methods to Eliminate Exploitable Bugs 10:30 - 11:15			PEPM Invited Talks Invited Talk: Automated Reasoning about Type Systems by Compilation to ... 11:15 - 12:00											PEPM Invited Talks Invited Talk: Program Synthesis: Opportunities for the next Decade 14:00 - 14:45			PEPM Invited Talks Invited Talk: LMS: a Perspective on Generative Programming 14:45 - 15:30					PEPM Invited Talks Invited Talk: Fiat: Extensible Code Generation with Proofs 16:00 - 16:45			PEPM Invited Talks Invited Talk: The Promise of Relational Programming 16:45 - 17:30
Room HTC 1			POPL Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines 08:30 - 10:00								POPL Tutorials T2: Declare Your Language (Part 1): Hands-On Spoofax Tutorial 10:30 - 12:00														POPL Tutorials T1: An Introduction to Redex with Abstracting Abstract Machines(Advance ... 14:00 - 15:30								POPL Tutorials T2: Declare Your Language (Part 2): Name Binding with Scope Graphs 16:00 - 17:30
Room HTC 2			POPL Tutorials T3: Syntax-Guided Synthesis (SyGuS) 08:30 - 10:00								POPL Tutorials T3: Syntax-Guided Synthesis (SyGuS) (Advanced Material) 10:30 - 12:00														POPL Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 14:00 - 15:30								POPL Tutorials T7: Trace-based Synchronization Synthesis for Concurrent Programs 16:00 - 17:30
Room HTC 3			POPL Tutorials T5: Higher-Order Model Checking 08:30 - 10:00								POPL Tutorials T4: Programs and Proofs in the Coq Proof Assistant 10:30 - 12:00														POPL Tutorials T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material) 14:00 - 15:30								POPL Tutorials T5: Higher-Order Model Checking 16:00 - 17:30
Room HTC 4											POPL Tutorials T6: Security and Privacy by Typing in Cryptographic Systems 10:30 - 12:00														POPL 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 Perspectives on Formal Verfication 09:00 - 10:00						CPP Higher-order Representation Predicates in Separation Logic 10:30 - 11:00		CPP A Unified Coq Framework for Verifying C Programs with Floating-Point Co ... 11:00 - 11:30		CPP Refinement Based Verification of Imperative Data Structures 11:30 - 12:00										CPP The Vampire and the FOOL 14:00 - 14:30		CPP Improving automation in interactive theorem provers by efficient encodi ... 14:30 - 15:00		CPP Mizar Environment for Isabelle 15:00 - 15:30				CPP A Modular, Efficient Formalisation of Real Algebraic Numbers 16:00 - 16:30		CPP Formal proofs of transcendence for e and pi as an application of multiv ... 16:30 - 17:00		CPP Formalizing Jordan Normal Forms in Isabelle/HOL 17:00 - 17:30		CPP 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 Invited Talks Invited Keynote: Building Languages in Racket: Syntax Objects as an Int ... 09:00 - 10:00
Room Harbor View							PEPM Practical, General Parser Combinators 10:30 - 11:00		PEPM Operator Precedence for Data-Dependent Grammars 11:00 - 11:30		PEPM Everything Old Is New Again: Quoted Domain-Specific Languages 11:30 - 12:00										PEPM BiGUL: A Formally Verified Core Language for Putback-Based Bidirectiona ... 14:00 - 14:30		PEPM A Constraint Language for Static Semantic Analysis Based on Scope Graphs 14:30 - 15:00		PEPM Finally, Safely-Extensible and Efficient Language-Integrated Query 15:00 - 15:30				PEPM Staging Generic Programming 16:00 - 16:30		PEPM Removing Runtime Overhead for Optimized Object Queries 16:30 - 17:00		PEPM Toward Introducing Binding-Time Analysis to MetaOCaml 17:00 - 17:20		PEPM 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 CPP Reception, sponsored by the DeepSpec project 18:00 - 21:00
Room St Petersburg II	CPP Dependent Type Practice 09:00 - 10:00						CPP A Logic of Proofs for Differential Dynamic Logic 10:30 - 11:00		CPP Constructing the Propositional Truncation using Non-recursive HITs 11:00 - 11:30		CPP A Nominal Exploration of Intuitionism 11:30 - 12:00										CPP Bisimulation Up-to Techniques for Psi-calculi 14:00 - 14:30		CPP Planning for Change in a Formal Verification of the Raft Consensus Protocol 14:30 - 15:00		CPP A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules 15:00 - 15:30				CPP Formal Verification of Control-flow Graph Flattening 16:00 - 16:30		CPP 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 Invited Speakers Programming the World of Uncertain Things 09:00 - 10:00
Grand Bay North							POPL Research Papers Temporal Verification of Higher-order Functional Programs 10:30 - 10:55		POPL Research Papers Scaling Network Verification using Symmetry and Surgery 10:55 - 11:20			POPL Research Papers Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates 11:20 - 11:45		POPL Research Papers Reducing Crash Recoverability to Reachability 11:45 - 12:10											POPL Research Papers Query-Guided Maximum Satisfiability 14:20 - 14:45		POPL Research Papers String Solving with Word Equations and Transducers: Decidability and Ap ... 14:45 - 15:10		POPL Research Papers Symbolic Computation of Differential Equivalences 15:10 - 15:35			POPL Research Papers Unboundedness and Downward Closures of Higher-Order Pushdown Automata 15:35 - 16:00				POPL Research Papers Dependent Types and Multi-Monadic Effects in F* 16:30 - 16:55		POPL Research Papers Fabular: Regression Formulas as Probabilistic Programming 16:55 - 17:20			POPL Research Papers Kleenex: Compiling Nondeterministic Transducers to Deterministic Stream ... 17:20 - 17:45
Grand Bay South							POPL Research Papers Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega 10:30 - 10:55		POPL Research Papers Type Theory in Type Theory using Quotient Inductive Types 10:55 - 11:20			POPL Research Papers System Fω with Equirecursive Types for Datatype-generic Programming 11:20 - 11:45		POPL Research Papers A Theory of Effects and Resources: Adjunction Models and Polarised Calculi 11:45 - 12:10											POPL Research Papers Fully-Abstract Compilation by Approximate Back-Translation 14:20 - 14:45		POPL Research Papers Lightweight Verification of Separate Compilation 14:45 - 15:10		POPL Research Papers From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes 15:10 - 15:35			POPL Research Papers Sound Type-dependent Syntactic Language Extension 15:35 - 16:00				POPL Research Papers Decidability of Inferring Inductive Invariants 16:30 - 16:55		POPL Research Papers The Hardness of Data Packing 16:55 - 17:20			POPL 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 Invited Speakers Synthesis of Reactive Controllers for Hybrid Systems 09:00 - 10:00
Grand Bay North							POPL Research Papers Certified Causally Consistent Distributed Key-Value Stores 10:30 - 10:55		POPL Research Papers 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distri ... 10:55 - 11:20			POPL Research Papers A Program Logic for Concurrent Objects under Fair Scheduling 11:20 - 11:45		POPL Research Papers PSync: a partially synchronous language for fault-tolerant distributed ... 11:45 - 12:10											POPL Research Papers Combining Static Analysis with Probabilistic Models to Enable Market-Sc ... 14:20 - 14:45		POPL Research Papers Abstraction Refinement Guided by a Learnt Probabilistic Model 14:45 - 15:10		POPL Research Papers Learning Invariants using Decision Trees and Implication Counterexamples 15:10 - 15:35			POPL Research Papers Symbolic Abstract Data Type Inference 15:35 - 16:00				POPL Research Papers SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Opti ... 16:30 - 16:55		POPL Research Papers PolyCheck: Dynamic Verification of Iteration Space Transformations on A ... 16:55 - 17:20			POPL Research Papers Printing Floating-Point Numbers: A Faster, Always Correct Method 17:20 - 17:45
Grand Bay South							POPL Research Papers Prophet: Automatic Patch Generation via Learning from Successful Patches 10:30 - 10:55		POPL Research Papers Estimating types in binaries using predictive modeling 10:55 - 11:20			POPL Research Papers Algorithmic Analysis of Qualitative and Quantitative Termination Proble ... 11:20 - 11:45		POPL Research Papers Transforming Spreadsheet Data Types using Examples 11:45 - 12:10											POPL Research Papers Principal Type Inference for GADTs 14:20 - 14:45		POPL Research Papers Abstracting Gradual Typing 14:45 - 15:10		POPL Research Papers The Gradualizer: a methodology and algorithm for generating gradual typ ... 15:10 - 15:35			POPL Research Papers Is Sound Gradual Typing Dead? 15:35 - 16:00				POPL Research Papers Effects as sessions, sessions as effects 16:30 - 16:55		POPL Research Papers Monitors and Blame Assignment for Higher-Order Session Types 16:55 - 17:20			POPL 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 Invited Speakers Confluences in Programming Languages Research 09:00 - 10:00
Grand Bay North							POPL Research Papers Newtonian Program Analysis via Tensor Product 10:30 - 10:55		POPL Research Papers Casper: An Efficient Approach to Call Trace Collection 10:55 - 11:20			POPL Research Papers Pushdown Control-flow Analysis for Free 11:20 - 11:45		POPL Research Papers Binding as Sets of Scopes 11:45 - 12:10											POPL Research Papers Learning Programs from Noisy Data 14:20 - 14:45		POPL Research Papers Optimizing Synthesis with Metasketches 14:45 - 15:10		POPL Research Papers Maximal Specification Synthesis 15:10 - 15:35			POPL Research Papers Example-Directed Synthesis: A Type-Theoretic Interpretation 15:35 - 16:00
Grand Bay South							POPL Research Papers Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA 10:30 - 10:55		POPL Research Papers A concurrency semantics for relaxed atomics that permits optimisation a ... 10:55 - 11:20			POPL Research Papers Overhauling SC atomics in C11 and OpenCL 11:20 - 11:45		POPL Research Papers Taming Release-Acquire Consistency 11:45 - 12:10											POPL Research Papers Lattice-Theoretic Progress Measures and Coalgebraic Model Checking 14:20 - 14:45</

POPL 2016 Program

Sun 17 Jan

Mon 18 Jan

Tue 19 Jan

Wed 20 Jan

Thu 21 Jan

Fri 22 Jan

Sat 23 Jan

Sun 17 Jan 2016

VMCAI

VMCAI

VMCAI

VMCAI

VMCAI

Mon 18 Jan 2016

PADL

PADL

PADL

PADL

PADL

PEPM Invited Talks

PEPM Invited Talks

PEPM Invited Talks

PEPM Invited Talks

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

POPL Tutorials

VMCAI

VMCAI

VMCAI

VMCAI

CPP

CPP

CPP

CPP

Tue 19 Jan 2016

PADL

PEPM Invited Talks

PEPM

PEPM

PEPM

PEPM

PEPM

PEPM

PADL

VMCAI

VMCAI

VMCAI

VMCAI

CPP

CPP

CPP

CPP

CPP

PLMW

PLMW

PLMW

PLMW

PLMW

PLMW

Wed 20 Jan 2016

POPL Research Papers

POPL Invited Speakers

POPL Research Papers

POPL Research Papers

POPL Research Papers

POPL Research Papers

POPL Research Papers

POPL Research Papers