Program - POPL 2016

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sun 17 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

	08:50 - 09:00: WelcomeVMCAI at Room St Petersburg I Chair(s): K. Rustan M. LeinoMicrosoft Research

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

	09:00 - 10:00 Talk		Automating Abstract Interpretation VMCAI Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.

	10:30 - 12:00: Abstract InterpretationVMCAI at Room St Petersburg I Chair(s): Peter MüllerETH Zurich

	10:30 - 11:00 Talk		An Abstract Domain of Uninterpreted Functions VMCAI Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard, Peter Stuckey
	11:00 - 11:30 Talk		Predicate Abstraction for Linked Data Structures VMCAI Alexander Bakst, Ranjit JhalaUniversity of California, San Diego
	11:30 - 12:00 Talk		Property Directed Abstract Interpretation VMCAI Noam Rinetzky, Sharon Shoham

	14:00 - 15:30: Abstraction IVMCAI at Room St Petersburg I Chair(s): Eva DarulovaMPI-SWS, Germany

	14:00 - 14:30 Talk		Program Analysis with Local Policy Iteration VMCAI Egor Karpenkov, David MonniauxCNRS, VERIMAG, Philipp Wendler
	14:30 - 15:00 Talk		Lazy Constrained Monotonic Abstraction VMCAI Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng
	15:00 - 15:30 Talk		Polyhedral Approximation of Multivariate Polynomials using Handelman’s Theorem VMCAI Alexandre Maréchal, Alexis Fouilhé, Tim King, David MonniauxCNRS, VERIMAG, Michael Perin

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

	16:00 - 16:30 Talk		D3 : Data-Driven Disjunctive Abstraction VMCAI Hila Peleg, Sharon Shoham, Eran YahavTechnion
	16:30 - 17:00 Talk		Exact Heap Summaries for Symbolic Execution VMCAI Benjamin Hillery, Eric Mercer, Neha Rungta, Suzette Person

Mon 18 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

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

	08:30 - 09:15 Talk		Invited Talk: Learning from Big Code: Probabilistic Models, Program Analysis and Synthesis PEPM Invited Talks I: Martin VechevETH Zurich
	09:15 - 10:00 Talk		Invited Talk: Tracing JITs for Functional Languages PEPM Invited Talks I: Sam Tobin-HochstadtIndiana University

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

	08:30 - 10:00 Talk		T1: An Introduction to Redex with Abstracting Abstract Machines Tutorials David Van HornUniversity of Maryland, College Park Link to publication

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

	08:30 - 10:00 Talk		T3: Syntax-Guided Synthesis (SyGuS) Tutorials Rajeev AlurUniversity of Pennsylvania, Dana FismanUniversity of Pennsylvania, Rishabh SinghMicrosoft Research, Armando Solar-LezamaMIT Link to publication

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

	08:30 - 10:00 Talk		T5: Higher-Order Model Checking Tutorials Naoki KobayashiUniversity of Tokyo, C.-H. Luke OngUniversity of Oxford, UK

	08:45 - 09:00: WelcomePADL at Room Bayboro Chair(s): John ReppyUniversity of Chicago

	09:00 - 10:00: Invited TalkPADL at Room Bayboro

	09:00 - 10:00 Talk		Program Synthesis for Direct Manipulation Interfaces PADL Ravi ChughUniversity of Chicago

	09:00 - 10:00: Invited Talk IIVMCAI at Room St Petersburg I Chair(s): K. Rustan M. LeinoMicrosoft Research

	09:00 - 10:00 Talk		Ironclad - Full Verification of Complex Systems VMCAI Bryan ParnoMicrosoft Research

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

	09:00 - 10:00 Talk		Perspectives on Formal Verfication CPP Harvey FriedmanOhio State University

	10:30 - 12:00: Functional Programming IPADL at Room Bayboro

	10:30 - 11:00 Talk		Simplifying Probabilistic Programs Using Computer Algebra PADL Jacques CaretteMcMaster University, Chung-chieh ShanIndiana University
	11:00 - 11:30 Talk		Haskino: A Remote Monad for Programming the Arduino PADL Mark GrebeUniversity of Kansas, Andy GillUniversity of Kansas
	11:30 - 12:00 Talk		From Monads to Effects and Back PADL Niki VazouUC San Diego, Daan LeijenMicrosoft Research

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

	10:30 - 11:15 Talk		Invited Talk: Using Formal Methods to Eliminate Exploitable Bugs PEPM Invited Talks I: Kathleen FisherTufts University
	11:15 - 12:00 Talk		Invited Talk: Automated Reasoning about Type Systems by Compilation to First-Order Logic PEPM Invited Talks I: Sebastian ErdwegTU Darmstadt, Germany

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

	10:30 - 12:00 Talk		T2: Declare Your Language (Part 1): Hands-On Spoofax Tutorial Tutorials Eelco VisserDelft University of Technology

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

	10:30 - 12:00 Talk		T3: Syntax-Guided Synthesis (SyGuS) (Advanced Material) Tutorials Rajeev AlurUniversity of Pennsylvania, Dana FismanUniversity of Pennsylvania, Rishabh SinghMicrosoft Research, Armando Solar-LezamaMIT Link to publication

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

	10:30 - 12:00 Talk		T4: Programs and Proofs in the Coq Proof Assistant Tutorials Robert RandUniversity of Pennsylvania, Arthur Azevedo de AmorimUniversity of Pennsylvania Link to publication

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

	10:30 - 12:00 Talk		T6: Security and Privacy by Typing in Cryptographic Systems Tutorials Matteo MaffeiSaarland University

	10:30 - 12:00: Hybrid and Timed SystemsVMCAI at Room St Petersburg I Chair(s): David MonniauxCNRS, VERIMAG

	10:30 - 11:00 Talk		Abstract Interpretation with Infinitesimals VMCAI Kengo Kido, Swarat ChaudhuriRice University, Ichiro HasuoUniversity of Tokyo
	11:00 - 11:30 Talk		Lipschitz Robustness of Timed I/O Systems VMCAI Thomas A. HenzingerIST Austria, Jan OtopUniversity of Wrocław, Roopsha SamantaIST Austria
	11:30 - 12:00 Talk		A method for invariant generation for polynomial continuous systems VMCAI Andrew Sogokon, Khalil GhorbalCarnegie Mellon University, Paul Jackson, André Platzer

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

	10:30 - 11:00 Talk		Higher-order Representation Predicates in Separation Logic CPP Arthur Charguéraud
	11:00 - 11:30 Talk		A Unified Coq Framework for Verifying C Programs with Floating-Point Computations CPP Tahina Ramananandro, Paul Mountcastle, Benoit Meister, Richard Lethin
	11:30 - 12:00 Talk		Refinement Based Verification of Imperative Data Structures CPP Peter LammichTechnische Universität München

	14:00 - 15:30: ConstraintsPADL at Room Bayboro

	14:00 - 14:30 Talk		A GPU implementation of the ASP computation PADL 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 PADL Jan JelínekCharles University in Prague, Roman BartákCharles University in Prague
	15:00 - 15:30 Talk		The Picat-SAT Compiler PADL Neng-Fa ZhouCUNY Brooklyn College and Graduate Center, Håkan KjellerstrandCUNY Brooklyn College and Graduate Center

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

	14:00 - 14:45 Talk		Invited Talk: Program Synthesis: Opportunities for the next Decade PEPM Invited Talks I: Rastislav BodikUniversity of Washington, USA
	14:45 - 15:30 Talk		Invited Talk: LMS: a Perspective on Generative Programming PEPM Invited Talks I: Nada AminEPFL

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

	14:00 - 15:30 Talk		T1: An Introduction to Redex with Abstracting Abstract Machines(Advanced Material) Tutorials David Van HornUniversity of Maryland, College Park Link to publication

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

	14:00 - 15:30 Talk		T7: Trace-based Synchronization Synthesis for Concurrent Programs Tutorials Arjun RadhakrishnaMicrosoft, Roopsha SamantaIST Austria

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

	14:00 - 15:30 Talk		T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material) Tutorials Robert RandUniversity of Pennsylvania, Arthur Azevedo de AmorimUniversity of Pennsylvania Link to publication

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

	14:00 - 15:30 Talk		T6: Security and Privacy by Typing in Cryptographic Systems Tutorials Matteo MaffeiSaarland University

	14:00 - 15:30: Dynamic and Static VerificationVMCAI 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 VMCAI Pavel ParizekCharles University in Prague
	14:30 - 15:00 Talk		Cloud-Based Verification of Concurrent Software VMCAI Gerald Holzmann
	15:00 - 15:30 Talk		Abstraction-driven Concolic Testing VMCAI Przemyslaw Daca, Ashutosh Gupta, Thomas A. HenzingerIST Austria

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

	14:00 - 14:30 Talk		The Vampire and the FOOL CPP 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 CPP Lukasz CzajkaUniversity of Innsbruck
	15:00 - 15:30 Talk		Mizar Environment for Isabelle CPP Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity of Bialystok, Institute of Computer Science, Josef Urban

	16:00 - 17:00: Logic ProgrammingPADL at Room Bayboro

	16:00 - 16:30 Talk		The KB paradigm and its application to interactive configuration PADL Pieter Van HertumKU Leuven, Ingmar DassevilleKU Leuven, Gerda JanssensKU Leuven, Marc DeneckerKU Leuven
	16:30 - 17:00 Talk		Default Rules for Curry PADL Sergio AntoyKiel University, Michael HanusKiel University

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

	16:00 - 16:45 Talk		Invited Talk: Fiat: Extensible Code Generation with Proofs PEPM Invited Talks I: Adam ChlipalaMIT
	16:45 - 17:30 Talk		Invited Talk: The Promise of Relational Programming PEPM Invited Talks I: William E. ByrdUniversity of Utah

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

	16:00 - 17:30 Talk		T2: Declare Your Language (Part 2): Name Binding with Scope Graphs Tutorials Eelco VisserDelft University of Technology Link to publication DOI Media Attached

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

	16:00 - 17:30 Talk		T7: Trace-based Synchronization Synthesis for Concurrent Programs Tutorials Arjun RadhakrishnaMicrosoft, Roopsha SamantaIST Austria

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

	16:00 - 17:30 Talk		T5: Higher-Order Model Checking Tutorials Naoki KobayashiUniversity of Tokyo, C.-H. Luke OngUniversity of Oxford, UK

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

	16:00 - 16:30 Talk		Reward-Bounded Reachability Probability for Uncertain Weighted MDPs VMCAI Vahid Hashemi, Holger Hermanns, Lei Song
	16:30 - 17:00 Talk		Parameter Synthesis for Parametric Interval Markov Chains VMCAI Benoit Delahaye, Didier Lime, Laure Petrucci

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

	16:00 - 16:30 Talk		A Modular, Efficient Formalisation of Real Algebraic Numbers CPP 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 CPP Sophie BernardINRIA, Yves BertotINRIA, Laurence RideauINRIA, Pierre-Yves StrubIMDEA Software Institute
	17:00 - 17:30 Talk		Formalizing Jordan Normal Forms in Isabelle/HOL CPP René ThiemannUniversity of Innsbruck, Akihisa Yamada
	17:30 - 18:00 Talk		Formalization of a Newton series representation of polynomials CPP Cyril Cohen, Boris DjalalINRIA

Tue 19 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

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

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

	09:00 - 10:00 Talk		Invited Keynote: Building Languages in Racket: Syntax Objects as an Intermediate Representation PEPM Invited Talks K: Matthew FlattUniversity of Utah

	09:00 - 10:00: Invited Talk IIIVMCAI 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 VMCAI Peter MüllerETH Zurich

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

	09:00 - 10:00 Talk		Dependent Type Practice CPP Leonardo De MouraMicrosoft Research, Redmond

	09:00 - 10:00: Session IPLMW at Room St Petersburg III

	09:00 - 09:30 Talk		Grad School: A Survival Guide PLMW Matthew MightUniversity of Utah, USA Media Attached
	09:30 - 10:00 Talk		Theorem Provers are a PL Researcher's Best Friend PLMW Xavier LeroyInria Media Attached

	10:30 - 12:00: Functional Programming IIPADL at Room Bayboro

	10:30 - 11:00 Talk		Computing with Catalan Families, Generically PADL 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 PADL Paul TarauUniversity of North Texas
	11:30 - 12:00 Talk		Generic Matching of Tree Regular Expressions over Haskell Data Types PADL Alejandro SerranoUtrecht University, Jurriaan HageUtrecht University

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

	10:30 - 11:00 Talk		Practical, General Parser Combinators PEPM 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 PEPM 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 PEPM Shayan Najd, Sam LindleyUniversity of Edinburgh, Josef SvenningssonChalmers University of Technology, Sweden, Philip WadlerUniversity of Edinburgh DOI

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

	10:30 - 11:00 Talk		Pointer Race Freedom VMCAI Frédéric Haziza, Lukáš Holík, Roland Meyer, Sebastian WolffFraunhofer ITWM and TU Kaiserslautern
	11:00 - 11:30 Talk		A program logic for C11 memory fences VMCAI Marko DokoMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany
	11:30 - 12:00 Talk		From Low Level Pointers to High Level Containers VMCAI Kamil Dudka, Lukáš Holík, Petr Peringer, Tomáš VojnarBrno University of Technology

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

	10:30 - 11:00 Talk		A Logic of Proofs for Differential Dynamic Logic CPP Nathan FultonCarnegie Mellon University, André Platzer
	11:00 - 11:30 Talk		Constructing the Propositional Truncation using Non-recursive HITs CPP Floris van DoornCarnegie Mellon University
	11:30 - 12:00 Talk		A Nominal Exploration of Intuitionism CPP Vincent RahliSnT, Mark BickfordCornell University

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

	10:30 - 11:00 Talk		Academia or Industry? PLMW Aarti GuptaPrinceton University Media Attached
	11:00 - 11:30 Talk		Refining Types with SMT PLMW Ranjit JhalaUniversity of California, San Diego Media Attached
	11:30 - 12:00 Talk		How to Write Papers So People Can Read Them PLMW Derek DreyerMPI-SWS Media Attached

	14:00 - 15:30: Domain-Specific Languages IIPEPM 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 PEPM 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 PEPM 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 PEPM Kenichi SuzukiUniversity of Tsukuba, Japan, Oleg Kiselyov, Yukiyoshi Kameyama DOI

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

	14:00 - 14:30 Talk		Regular Symmetry Patterns VMCAI 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 VMCAI Simon Außerlechner, Swen Jacobs, Ayrat Khalimov
	15:00 - 15:30 Talk		A General Modular Synthesis Problem for Pushdown Systems VMCAI Ilaria De Crescenzo, Salvatore La Torre

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

	14:00 - 14:30 Talk		Bisimulation Up-to Techniques for Psi-calculi CPP Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
	14:30 - 15:00 Talk		Planning for Change in a Formal Verification of the Raft Consensus Protocol CPP Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, 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 CPP Michel St-MartinUniversity of Ottawa, Amy FeltyUniversity of Ottawa

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

	14:00 - 14:30 Talk		Student Interaction Activity PLMW Isil DilligUniversity of Texas, Austin, Ross TateCornell University
	14:30 - 15:00 Talk		Automata and Coinduction PLMW Alexandra SilvaRadboud University Nijmegen Media Attached
	15:00 - 15:30 Talk		Unaccustomed As I Am to Public Speaking PLMW John HughesChalmers University of Technology Media Attached

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

	16:00 - 16:30 Talk		Staging Generic Programming PEPM Jeremy YallopUniversity of Cambridge, UK DOI
	16:30 - 17:00 Talk		Removing Runtime Overhead for Optimized Object Queries PEPM Jon Brandvein, Yanhong A. LiuStony Brook University, USA DOI
	17:00 - 17:20 Talk		Toward Introducing Binding-Time Analysis to MetaOCaml PEPM Kenichi AsaiOchanomizu University DOI
	17:20 - 17:40 Talk		Staging beyond Terms: Prospects and Challenges PEPM Jun InoueNational Institute of Advanced Industrial Science and Technology, Japan, Oleg Kiselyov, Yukiyoshi Kameyama DOI

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

	16:00 - 16:30 Talk		Model Checking with Multi-Threaded IC3 Portfolios VMCAI Sagar Chaki, Derrick Karimi
	16:30 - 17:00 Talk		Automatic Generation of Propagation Complete SAT Encodings VMCAI Martin Brain, Liana Hadarean, Daniel KroeningUniversity of Oxford, Ruben Martins

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

	16:00 - 16:30 Talk		Formal Verification of Control-flow Graph Flattening CPP Sandrine BlazyIRISA / University of Rennes 1, Alix TrieuENS Rennes
	16:30 - 17:00 Talk		Axiomatic Semantics for Compiler Verification CPP Steven Schäfer, Sigurd SchneiderSaarland University, Gert SmolkaSaarland University

	16:00 - 17:00: Session IVPLMW at Room St Petersburg III

	16:00 - 16:30 Talk		Two Notions of Beauty in Programming PLMW Robert HarperCarnegie Mellon University Media Attached
	16:30 - 17:00 Talk		Highs and Lows of a Language Researcher PLMW Greg MorrisettCornell University Media Attached

	17:00 - 17:45: Session VPLMW 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) PLMW Dimitrios VytiniotisMicrosoft Research, Cambridge Media Attached

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

	18:00 - 21:00 Social Event		CPP Reception, sponsored by the DeepSpec project CPP

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

	09:00 - 10:00: Invited WedInvited Speakers at Grand Bay Ballroom Chair(s): Rastislav BodikUniversity of Washington, USA

	09:00 - 10:00 Talk		Programming the World of Uncertain Things Invited Speakers Kathryn S McKinleyMicrosoft Research

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

	10:30 - 10:55 Talk		Temporal Verification of Higher-order Functional Programs Research Papers 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 Research Papers 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 Research Papers James Brotherston, Nikos Gorogiannis, Max Kanovich, Reuben Rowe
	11:45 - 12:10 Talk		Reducing Crash Recoverability to Reachability Research Papers Eric KoskinenYale University, Junfeng YangColumbia University

	10:30 - 12:10: Track 2: Types and FoundationsResearch Papers 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 Research Papers 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 Research Papers 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 Research Papers 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 Research Papers 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: Track 1: Decision ProceduresResearch Papers at Grand Bay North Chair(s): Loris D'AntoniUniversity of Pennsylvania

	14:20 - 14:45 Talk		Query-Guided Maximum Satisfiability Research Papers 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 Research Papers Anthony Widjaja LinYale-NUS College, Singapore, Pablo BarceloUniversity of Chile, Chile Media Attached
	15:10 - 15:35 Talk		Symbolic Computation of Differential Equivalences Research Papers 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 Research Papers 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: Track 2: Correct CompilationResearch Papers at Grand Bay South Chair(s): Jens PalsbergUniversity of California, Los Angeles

	14:20 - 14:45 Talk		Fully-Abstract Compilation by Approximate Back-Translation Research Papers 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 Research Papers 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 Research Papers Ed RobbinsKent, Andy KingKent, Tom SchrijversKU Leuven Media Attached
	15:35 - 16:00 Talk		Sound Type-dependent Syntactic Language Extension Research Papers Florian LorenzenTU Berlin, Sebastian ErdwegTU Darmstadt, Germany Pre-print Media Attached File Attached

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

	16:30 - 16:55 Talk		Dependent Types and Multi-Monadic Effects in F* Research Papers 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 Research Papers 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 Research Papers 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: Track 2: Decidability and complexityResearch Papers at Grand Bay South Chair(s): C.-H. Luke OngUniversity of Oxford, UK

	16:30 - 16:55 Talk		Decidability of Inferring Inductive Invariants Research Papers 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 Research Papers Rahman Lavaee, Chen DingUniversity of Rochester Media Attached
	17:20 - 17:45 Talk		The Complexity of Interaction Research Papers Stéphane GimenezUniversity of Innsbruck, Georg MoserUniversity of Innsbruck Media Attached

	19:00 - 22:00: BanquetResearch Papers at Dali Museum

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

	09:00 - 10:00: Invited Speaker ThuInvited Speakers at Grand Bay Ballroom Chair(s): Rupak MajumdarMPI-SWS

	09:00 - 10:00 Talk		Synthesis of Reactive Controllers for Hybrid Systems Invited Speakers Richard M. MurrayCalifornia Institute of Technology Media Attached

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

	10:30 - 10:55 Talk		Certified Causally Consistent Distributed Key-Value Stores Research Papers 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 Research Papers 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 Research Papers 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 Research Papers 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: Track 2: Probabilistic and statistical analysisResearch Papers at Grand Bay South Chair(s): Aditya NoriMicrosoft Research, UK

	10:30 - 10:55 Talk		Prophet: Automatic Patch Generation via Learning from Successful Patches Research Papers Fan LongMIT CSAIL, Martin RinardMassachusetts Institute of Technology, USA Media Attached
	10:55 - 11:20 Talk		Estimating types in binaries using predictive modeling Research Papers 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 Research Papers 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 Research Papers Rishabh SinghMicrosoft Research, Sumit GulwaniMicrosoft Research Media Attached

	14:20 - 16:00: Track 1: Learning and verificationResearch Papers 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 Research Papers 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 Research Papers Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK Media Attached
	15:10 - 15:35 Talk		Learning Invariants using Decision Trees and Implication Counterexamples Research Papers 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 Research Papers Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot Media Attached

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

	14:20 - 14:45 Talk		Principal Type Inference for GADTs Research Papers Sheng ChenUniversity of louisiana at Lafayette, Martin ErwigOregon State University Media Attached
	14:45 - 15:10 Talk		Abstracting Gradual Typing Research Papers 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 Research Papers Matteo CiminiIndiana University, Jeremy G. SiekIndiana University Media Attached
	15:35 - 16:00 Talk		Is Sound Gradual Typing Dead? Research Papers 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: Track 1: OptimizationResearch Papers 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 Research Papers 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 Research Papers Wenlei Bao, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noël 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 Research Papers Marc AndryscoUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego Media Attached

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

	16:30 - 16:55 Talk		Effects as sessions, sessions as effects Research Papers 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 Research Papers 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 Research Papers Davide SangiorgiUniversity of Bologna, Valeria VignudelliUniversity of Bologna/INRIA Media Attached

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

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

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

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

	09:00 - 10:00 Talk		Confluences in Programming Languages Research Invited Speakers David WalkerPrinceton University Media Attached

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

	10:30 - 10:55 Talk		Newtonian Program Analysis via Tensor Product Research Papers 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 Research Papers 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 Research Papers 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 Research Papers Matthew FlattUniversity of Utah Pre-print Media Attached

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

	10:30 - 10:55 Talk		Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA Research Papers 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 Research Papers Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge File Attached
	11:20 - 11:45 Talk		Overhauling SC atomics in C11 and OpenCL Research Papers 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 Research Papers Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany Pre-print Media Attached File Attached

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

	14:20 - 14:45 Talk		Learning Programs from Noisy Data Research Papers 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 Research Papers 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 Research Papers 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 Research Papers Jonathan FranklePrinceton University, Peter-Michael OseraGrinnell College, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania Pre-print Media Attached File Attached

	14:20 - 15:35: Track 2: Foundations of Model CheckingResearch Papers at Grand Bay South Chair(s): Alexandra SilvaRadboud University Nijmegen

	14:20 - 14:45 Talk		Lattice-Theoretic Progress Measures and Coalgebraic Model Checking Research Papers 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 Research Papers 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 Research Papers Koko MuroyaUniversity of Tokyo, Naohiko HoshinoKyoto University, Ichiro HasuoUniversity of Tokyo Media Attached

Sat 23 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

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

	09:00 - 09:15 Day opening		Opening remarks and program chair's report Off the Beaten Track Lindsey KuperIntel Labs
	09:15 - 10:00 Talk		Keynote Talk: Operationalizing Creative Theories Off the Beaten Track K: Chris MartensCarnegie Mellon University

	09:00 - 10:00: Session 1PPS 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? PPS Norman Ramsey Pre-print
	09:20 - 09:30 Meeting		Discussion 1 PPS
	09:30 - 09:50 Talk		An Interface for Black Box Learning in Probabilistic Programs PPS 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 PPS

	09:00 - 10:00: Session ICoqPL at Room St Petersburg III

	09:00 - 10:00 Talk		Coq 8.5 at work and the future of Coq CoqPL Matthieu SozeauInria

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

	10:30 - 10:55 Talk		Chanakya: Computer-Aided Strategic Reasoning Off the Beaten Track Suguman BansalRice University, USA, A: Swarat ChaudhuriRice University Pre-print
	10:55 - 11:20 Talk		Programming Interactivity Requires Both Semantics and Semiotics Off the Beaten Track Joseph Osborn, Michael Mateas Pre-print
	11:20 - 11:45 Talk		Correct-by-Construction Interactive Software: From Declarative Specifications to Efficient Implementations Off the Beaten Track Kyle Headley, A: Matthew HammerUniversity of Colorado, Boulder Pre-print
	11:45 - 12:10 Talk		Challenges Facing a High-Level Language for Machine Knitting Off the Beaten Track Lea Albaugh, James McCann Pre-print

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

	10:30 - 10:50 Talk		Models for Probabilistic Programs with an Adversary PPS Robert RandUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania Pre-print
	10:50 - 11:00 Meeting		DIscussion 3 PPS
	11:00 - 11:20 Talk		The Semantics of Figaro, an Embedded Probabilistic Programming Language PPS Avi PfefferCharles River Analytics, Brian RuttenbergCharles River Analytics Pre-print
	11:20 - 11:30 Meeting		Discussion 4 PPS
	11:30 - 12:15 Meeting		Implementor Panel: What can semantics do for probabilistic programming and what can probabilistic programming do for semantics? PPS Angelika KimmigKU Leuven, Oleg Kiselyov, Jan-Willem van de MeentUniversity of Oxford, Avi PfefferCharles River Analytics, M: Frank WoodUniversity of Oxford

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

	10:30 - 10:55 Talk		A Coq Library for Binary Logical Relations CoqPL Jérémie Koenig Link to publication
	10:55 - 11:20 Talk		A Coinduction Proof Rule for Hoare Doubles CoqPL Christian J. BellMIT CSAIL Link to publication
	11:20 - 11:45 Talk		Formalizing Simple Refinements in Coq CoqPL 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 CoqPL Clément Pit-ClaudelMIT CSAIL, Pierre Courtieu Link to publication

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

	14:00 - 14:45 Talk		Keynote Talk: Generalising Abstraction Off the Beaten Track K: Robert AtkeyUniversity of Strathclyde
	14:45 - 15:10 Talk		The Semantics of Syntax: Applying Denotational Semantics to Hygienic Macro Systems Off the Beaten Track A: Neel Krishnaswami Pre-print
	15:10 - 15:35 Talk		Affine Functional Programs as Higher-order Boolean Circuits Off the Beaten Track Damiano Mazza Pre-print

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

	14:00 - 14:20 Talk		A Lambda-Calculus Foundation for Universal Probabilistic Programming PPS 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 PPS
	14:30 - 14:50 Talk		Making our Own Luck: A Language for Random Generators PPS 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 PPS
	15:00 - 15:20 Talk		Semantics of Higher-order Probabilistic Programs PPS 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 PPS

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

	14:00 - 15:00 Talk		A Tutorial on using the Paco Library for coinductive reasoning CoqPL Chung-Kil HurSeoul National University
	15:00 - 15:25 Talk		Certified Desugaring of Javascript Programs using Coq CoqPL Marek MaterzokUniversity of Wroclaw Link to publication

	15:30 - 16:30: Poster SessionPPS at Room St Petersburg II

	15:30 - 16:30 Meeting		Insomnia: Types and Modules for Probabilistic Programming PPS 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 PPS 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 PPS Larry MossIndiana University, Chung-chieh ShanIndiana University, Alexandra SilvaRadboud University Nijmegen Pre-print
	15:30 - 16:30 Meeting		Reasoning about Probability and Nondeterminism PPS 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 PPS Johannes HölzlTechnische Universität München Pre-print
	15:30 - 16:30 Meeting		A Denotational Semantics of a Probabilistic Stream-Processing Language PPS 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 PPS Ryan CulpepperNortheastern University Pre-print
	15:30 - 16:30 Meeting		Problems of the Lightweight Implementation of Probabilistic Programming PPS Oleg Kiselyov Pre-print
	15:30 - 16:30 Meeting		Parameterized Probability Monad PPS 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 PPS Adam ŚcibiorUniversity of Cambridge, Bernhard SchölkopfMPI Tuebingen Pre-print

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

	16:00 - 16:25 Talk		Declarative, Secure, Convergent Edge Computation Off the Beaten Track A: Christopher Meiklejohn Pre-print
	16:25 - 16:50 Talk		Starting from a Clean Slate: Creating a Top-down Parseable Runtime Off the Beaten Track A: Randolph Langley Pre-print
	16:50 - 17:15 Talk		New Tools and Practices for Online Collaboration in Teaching, Learning, and Research of Programming Languages Off the Beaten Track A: William E. ByrdUniversity of Utah Pre-print
	17:15 - 17:30 Day closing		Closing remarks Off the Beaten Track

	16:00 - 18:00: Session IVCoqPL at Room St Petersburg III

	16:00 - 16:25 Talk		The Category-theoretic Solution of Recursive Ultra-metric Space Equations CoqPL Amin Timany, Bart JacobsiMinds - Distrinet, KU Leuven Link to publication
	16:25 - 16:50 Talk		A Case for Tactics with (Limited) Side Effects CoqPL Benjamin Delaware Pre-print
	16:50 - 17:15 Talk		Formal Verification of Stability Properties of Cyber-Physical Systems CoqPL 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 CoqPL Andrew AppelPrinceton
	17:45 - 18:00 Talk		Discussion CoqPL

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

	16:30 - 16:50 Talk		eXchangeable Random Primitives PPS Nathanael L. AckermanHarvard University, Cameron FreerGamalon, Daniel RoyUniversity of Toronto Pre-print
	16:50 - 17:00 Meeting		Discussion 8 PPS
	17:00 - 17:20 Talk		An Application of Computable Distributions to the Semantics of Probabilistic Programs PPS Daniel HuangHarvard University, Greg MorrisettCornell University Pre-print
	17:20 - 17:30 Meeting		Discussion 9 PPS
	17:30 - 17:50 Talk		On The Semantic Intricacies of Conditioning PPS 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 PPS

Sun 17 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
Room St Petersburg I											VMCAI Welcome		VMCAI Invited Talk I																		VMCAI Abstract Interpretation																																										VMCAI Abstraction I																								VMCAI Abstraction II

Mon 18 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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

Tue 19 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
Room Bayboro							PADL Functional Programming II
Room Demens				PEPM Invited Talks Keynote			PEPM							PEPM				PEPM
Room Harbor View							PEPM Parsing & Domain-Specific Languages I							PEPM Domain-Specific Languages II				PEPM Staging
Room St Petersburg I				PADL VMCAI Invited Talk III 09:00 - 10:00			VMCAI Concurrent Programs							VMCAI Parameterized and Component-Based Systems				VMCAI Solver Improvements				CPP CPP Reception, sponsored by the DeepSpec project
Room St Petersburg II				CPP Session 5: Invited talk by Leonardo de Moura			CPP Session 6: Foundations							CPP Session 7: Verification for Concurrent and Distributed Systems				CPP Session 8: Compiler Verification
Room St Petersburg III			PLMW Welcome Session	PLMW Session I			PLMW Session II							PLMW Session III				PLMW Session IV		PLMW Session V

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
Dali Museum												Research Papers Banquet
Grand Bay Ballroom	Invited Speakers Invited Wed
Grand Bay North				Research Papers Track 1: Algorithmic Verification								Research Papers Track 1: Decision Procedures					Research Papers Track 1: Language Design
Grand Bay South				Research Papers Track 2: Types and Foundations								Research Papers Track 2: Correct Compilation					Research Papers Track 2: Decidability and complexity

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
Grand Bay Ballroom	Invited Speakers Invited Speaker Thu
Grand Bay North				Research Papers Track 1: Foundations of distributed systems								Research Papers Track 1: Learning and verification					Research Papers Track 1: Optimization			Research Papers SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business Meeting
Grand Bay South				Research Papers Track 2: Probabilistic and statistical analysis								Research Papers Track 2: Types, Generally or Gradually					Research Papers Track 2: Sessions and processes
Lobby III												SRC POPL SRC Posters and Reception

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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

Sat 23 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
Room St Petersburg I	Off the Beaten Track Session One			Off the Beaten Track Session Two							Off the Beaten Track Session Three				Off the Beaten Track Session Four
Room St Petersburg II	PPS Session 1			PPS Session 2							PPS Session 3			PPS Poster Session		PPS Session 5
Room St Petersburg III	CoqPL Session I			CoqPL Session II							CoqPL Session III				CoqPL Session IV

Sun 17 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change


Room

POPL 2016 Program

Filter Program

Program Display Configuration

Sun 17 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Wed 20 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Thu 21 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Fri 22 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Sun 17 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

VMCAI

VMCAI

VMCAI

VMCAI

VMCAI

Mon 18 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

PADL

PADL

PADL

PADL

PADL

PEPM Invited Talks

PEPM Invited Talks

PEPM Invited Talks

PEPM Invited Talks

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

Tutorials

VMCAI

VMCAI

VMCAI

VMCAI

CPP

CPP

CPP

CPP

Tue 19 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

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 Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Research Papers

Invited Speakers

Research Papers

Research Papers

Research Papers

Research Papers

Sun 17 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Sun 17 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Sun 17 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change