Program - POPL 2017

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect 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 15 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 10:00	First Morning SessionTTT at Salle 105, Barre 44-54 Chair(s): Assia MahboubiINRIA

08:50 10m Day opening		Welcome TTT
09:00 20m Talk		A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT David ThibodeauMcGill University, Canada, Alberto Momigliano, Brigitte PientkaMcGill University
09:20 20m Talk		Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT Steven Keuchel, Koar Marntirosian, Tom SchrijversKU Leuven
09:40 20m Talk		Equivalence of System F and λ2 in Abella TTT Jonas Kaiser, Gert SmolkaSaarland University

09:00 - 10:00	Invited talk 1VMCAI at Amphitheater 44 Chair(s): David MonniauxCNRS, VERIMAG

09:00 60m Talk		Detecting Strict Aliasing Violations in the Wild VMCAI Pascal CuoqTrust-in-Soft File Attached

09:15 - 10:00	Session ISCM at Salle 109, Barre 44-54

09:15 45m Talk		What is Secure Compilation? Part I SCM Marco PatrignaniMPI-SWS, Germany Link to publication

10:00 - 10:30	Coffee breakCatering at Catering area

10:00 30m Coffee break		Break Catering

10:30 - 12:00	Program AnalysisVMCAI at Amphitheater 44 Chair(s): Boris YakobowskiCEA - LIST

10:30 30m Talk		Partitioned Memory Models for Program Analysis. VMCAI Wei WangGoogle, Inc., Clark BarrettStanford University, Thomas WiesNew York University File Attached
11:00 30m Talk		Property Directed Reachability for Proving Absence of Concurrent Modification Errors VMCAI Asya FrumkinTel Aviv University, Yotam M. Y. FeldmanTel Aviv University, Ondřej LhotákUniversity of Waterloo, Canada, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university File Attached
11:30 30m Talk		Stabilizing Floating-Point Programs using Provenance Analysis VMCAI Yijia GuNortheastern University, Thomas WahlNortheastern University

10:30 - 12:00	Second Morning SessionTTT at Salle 105, Barre 44-54 Chair(s): Keiko Nakata

10:30 50m Talk		Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron TombGalois, Inc.
11:20 20m Talk		Modelling Program Behaviour within Software Verification Tool LAV TTT Milena Vujosevic Janicic
11:40 20m Talk		agdARGS - Declarative Hierarchical Command Line Interfaces TTT Guillaume AllaisRadboud University Nijmegen

10:30 - 12:00	Session IISCM at Salle 109, Barre 44-54

10:30 10m Talk		What is Secure Compilation? Part II (Short talk) SCM Cătălin HriţcuInria Paris Link to publication
10:40 10m Talk		Can relational logic facilitate secure compilation? (Short talk) SCM David NaumannStevens Institute of Technology File Attached
10:50 10m Talk		Full Abstraction for Language Design (Short talk) SCM Gabriel SchererNortheastern University File Attached
11:00 10m Talk		Cogent: Where we Stand and What Comes Next (Short talk) SCM Christine RizkallahUniversity of Pennsylvania, USA File Attached
11:15 45m Talk		Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities SCM Lau Skorstengaard File Attached

12:00 - 14:00	BuffetCatering at Catering area

12:00 2h Lunch		Lunch Catering

14:00 - 15:30	Concurrency 1VMCAI at Amphitheater 44 Chair(s): Camille CotiLIPN, Université Paris 13

14:00 30m Talk		Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI Igor KonnovTU Wien, Josef WidderTU Wien, Francesco Spegni, Luca Spalazzi
14:30 30m Talk		Independence Abstractions and Models of Concurrency VMCAI Vijay D'SilvaGoogle Inc., Daniel KroeningUniversity of Oxford, Marcelo SousaUniversity of Oxford
15:00 30m Talk		Static Analysis of Communicating Process using Symbolic Transducers VMCAI Vincent BotbolCEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le GallCEA LIST, Emmanuel ChaillouxLIP6 - UPMC Media Attached File Attached

14:00 - 15:30	First Afternoon SessionTTT at Salle 105, Barre 44-54 Chair(s): Bas Spitters

14:00 50m Talk		Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders MörtbergInria
14:50 20m Talk		Equations: a tool for dependent pattern-matching TTT Cyprien Mangin, Matthieu SozeauInria File Attached
15:10 20m Talk		Coq's Prolog and application to defining semi-automatic tactics TTT Théo ZimmermannIRIF, Université Paris Diderot, Hugo Herbelin File Attached

14:00 - 15:30	Session IIISCM at Salle 109, Barre 44-54

14:00 45m Talk		Linking Types: Secure compilation of multi-language programs SCM Daniel PattersonNortheastern University File Attached
14:45 45m Talk		Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing SCM Dominique DevrieseiMinds - Distrinet, KU Leuven File Attached

15:30 - 16:00	Coffee breakCatering at Catering area

15:30 30m Coffee break		Break Catering

16:00 - 17:30	Decision proceduresVMCAI at Amphitheater 44 Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

16:00 30m Talk		Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games VMCAI Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences File Attached
16:30 30m Talk		Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-Alpes File Attached
17:00 30m Talk		Matching multiplications in Bit-Vector formulas VMCAI Supratik ChakrabortyIIT Bombay, Ashutosh Gupta, Rahul JainTata Institute of Fundamental Research File Attached

16:00 - 18:00	Second Afternoon SessionTTT at Salle 105, Barre 44-54 Chair(s): Hugo Herbelin

16:00 50m Talk		Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq TTT Robbert KrebbersDelft University of Technology, Netherlands
16:50 20m Talk		Introducing MetaCoq: A Safe Tactic Language for Coq TTT Beta ZilianiFAMAF, UNC (Argentina) / CONICET (Argentina)
17:10 50m Other		COST EUTypes session TTT

16:00 - 17:30	Session IVSCM at Salle 109, Barre 44-54

16:00 45m Talk		Software Fault Isolation avec CompCert SCM Frédéric Besson File Attached
16:45 45m Talk		Security preserving compilation of low-level programs embedded in F* SCM Jonathan ProtzenkoMicrosoft Research File Attached

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 09:00	Opening remarksPADL at Salle 116, Barre 44-54 Chair(s): Yuliya LierlerUniversity of Nebraska, Walid TahaHalmstad University

08:50 10m Talk		Opening remarks PADL

09:00 - 10:00	Invited talk 2VMCAI at Amphitheater 44 Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot

09:00 60m Talk		Verified Concurrent Code: Tricks of the Trade VMCAI A: Ernie CohenAmazon Web Services

09:00 - 10:00	Invited TalkCPP at Auditorium

09:00 60m Talk		Porting the HOL Light Analysis Library: Some Lessons CPP Lawrence PaulsonUniversity of Cambridge File Attached

09:00 - 12:00	Gradual Typing (AM)Tutorials at Salle 105, Barre 44-54

09:00 3h Talk		The State of the Art in Gradual Typing Tutorials Jeremy G. SiekIndiana University Bloomington

09:00 - 12:00	Lean (AM)Tutorials at Salle 107, Barre 44-54

09:00 3h Talk		The Lean Theorem Prover Tutorials Leonardo De MouraMicrosoft Research, Redmond, Gabriel EbnerVienna University of Technology, Jared RoeschUniversity of Washington, USA, Sebastian UllrichKarlsruhe Institute of Technology

09:00 - 10:00	KeynotePEPM at Salle 109, Barre 44-54 Chair(s): Ulrik Pagh SchultzUniversity of Southern Denmark

09:00 60m Talk		Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk) PEPM Daniil BerezunJetBrains, Russia, Neil D. JonesUniversity of Copenhagen, Danmark DOI

09:00 - 12:00	Flow (AM)Tutorials at Salle 112, Barre 44-54

09:00 3h Talk		Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials Avik ChaudhuriFacebook Media Attached

09:00 - 12:00	Frama-C (AM)Tutorials at Salle 114, Barre 44-54

09:00 3h Talk		Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials François BobotCEA, Loïc Correnson, Boris YakobowskiCEA - LIST

09:00 - 10:00	Invited TalkPADL at Salle 116, Barre 44-54

09:00 60m Talk		Proof checking and logic programming PADL Dale MillerINRIA Saclay and LIX

10:00 - 10:30	Coffee breakCatering at Auditorium Hall

10:00 30m Coffee break		Break Catering

10:30 - 12:00	Numerical domainsVMCAI at Amphitheater 44 Chair(s): Laure GonnordUniversity of Lyon & LIP, France

10:30 30m Talk		Sound Bit-Precise Numerical Domains VMCAI Tushar SharmaUniversity of Wisconsin - Madison, USA, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc. File Attached
11:00 30m Talk		Efficient Elimination of Redundancies in Polyhedra using Raytracing VMCAI Alexandre Maréchal, Michael Perin Media Attached File Attached
11:30 30m Talk		Finding Relevant Templates via the Principal Component Analysis VMCAI Yassamine SeladjiUniversity of Tlemcen File Attached

10:30 - 12:00	Algorithm and library verificationCPP at Auditorium

10:30 30m Talk		Verifying a hash table and its iterators in higher-order separation logic CPP François Pottier
11:00 30m Talk		A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm CPP Jose Divasón, Sebastiaan Joosten, René ThiemannUniversity of Innsbruck, Akihisa Yamada
11:30 30m Talk		Formal foundations of 3D geometry for modeling robot manipulators CPP Reynald AffeldtAIST, Japan, Cyril Cohen

10:30 - 12:00	Programming languagesPEPM at Salle 109, Barre 44-54 Chair(s): Andrew FarmerFacebook

10:30 30m Talk		Lightweight Soundness for Towers of Language Extensions PEPM Alejandro SerranoUtrecht University, Jurriaan HageUtrecht University
11:00 30m Talk		Detecting code clones with gaps by function applications PEPM Tsubasa MatsushitaShibaura Institute of Technology, Isao SasanoShibaura Institute of Technology
11:30 30m Talk		PEG Parsing in Less Space Using Progressive Tabling and Dynamic AnalysisBest Paper PEPM Fritz HengleinDIKU, Denmark, Ulrik Terp RasmussenDIKU, University of Copenhagen

10:30 - 12:00	Answer Set ProgrammingPADL at Salle 116, Barre 44-54

10:30 30m Talk		Lowering the learning curve for declarative programming: a Python API for the IDP system PADL Joost VennekensKU Leuven
11:00 30m Talk		Extending Answer Set Programs with Interpreted Functions as First-class Citizens PADL Christoph RedlVienna University of Technology
11:30 30m Talk		Integrating Answer Set Programming with Object-oriented Languages PADL Jakob RathVienna University of Technology, Christoph RedlVienna University of Technology

12:00 - 14:00	BuffetCatering at Catering area

12:00 2h Lunch		Lunch Catering

14:00 - 15:30	Model-checking and bug findingVMCAI at Amphitheater 44 Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

14:00 30m Talk		Effective Bug Finding in C Programs with Shape and Effect Abstraction VMCAI Iago AbalIT University of Copenhagen, Claus BrabrandIT University of Copenhagen, Denmark, Andrzej WąsowskiIT University of Copenhagen, Denmark
14:30 30m Talk		Reduction of Workflow Nets for Generalised Soundness Verification VMCAI Hadrien BrideFemto-ST / Université de Franche-Comté, Olga KouchnarenkoFemto-ST / Université de Franche-Comté, Fabien PeureuxFemto-ST / Université de Franche-Comté + Smartesting S&S Media Attached
15:00 30m Talk		Dynamic Reductions for Model Checking Concurrent Software. VMCAI Henning GüntherTechnische Universität Wien, Alfons LaarmanVienna University of Technology, Ana SokolovaUniversity of Salzburg, Georg WeissenbacherTechnische Universität Wien File Attached

14:00 - 15:30	Automated proof and its verificationCPP at Auditorium

14:00 30m Talk		BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP Jan Jakubuv, Josef Urban
14:30 30m Talk		Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP Reuben RoweUniversity College London, James Brotherston
15:00 30m Talk		Formalization of Karp-Miller Tree Construction on Petri Nets CPP Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto

14:00 - 17:00	Gradual Typing (PM)Tutorials at Salle 105, Barre 44-54

14:00 3h Talk		The State of the Art in Gradual Typing Tutorials Jeremy G. SiekIndiana University Bloomington

14:00 - 17:00	Lean (PM)Tutorials at Salle 107, Barre 44-54

14:00 3h Talk		The Lean Theorem Prover Tutorials Leonardo De MouraMicrosoft Research, Redmond, Gabriel EbnerVienna University of Technology, Jared RoeschUniversity of Washington, USA, Sebastian UllrichKarlsruhe Institute of Technology

14:00 - 15:30	Tutorial (Idris, Inside-Out) and Poster SessionPEPM at Salle 109, Barre 44-54 Chair(s): Ulrik Pagh SchultzUniversity of Southern Denmark, Jeremy YallopUniversity of Cambridge, UK

14:00 60m Talk		Idris, Inside-Out: A Tutorial on Extending Idris in Idris PEPM David Thrane ChristiansenIndiana University
15:00 30m Talk		Invited posters PEPM Nada AminEPFL, Tiark RompfPurdue University, Oleg Kiselyov, Aggelos BiboudisUniversity of Athens, Nick PalladinosNessos Information Technologies, SA, Yannis SmaragdakisUniversity of Athens
15:00 30m Talk		Language-integrated Query with Ordering, Grouping and Outer Joins (poster) PEPM Tatsuya KatsushimaTohoku University, Japan, Oleg Kiselyov

14:00 - 17:00	Flow (PM)Tutorials at Salle 112, Barre 44-54

14:00 3h Talk		Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials Avik ChaudhuriFacebook Media Attached

14:00 - 17:00	Frama-C (PM)Tutorials at Salle 114, Barre 44-54

14:00 3h Talk		Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials François BobotCEA, Loïc Correnson, Boris YakobowskiCEA - LIST

14:00 - 15:30	Testing and GamesPADL at Salle 116, Barre 44-54

14:00 30m Talk		Failing Faster: Overlapping Patterns for Property-Based Testing PADL Jonathan FowlerUniversity of Nottingham, Graham HuttonUniversity of Nottingham
14:30 30m Talk		Boltzmann Samplers for Closed Simply-Typed Lambda Terms PADL Maciej BendkowskiJagiellonian University, Katarzyna GrygielJagiellonian University, Paul TarauUniversity of North Texas
15:00 30m Talk		Selection Equilibria of Higher-Order Games PADL Paulo OlivaQueen Mary University of London, Jules HedgesUniversity of Oxford, Viktor WinschelETH Zürich, Philipp ZahnUniversity of St. Gallen, Evguenia ShpritsUniversity of Mannheim

15:30 - 16:00	Coffee breakCatering at Auditorium Hall

15:30 30m Coffee break		Break Catering

16:00 - 17:30	Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44 Chair(s): Constantin EneaLIAFA, Université Paris Diderot

16:00 30m Talk		Block-wise abstract interpretation by combining abstract domains with SMT VMCAI Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang
16:30 30m Talk		IC3 - Flipping the E in ICE VMCAI Yakir Vizel, Arie GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University
17:00 30m Talk		Counterexample Validation and Interpolation-Based Refinement for Forest Automata VMCAI Lukáš Holík, Martin HruskaBrno University of Technology , Ondřej LengálBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomáš VojnarBrno University of Technology

16:00 - 18:00	Formalized mathematics with numerical computationsCPP at Auditorium

16:00 30m Talk		A Coq Formal Proof of the Lax–Milgram theorem CPP Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
16:30 30m Talk		A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations CPP Erik Martin-DorelIRIT, Université Paul Sabatier, Pierre Roux
17:00 30m Talk		Markov Processes in Isabelle/HOL CPP Johannes HölzlTechnische Universität München DOI Pre-print File Attached
17:30 30m Talk		Formalising Real Numbers in Homotopy Type Theory CPP Gaetan Gilbert

16:00 - 17:00	Transformation (part I)PEPM at Salle 109, Barre 44-54 Chair(s): Chung-chieh ShanIndiana University, USA

16:00 30m Talk		Verification of Code Generators via Higher-Order Model Checking PEPM Takashi SuwaUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Atsushi IgarashiKyoto University
16:30 30m Talk		Interactive data representation migration: Exploiting program dependence to aid program transformation PEPM Krishna NarasimhanGoethe University, Julia LawallInria/LIP6, Christoph ReichenbachGoethe University

16:00 - 17:30	Applications I and InferencePADL at Salle 116, Barre 44-54

16:00 30m Talk		A Domain-Specific Language for Software-Defined Radio PADL Geoffrey MainlandDrexel University
16:30 30m Talk		A Declarative DSL for Customized Rendering of Text-Based Art PADL Felix Klock
17:00 30m Talk		Using Iterative Deepening for Probabilistic Logic Inference PADL Theofrastos MantadelisUniversidade do Porto, Ricardo Rocha

	19:30 - 22:00	BanquetVMCAI at Procope

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 09:00	Welcome SessionPLMW at Salle 107, Barre 44-54

08:50 10m Day opening		Welcome Sesssion PLMW

09:00 - 10:00	Invited talk 3VMCAI at Amphitheater 44 Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

09:00 60m Talk		Verification of Cancer Programs VMCAI Jasmin FisherMicrosoft Research

09:00 - 10:00	Invited TalkCPP at Auditorium

09:00 60m Talk		Mechanized verification of preemptive OS kernels CPP Xinyu FengUniversity of Science and Technology of China File Attached

09:00 - 10:00	Session 1 PPS at Salle 105, Barre 44-54 Chair(s): Cameron FreerGamalon and Borelian

09:00 60m Talk		Towards a metric semantics for probabilistic programming (invited talk) PPS Gordon Plotkin

09:00 - 10:00	Session IPLMW at Salle 107, Barre 44-54

09:00 30m Talk		Time management, family and quality of life PLMW Kathleen FisherTufts University File Attached
09:30 30m Talk		Abductive Reasoning in Deductive Verification PLMW Isil DilligUT Austin File Attached

09:00 - 10:00	Tutorial: reversible computingPEPM at Salle 109, Barre 44-54 Chair(s): Ulrik Pagh SchultzUniversity of Southern Denmark

09:00 60m Talk		Reversible computing from a programming language perspective PEPM Robert Glück

09:00 - 10:00	Applications IIPADL at Salle 116, Barre 44-54

09:00 30m Talk		Funky Grooves: Declarative Programming of Full-Fledged Musical Applications PADL Henrik Nilsson, Guerric ChupinENSTA ParisTech
09:30 30m Talk		DALI for Cognitive Robotics: Principles and Prototype Implementation PADL Stefania CostantiniDipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila, Giovanni De GasperisDipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Giulio NazziconeDipartimento di Ingegneria e Scienze dell'Informazione eMatematica

10:00 - 10:30	Coffee breakCatering at Auditorium Hall

10:00 30m Coffee break		Break Catering

10:30 - 12:00	Model Checking and SynthesisVMCAI at Amphitheater 44 Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot

10:30 30m Talk		Reachability for dynamic parametric processes VMCAI Anca MuschollUniversité de Bordeaux / LaBRI, Helmut SeidlTechnische Universität München, Igor WalukiewiczCNRS, LaBRI
11:00 30m Talk		Synthesizing Non-Vacuous Systems VMCAI Roderick BloemInstitute of Software Technology, Graz University of Technology , Hana Chockler, Masoud EbrahimiInstitute of Applied Information Processing and Communications, Graz University of Technology, Ofer StrichmanTechnion File Attached
11:30 30m Talk		Solving Nonlinear Integer Arithmetic with MCSat VMCAI Dejan JovanovićSRI International

10:30 - 12:00	Verified programming toolsCPP at Auditorium

10:30 30m Talk		Verified compilation of CakeML to multiple machine-code targets CPP Anthony FoxUniversity of Cambridge, UK, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanIHPC at A*STAR, Singapore, Ramana Kumar
11:00 30m Talk		COMPLX: a verification framework for concurrent imperative programs CPP Sidney AmaniUNSW, Australia, June AndronickData61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin, Corey Lewis, Christine RizkallahUniversity of Pennsylvania, USA, Joseph Tuong
11:30 30m Talk		Verifying dynamic race detection CPP William ManskyUniversity of Pennsylvania, Yuanfeng PengUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania, Joseph DeviettiUniversity of Pennsylvania

10:30 - 12:00	Session 2 PPS at Salle 105, Barre 44-54 Chair(s): Chad ScherrerGalois, Inc.

10:30 20m Talk		An application of computable distributions to the semantics of probabilistic programs: part 2 PPS Daniel HuangHarvard University, Greg MorrisettCornell University
10:50 10m Meeting		Discussion 1 PPS
11:00 20m Talk		Probabilistic programming and a domain theoretic approach to Skorohod's theorem PPS Michael MisloveTulane
11:20 10m Meeting		Discussion 2 PPS
11:30 20m Talk		Building inference algorithms from monad transformers PPS Adam ŚcibiorUniversity of Cambridge, Yufei CaiUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany, Zoubin GhahramaniUniversity of Cambridge
11:50 10m Meeting		Discussion 3 PPS

10:30 - 12:00	Session IIPLMW at Salle 107, Barre 44-54

10:30 30m Talk		What is research and how to do it? Thinking globally and acting locally. PLMW Michael HicksUniversity of Maryland at College Park, USA File Attached
11:00 30m Talk		Mechanizing Meta-Theory in Beluga PLMW Brigitte PientkaMcGill University File Attached
11:30 30m Talk		Research: The Industrial Culture PLMW Nikhil SwamyMicrosoft Research File Attached

10:30 - 12:00	TypesPEPM at Salle 109, Barre 44-54 Chair(s): Robert Glück

10:30 30m Talk		Cost versus Precision for Approximate Typing for Python PEPM Levin FritzUtrecht University, Jurriaan HageUtrecht University
11:00 30m Talk		Refining types using type guards in TypeScript PEPM Ivo Gabe de WolffUtrecht University, Jurriaan HageUtrecht University
11:30 30m Talk		Predicting Resource Consumption of Higher-Order Workflows PEPM Markus KlinikRadboud University Nijmegen, Jurriaan HageUtrecht University, Jan Martin JansenNetherlands Defence Academy, Rinus PlasmeijerRadboud University Nijmegen

10:30 - 12:00	Programming LanguagesPADL at Salle 116, Barre 44-54

10:30 30m Talk		Improving Non-deterministic Computations in Functional Logic Programs PADL Sergio AntoyKiel University, Michael HanusKiel University
11:00 30m Talk		Canonicalizing High-Level Constructs in Picat PADL Neng-Fa ZhouCUNY Brooklyn College and Graduate Center, Jonathan FruhmanCUNY Brooklyn College
11:30 30m Talk		An Overview of PRhoLog PADL Besik DunduaInstitute of Applied Mathematics, Tbilisi State University, Temur Kutsia, Klaus Reisenberger-HagmayerJohannes Kepler University Linz

12:00 - 14:00	BuffetCatering at Catering area

12:00 2h Lunch		Lunch Catering

14:00 - 15:30	Abstract InterpretationVMCAI at Amphitheater 44 Chair(s): Roberto GiacobazziUniversity of Verona, Italy

14:00 30m Talk		Complete Abstractions and Subclassical Modal Logics VMCAI Vijay D'SilvaGoogle, Marcelo SousaUniversity of Oxford
14:30 30m Talk		Structuring Abstract Interpreters through State and Value Abstractions VMCAI David BühlerCEA LIST, Boris YakobowskiCEA - LIST, Sandrine BlazyUniversity of Rennes 1, France Media Attached
15:00 30m Talk		Conjunctive Abstract Interpretation using Paramodulation VMCAI Mooly SagivTel Aviv University, A: Or OzeriTel Aviv university, Oded PadonTel Aviv University, Noam RinetzkyTel Aviv University Media Attached

14:00 - 15:30	Homotopy type theoryCPP at Auditorium

14:00 30m Talk		The HoTT library: a formalization of homotopy type theory in Coq CPP Andrej BauerUniversity of Ljubljana, Jason GrossMIT CSAIL, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu SozeauInria, Bas Spitters Pre-print
14:30 30m Talk		Lifting proof-relevant unification to higher dimensions CPP Jesper CockxiMinds, Belgium, Dominique DevrieseiMinds - Distrinet, KU Leuven
15:00 30m Talk		The Next 700 Syntactical models of type theory CPP Simon Boulier, Pierre-Marie Pédrot, Nicolas TabareauInria, France

14:00 - 15:30	Session 3 PPS at Salle 105, Barre 44-54 Chair(s): Sam StatonUniversity of Oxford

14:00 20m Talk		Commutativity logic for probabilistic trace equivalence: complete or not? PPS Paul Blain Levy, Nathan BowlerUniversität Hamburg
14:20 10m Meeting		Discussion 4 PPS
14:30 20m Talk		Mathematical structures of probabilistic programming PPS Ilias GarnierUniversity of Edinburgh, Fredrik DahlqvistUniversity College London, Florence ClercMcGill University, Vincent DanosENS Paris/CNRS
14:50 10m Meeting		Discussion 5 PPS
15:00 20m Talk		A weakest pre-expectation semantics for mixed-sign expectations PPS Benjamin Lucien KaminskiRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University
15:20 10m Meeting		Discussion 6 PPS

14:00 - 15:30	Session IIIPLMW at Salle 107, Barre 44-54

14:00 60m Talk		Student Interaction Activity PLMW Eva DarulovaMPI-SWS, Loris D'AntoniUniversity of Wisconsin–Madison, Alexandra SilvaUniversity College London, Dimitrios VytiniotisMicrosoft Research, Cambridge
15:00 30m Talk		How to Give Talks That People Can Follow PLMW Derek DreyerMPI-SWS File Attached

14:00 - 15:30	Tutorial: Partial Evaluation for Language ImplementationPEPM at Salle 109, Barre 44-54 Chair(s): Jeremy YallopUniversity of Cambridge, UK

14:00 90m Talk		Practical Partial Evaluation for Language Implementation with Graal & Truffle PEPM Gilles Duboscq

15:30 - 16:00	Coffee breakCatering at Auditorium Hall

15:30 30m Coffee break		Break Catering

15:30 - 16:30	Poster Session PPS at Salle 105, Barre 44-54

15:30 60m Meeting		ProbLog and applicative probabilistic programming PPS Alexander VandenbrouckeKU Leuven, Belgium, Tom SchrijversKU Leuven
15:30 60m Meeting		Encapsulating models and approximate inference programs in probabilistic modules PPS Marco Cusumano-TownerMIT-CSAIL, Vikash MansinghkaMassachusetts Institute of Technology
15:30 60m Meeting		The extended semantics for probabilistic programming languages PPS Siddharth SrivastavaUTRC Berkeley, Nicholas HayVicarious, Yi WUUC Berkeley, Stuart RussellUniversity of California, Berkeley
15:30 60m Meeting		Synthetic topology in homotopy type theory for probabilistic programming PPS Florian Faissole, Bas Spitters
15:30 60m Meeting		Reasoning about inference in probabilistic programs PPS Chandrakana NandiUniversity of Washington, USA, Adrian SampsonCornell University, Dan GrossmanUniversity of Washington, Todd Mytkowicz, Kathryn S McKinleyMicrosoft Research
15:30 60m Meeting		On computable representations of exchangeable data PPS Nathanael L. AckermanHarvard University, Jeremy AvigadCarnegie Mellon University, Cameron FreerGamalon and Borelian, Daniel Roy, Jason M. RutePennsylvania State University
15:30 60m Meeting		Probabilistic logic programs: unifying program trace and possible world semantics PPS Angelika KimmigKU Leuven, Luc De RaedtKU Leuven
15:30 60m Meeting		Metropolis-Hastings for mixtures of conditional distributions PPS Oleg Kiselyov
15:30 60m Meeting		Support and influence analysis for visualizing posteriors of probabilistic programs PPS Long OuyangStanford University
15:30 60m Meeting		Efficient exact inference in discrete Anglican programs PPS Robert CornishUniversity of Oxford, Frank WoodUniversity of Oxford, Hongseok YangUniversity of Oxford

16:00 - 17:30	Concurrency 2VMCAI at Amphitheater 44 Chair(s): David MonniauxCNRS, VERIMAG

16:00 30m Talk		Using Abstract Interpretation to Correct Synchronization Faults VMCAI Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University
16:30 30m Talk		Detecting All High-Level Dataraces in an RTOS Kernel. VMCAI Suvam MukherjeeIndian Institute of Science, Arunkumar SIndian Institute of Science, Deepak D'Souza
17:00 30m Talk		Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions VMCAI Raphaël MonatEcole Normale Supérieure de Lyon, Antoine MinéUPMC, France

16:00 - 17:30	Formal verification of programming language foundationsCPP at Auditorium

16:00 30m Talk		Type-and-scope safe programs and their proofs CPP Guillaume AllaisRadboud University Nijmegen, James Chapman, Conor McBride, James McKinnaUniversity of Edinburgh
16:30 30m Talk		Formally verified differential dynamic logic CPP Brandon Bohrer, Vincent RahliSnT, Ivana Vukotic, Marcus Voelp, André Platzer
17:00 30m Talk		Equivalence of System F and λ2 in Coq based on context morphism lemmas CPP Jonas Kaiser, Tobias Tebbi, Gert SmolkaSaarland University

16:00 - 18:00	Session IVPLMW at Salle 107, Barre 44-54

16:00 30m Talk		Machine Learning and Programming Languages: latest directions and research opportunities PLMW Martin VechevETH Zurich File Attached
16:30 30m Talk		The Curse of Knowledge PLMW Benjamin C. PierceUniversity of Pennsylvania File Attached
17:00 60m Talk		Young Researcher Panel Session PLMW Roopsha SamantaPurdue University, Nada AminEPFL, Jonathan ProtzenkoMicrosoft Research, Zachary KincaidPrinceton University

16:00 - 17:00	Transformation (part II)PEPM at Salle 109, Barre 44-54 Chair(s): Jurriaan HageUtrecht University

16:00 30m Talk		Functional Parallels of Sequential Imperatives PEPM Tiark RompfPurdue University, Kevin J. BrownStanford University
16:30 30m Talk		A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction PEPM Kazutaka Matsuda, Kazuyuki AsadaUniversity of Tokyo

16:30 - 18:00	Session 5 PPS at Salle 105, Barre 44-54 Chair(s): Chung-chieh ShanIndiana University, USA

16:30 20m Talk		An exponential family basis for probabilistic programming PPS Chad ScherrerGalois, Inc.
16:50 10m Meeting		Discussion 7 PPS
17:00 20m Talk		The semantics of subroutines and iteration in the Bayesian programming language ProBT PPS Raphaël LaurentProbaYes, Kamel MekhnachaProbaYes, Emmanuel MazerCNRS/LIG, Pierre BessièreCNRS/ISIR
17:20 10m Meeting		Discussion 8 PPS
17:30 20m Talk		Exchangeable random process and data abstraction PPS Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, Nathanael L. AckermanHarvard University, Cameron FreerGamalon and Borelian, Daniel Roy
17:50 10m Meeting		Discussion 9 PPS

18:15 - 19:15	Session 6 PPS at Salle 105, Barre 44-54 Chair(s): Hongseok YangUniversity of Oxford

18:15 20m Talk		Reducing probabilistic choice to nondeterministic choice PPS Ernie CohenAmazon Web Services
18:35 10m Meeting		Discussion 10 PPS
18:45 20m Talk		GraPPa: spanning the expressivity vs. efficiency continuum PPS Edwin WestbrookGalois, Inc., Chad ScherrerGalois, Inc., Nathan CollinsGalois, Inc., Eric MertensGalois, Inc.
19:05 10m Meeting		Discussion 11 PPS

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05	OpeningPOPL at Auditorium Chair(s): Giuseppe CastagnaParis Diderot University & CNRS, Andrew D. GordonMicrosoft Research and University of Edinburgh

09:00 5m Day opening		Opening POPL

09:05 - 10:00	Invited speakerPOPL at Auditorium Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh

09:05 55m Talk		The Influence of Dependent Types POPL Stephanie WeirichUniversity of Pennsylvania

10:00 - 10:30	Coffee breakCatering at Auditorium Hall

10:00 30m Coffee break		Break Catering

10:30 - 12:10	Abstract InterpretationPOPL at Amphitheater 44 Chair(s): Isabella MastroeniUniversity of Verona, Italy

10:30 25m Talk		Ogre and Pythia, An invariance proof method for weak consistency models POPL Jade AlglaveUniversity College London, Patrick CousotNew York University
10:55 25m Talk		A Posteriori Environment Analysis with Pushdown Delta CFA POPL Kimball GermaneUniversity of Utah, Matthew MightUniversity of Utah; Harvard Medical School; The White House
11:20 25m Talk		Semantic-Directed Clumping of Disjunctive Abstract States POPL Huisong LiINRIA/CNRS/ENS/PSL, François BérengerINRIA/CNRS/ENS/PSL, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Xavier RivalINRIA/CNRS/ENS Paris
11:45 25m Talk		Fast Polyhedra Abstract Domain POPL Gagandeep SinghETH Zurich, Switzerland, Markus PüschelETH Zurich, Martin VechevETH Zurich

10:30 - 12:10	Type Systems 1POPL at Auditorium Chair(s): Avik ChaudhuriFacebook

10:30 25m Talk		Polymorphism, subtyping and type inference in MLsub POPL Stephen Dolan, Alan MycroftUniversity of Cambridge
10:55 25m Talk		Java generics are Turing complete POPL Radu GrigoreUniversity of Kent
11:20 25m Talk		Hazelnut: A Bidirectionally Typed Structure Editor Calculus POPL Cyrus OmarCarnegie Mellon University, Ian VoyseyCarnegie Mellon University, Michael HiltonOregon State University, USA, Jonathan AldrichCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder
11:45 25m Talk		Modules, Abstraction, and Parametric Polymorphism POPL Karl CraryCarnegie Mellon University

12:10 - 14:20	BuffetCatering at Catering area

12:10 2h10m Lunch		Lunch Catering

14:20 - 16:00	Probabilistic ProgrammingPOPL at Amphitheater 44 Chair(s): Marco GaboardiSUNY Buffalo, USA

14:20 25m Talk		Beginner's Luck: A Language for Property-Based Generators POPL Leonidas LampropoulosUniversity of Pennsylvania, Diane Gallois-WongInria Paris, ENS Paris, Cătălin HriţcuInria Paris, John HughesChalmers University of Technology, Benjamin C. PierceUniversity of Pennsylvania, Li-yao XiaENS Paris Pre-print
14:45 25m Talk		Exact Bayesian Inference by Symbolic Disintegration POPL Chung-chieh ShanIndiana University, USA, Norman Ramsey Pre-print
15:10 25m Talk		Stochastic Invariants for Probabilistic Termination POPL Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria, Djordje ZikelicUniversity of Cambridge
15:35 25m Talk		Coupling proofs are probabilistic product programs POPL Gilles BartheIMDEA, Benjamin GregoireINRIA, Justin Hsu, Pierre-Yves StrubÉcole Polytechnique

14:20 - 16:00	Concurrency 1POPL at Auditorium Chair(s): Ilya SergeyUniversity College London

14:20 25m Talk		A Promising Semantics for Relaxed-Memory Concurrency POPL Jeehoon KangSeoul National University, Chung-Kil HurSeoul National University, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS Link to publication Pre-print Media Attached
14:45 25m Talk		Automatically Comparing Memory Consistency Models POPL John WickersonImperial College London, Mark BattyUniversity of Kent, Tyler SorensenImperial College London, George A. ConstantinidesImperial College London, UK Pre-print Media Attached File Attached
15:10 25m Talk		Interactive Proofs in Higher-Order Concurrent Separation Logic POPL Robbert KrebbersDelft University of Technology, Netherlands, Amin Timanyimec - Distrinet, KU Leuven, Lars BirkedalAarhus University DOI Pre-print Media Attached
15:35 25m Talk		A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic POPL Morten Krogh-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University

16:00 - 16:30	Coffee breakCatering at Auditorium Hall

16:00 30m Coffee break		Break Catering

16:30 - 17:45	LogicPOPL at Amphitheater 44 Chair(s): Alexandra SilvaUniversity College London

16:30 25m Talk		Monadic second-order logic on finite sequences POPL Loris D'AntoniUniversity of Wisconsin–Madison, Margus VeanesMicrosoft Research
16:55 25m Talk		On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic POPL Naoki KobayashiUniversity of Tokyo, Japan, Etienne LozesENS Cachan, Florian BruseUniversity of Kassel
17:20 25m Talk		Coming to Terms with Quantified Reasoning POPL Simon RobillardChalmers University of Technology, Andrei VoronkovUniversity of Manchester, Laura KovacsChalmers University of Technology

16:30 - 17:45	Compiler OptimisationPOPL at Auditorium Chair(s): Andrew C. MyersCornell University

16:30 25m Talk		A Program Optimization for Automatic Database Result Caching POPL Ziv ScullyCarnegie Mellon University, Adam ChlipalaMIT
16:55 25m Talk		Stream Fusion, to Completeness POPL Oleg Kiselyov, Aggelos BiboudisUniversity of Athens, Nick PalladinosNessos Information Technologies, SA, Yannis SmaragdakisUniversity of Athens Pre-print Media Attached
17:20 25m Talk		Rigorous Floating-point Mixed Precision Tuning POPL Wei-Fan ChiangSchool of Computing, University of Utah, Ganesh GopalakrishnanUniversity of Utah, Zvonimir RakamaricUniversity of Utah, Ian BriggsSchool of Computing, University of Utah, Marek S. BaranowskiUniversity of Utah, Alexey SolovyevSchool of Computing, University of Utah Pre-print

19:30 - 23:00	Social dinnerCatering at Musée des Arts Forains

19:30 3h30m Dinner		Social dinner Catering

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:15	ACM and SIGPLAN AwardsPOPL at Auditorium Chair(s): Satnam SinghFacebook

09:00 5m Awards		Turing Award Video POPL
09:05 5m Awards		Most Influential Paper Award POPL
09:10 5m Awards		Reynolds Doctoral Dissertation Award POPL

09:15 - 10:00	Invited speakerPOPL at Auditorium Chair(s): Roberto GiacobazziUniversity of Verona, Italy

09:15 45m Talk		40 Years of Abstract Interpretation — An Interview with Patrick Cousot POPL Patrick CousotNew York University, Roberto GiacobazziUniversity of Verona, Italy

10:00 - 10:30	Coffee breakCatering at Auditorium Hall

10:00 30m Coffee break		Break Catering

10:30 - 12:10	Program AnalysisPOPL at Amphitheater 44 Chair(s): Francesco LogozzoFacebook

10:30 25m Talk		Relational Cost Analysis POPL Ezgi ÇiçekMPI-SWS, Germany, Gilles BartheIMDEA, Marco GaboardiSUNY Buffalo, USA, Deepak GargMPI-SWS, Germany, Jan HoffmannCarnegie Mellon University
10:55 25m Talk		Contract-based Resource Verification for Higher-order Functions with Memoization POPL Ravichandhran MadhavanEPFL, Sumith KulalIIT Bombay, Viktor KunčakEPFL, Switzerland
11:20 25m Talk		Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability POPL Qirun ZhangUniversity of California, Davis, Zhendong SuUniversity of California, Davis
11:45 25m Talk		Towards Automatic Resource Bound Analysis for OCaml POPL Jan HoffmannCarnegie Mellon University, Ankush DasCarnegie Mellon University, Shu-chun WengYale University

10:30 - 12:10	Type Systems 2POPL at Auditorium Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh

10:30 25m Talk		Deciding equivalence with sums and the empty type POPL Gabriel SchererNortheastern University
10:55 25m Talk		The exp-log normal form of types: Decomposing extensional equality and representing terms compactly POPL Danko IlikTrusted Labs
11:20 25m Talk		Contextual isomorphisms POPL Paul Blain Levy
11:45 25m Talk		Typed Self-Evaluation via Intensional Type Functions POPL Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles

12:10 - 14:20	BuffetCatering at Catering area

12:10 2h10m Lunch		Lunch Catering

14:20 - 16:00	Concurrency 2POPL at Amphitheater 44 Chair(s): Nobuko YoshidaImperial College London, UK

14:20 25m Talk		Mixed-size Concurrency: ARM, POWER, C/C++11, and SC POPL Shaked FlurUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, UK, Christopher PulteUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Luc MarangetINRIA Rocquencourt, Kathryn E. GrayUniversity of Cambridge, Ali SezginUniversity of Cambridge, Mark BattyUniversity of Kent, Peter SewellUniversity of Cambridge
14:45 25m Talk		Dynamic Race Detection For C++11 POPL Christopher LidburyImperial College London, Alastair DonaldsonImperial College London
15:10 25m Talk		Serializability for Eventual Consistency: Criterion, Analysis and Applications POPL Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zurich Pre-print
15:35 25m Talk		Thread Modularity at Many Levels: a Pearl in Compositional Verification POPL Jochen HoenickeUniversität Freiburg, Rupak MajumdarMPI-SWS, Andreas PodelskiUniversity of Freiburg, Germany

14:20 - 16:00	Functional Programming with EffectsPOPL at Auditorium Chair(s): Kathleen FisherTufts University

14:20 25m Talk		Type Directed Compilation of Row-Typed Algebraic Effects POPL Daan LeijenMicrosoft Research
14:45 25m Talk		Do be do be do POPL Sam LindleyUniversity of Edinburgh, Conor McBride, Craig McLaughlinThe University of Edinburgh
15:10 25m Talk		Dijkstra Monads for Free POPL Danel AhmanUniversity of Edinburgh, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris, ENS Paris, and Microsoft Research, Guido MartínezCIFASIS-CONICET, Argentina, Gordon Plotkin, Jonathan ProtzenkoMicrosoft Research, Aseem RastogiMicrosoft Research India, Nikhil SwamyMicrosoft Research Pre-print
15:35 25m Talk		Stateful Manifest Contracts POPL Taro Sekiyama, Atsushi IgarashiKyoto University

16:00 - 16:30	Coffee breakCatering at Auditorium Hall

16:00 30m Coffee break		Break Catering

16:30 - 17:20	Semantic FoundationsPOPL at Amphitheater 44 Chair(s): Lars BirkedalAarhus University

16:30 25m Talk		A Semantic Account of Metric Preservation POPL Arthur Azevedo de AmorimUniversity of Pennsylvania, USA, Ikram CheriguiENS Paris, Marco GaboardiSUNY Buffalo, USA, Justin Hsu, Shin-ya KatsumataKyoto University
16:55 25m Talk		Cantor Meets Scott: Semantic Foundations for Probabilistic Networks POPL Steffen SmolkaCornell University, Praveen KumarCornell University, Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London DOI File Attached

16:30 - 17:20	Logic and ProgrammingPOPL at Auditorium Chair(s): Nada AminEPFL

16:30 25m Talk		Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks POPL Kausik SubramanianUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison, Aditya AkellaUniversity of Wisconsin-Madison
16:55 25m Talk		LOIS: syntax and semantics POPL Eryk Kopczynski, Szymon Toruńczyk

17:20 - 18:20	Business meetingPOPL at Auditorium Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh

17:20 20m Talk		PC Chair report POPL Andrew D. GordonMicrosoft Research and University of Edinburgh
17:40 10m Talk		POPL 2018 presentation POPL Andrew C. MyersCornell University, Ranjit JhalaUniversity of California, San Diego
17:50 30m Meeting		SIGPLAN business meeting POPL C: Andrew D. GordonMicrosoft Research and University of Edinburgh

18:20 - 20:20	Poster SessionStudent Research Competition at Auditorium Hall Chair(s): Qirun ZhangUniversity of California, Davis, Matteo CiminiIndiana University, USA, Julien SignolesCEA LIST, Kim NguyễnLRI, Université Paris-Sud

18:20 10m Demonstration		Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism Student Research Competition Nicholas RiouxNortheastern University
18:30 10m Demonstration		Gradual Type Precision as Retraction Student Research Competition Max NewNortheastern University
18:40 10m Demonstration		Linking Types: Specifying Safe Interoperability and Equivalences Student Research Competition Daniel PattersonNortheastern University
18:50 10m Demonstration		A Monadic Framework for Bidirectional Programming Student Research Competition Li-yao XiaENS Paris
19:00 10m Demonstration		Gradual Set-Theoretic Types Student Research Competition Victor LanvinENS Paris-Saclay
19:10 10m Demonstration		Abstract Interpretation of High-Level Transformations Student Research Competition Ahmad Salim Al-SibahiIT University of Copenhagen, Denmark
19:20 10m Demonstration		FairSquare: A Static Analysis Tool for Algorithmic Fairness Student Research Competition Samuel DrewsUniversity of Wisconsin-Madison
19:30 10m Demonstration		Toward Type-Preserving Compilation of Coq Student Research Competition William J. BowmanNortheastern University
19:40 10m Demonstration		A Symbolic Execution Framework for Haskell Student Research Competition Anton XueYale University
19:50 10m Demonstration		Synthesizing Imperative Programs from Examples for Introductory Programming Assignments Student Research Competition Sunbeom SoKorea University
20:00 10m Demonstration		Provenance for Configuration Language Security Student Research Competition Weili FuUniversity of Edinburgh
20:10 10m Demonstration		A gradually typed polymorphic lambda calculus Student Research Competition Yuu IgarashiKyoto University

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05	Student Competition AwardStudent Research Competition at Auditorium Chair(s): Kim NguyễnLRI, Université Paris-Sud

09:00 5m Awards		Student Competition Award Student Research Competition

09:05 - 10:00	Invited speakerPOPL at Auditorium Chair(s): Giuseppe CastagnaParis Diderot University & CNRS

09:05 55m Talk		Rust: from POPL to practice POPL Aaron TuronMPI-SWS

10:00 - 10:30	Coffee breakCatering at Auditorium Hall

10:00 30m Coffee break		Break Catering

10:30 - 12:10	Verification and SynthesisPOPL at Amphitheater 44 Chair(s): Benjamin DelawarePurdue University

10:30 25m Talk		Component-Based Synthesis for Complex APIs POPL Yu FengUniversity of Texas at Austin, USA, Ruben Martins, Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.
10:55 25m Talk		Learning nominal automata POPL Joshua MoermanRadboud University, Matteo SammartinoUniversity College London, Alexandra SilvaUniversity College London, Bartek KlinUniversity of Warsaw, Michał SzynwelskiUniversity of Warsaw
11:20 25m Talk		On Verifying Causal Consistency POPL Ahmed BouajjaniIRIF, Université Paris Diderot, Constantin EneaLIAFA, Université Paris Diderot, Rachid Guerraoui, Jad HamzaLIAFA, Université Paris Diderot
11:45 25m Talk		Complexity Verification Using Guided Theorem Enumeration POPL Akhilesh SrikanthGeorgia Institute of Technology, Burak SahinGeorgia Institute of Technology, William Harris

10:30 - 12:10	Type Systems 3POPL at Auditorium Chair(s): Derek DreyerMPI-SWS

10:30 25m Talk		Intersection Type Calculi of Bounded Dimension POPL Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
10:55 25m Talk		Type Soundness Proofs with Definitional Interpreters POPL Nada AminEPFL, Tiark RompfPurdue University
11:20 25m Talk		Computational Higher-Dimensional Type Theory POPL Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno
11:45 25m Talk		Type Systems as Macros POPL Stephen ChangNortheastern University, Alex KnauthNortheastern University, Ben GreenmanNortheastern University

12:10 - 14:20	BuffetCatering at Catering area

12:10 2h10m Lunch		Lunch Catering

14:20 - 16:00	Concurrency 3POPL at Amphitheater 44 Chair(s): Adam ChlipalaMIT

14:20 25m Talk		Parallel Functional Arrays POPL Ananya Kumar, Guy E. BlellochCarnegie Mellon University, Robert Harper
14:45 25m Talk		A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms POPL Igor KonnovTU Wien, Marijana LazićTU Wien, Helmut VeithTU Wien, Josef WidderTU Wien DOI Pre-print
15:10 25m Talk		Analyzing divergence in bisimulation semantics POPL Xinxin LiuInstitute of software, Chinese academy of sciences, Tingting Yu, Wenhui ZhangInstitute of software, Chinese academy of sciences
15:35 25m Talk		Fencing off Go: Liveness and Safety for Channel-Based Programming POPL Julien LangeImperial College London, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London, UK Pre-print

14:20 - 16:00	Gradual Typing and ContractsPOPL at Auditorium Chair(s): Ronald GarciaUniversity of British Columbia

14:20 25m Talk		Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL Michael Vitousek, Cameron SwordsIndiana University, Jeremy G. SiekIndiana University Bloomington
14:45 25m Talk		Gradual Refinement Types POPL Nicolás Lehmann, Éric TanterUniversity of Chile, Chile Link to publication DOI Pre-print
15:10 25m Talk		Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL Matteo CiminiIndiana University, USA, Jeremy G. SiekIndiana University Bloomington
15:35 25m Talk		Sums of Uncertainty: Refinements go gradual POPL Khurram A. JaferyUniversity of British Columbia, Jana DunfieldUniversity of British Columbia

16:00 - 16:30	Coffee breakCatering at Auditorium Hall

16:00 30m Coffee break		Break Catering

16:30 - 17:45	QuantumPOPL at Amphitheater 44 Chair(s): Michele PaganiIRIF, Université Paris Diderot

16:30 25m Talk		Invariants of Quantum Programs: Characterisations and Generation POPL Mingsheng YingUniversity of Technology Sydney, Australia, Shenggang YingUniversity of Technology Sydney, Australia, Xiaodi WuUniversity of Oregon, USA
16:55 25m Talk		The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects POPL Ugo Dal LagoUniversity of Bologna, France, Claudia Faggian, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay, Akira YoshimizuUniv.Tokyo
17:20 25m Talk		QWIRE: A Core Language for Quantum Circuits POPL Jennifer Paykin, Robert RandUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania

16:30 - 17:45	Security and PrivacyPOPL at Auditorium Chair(s): Cătălin HriţcuInria Paris

16:30 25m Talk		LMS-Verify: Abstraction Without Regret for Verified Systems Programming POPL Nada AminEPFL, Tiark RompfPurdue University
16:55 25m Talk		Hypercollecting Semantics and its Application to Static Analysis of Information Flow POPL Mounir AssafStevens Institute of Technology, David NaumannStevens Institute of Technology, Julien SignolesCEA LIST, Éric TotelCentraleSupélec, Frédéric TronelCentraleSupélec
17:20 25m Talk		LightDP: Towards Automating Differential Privacy Proofs POPL Danfeng ZhangPennsylvania State University, Daniel KiferDept. of Computer Science and Engineering, Penn State University

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:45 - 09:00	OpeningN40AI at Amphitheater 44 Chair(s): Roberto GiacobazziUniversity of Verona, Italy

08:45 15m Day opening		Opening N40AI

08:55 - 09:00	WelcomePiP at Salle 105, Barre 44-54

08:55 5m Talk		Welcome PiP

09:00 - 10:00	Industrial Panel 1N40AI at Amphitheater 44 Chair(s): Antoine MinéUPMC, France

09:00 30m Talk		Abstract Interpretation in Absint N40AI Christian FerdinandAbsInt
09:30 30m Talk		Abstract Interpretation in Facebook N40AI Francesco LogozzoFacebook

09:00 - 10:00	Opening SessionCoqPL at Auditorium Chair(s): Emilio Jesús Gallego AriasMINES ParisTech

09:00 60m Talk		Invited Talk -- Demonstration of the Iris separation logic in Coq CoqPL I: Robbert KrebbersDelft University of Technology, Netherlands

09:00 - 10:00	Session 1PiP at Salle 105, Barre 44-54

09:00 30m Talk		Andrew Kennedy (Facebook) Static type checking for PHP PiP
09:30 30m Talk		Jean-Louis Colaco (Ansys - Esterel Technologies) A brief history of the Scade language PiP

09:00 - 10:00	Session IRDP at Salle 107, Barre 44-54 Chair(s): Victor VianuUC San Diego

09:00 15m Talk		Welcome RDP Nate FosterCornell University, Mooly SagivTel Aviv University, Victor VianuUC San Diego
09:15 45m Talk		Automatic Verification of Database-Centric Workflows RDP Alin Deutsch

09:00 - 10:00	Session OneOff the Beaten Track at Salle 109, Barre 44-54

09:00 60m Talk		Keynote talk: Reasoning about Functional Programs: Exploring, Testing and Inductive Proofs. Off the Beaten Track Moa JohanssonChalmers University of Technology

10:00 - 10:30	Coffee breakCatering at Auditorium Hall

10:00 30m Coffee break		Break Catering

10:30 - 12:00	Industrial Panel 2 & Systems BiologyN40AI at Amphitheater 44 Chair(s): Jerome FeretINRIA Paris

10:30 30m Talk		Abstract Interpretation in Amazon N40AI Byron CookAmazon
11:00 30m Talk		Abstract Interpretation at Galois N40AI Aaron TombGalois, Inc.
11:30 30m Talk		Systems biology N40AI Vincent DanosENS Paris/CNRS

10:30 - 12:10	Morning SessionCoqPL at Auditorium Chair(s): Alan SchmittInria

10:30 25m Talk		IxFree: Step-Indexed Logical Relations in Coq CoqPL Piotr Polesiuk File Attached
10:55 25m Talk		Logical Relations in Iris CoqPL Amin Timanyimec - Distrinet, KU Leuven, Robbert KrebbersDelft University of Technology, Netherlands, Lars BirkedalAarhus University File Attached
11:20 25m Talk		Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting CoqPL Edwin WestbrookGalois, Inc., Gregory MalechaUCSD File Attached
11:45 25m Talk		ppsimpl: a reflexive Coq tactic for canonising goals CoqPL Frédéric Besson File Attached

10:30 - 12:05	Session 2PiP at Salle 105, Barre 44-54

10:30 5m Talk		Peter Sewell (Cambridge) REMS Short Introduction PiP
10:35 30m Talk		Simon Moore (Cambridge) Experiences of Formal Modelling in the CHERI Computer Architecture Research Project PiP
11:05 30m Talk		Stephen Kell/Dominic Mulligan (Cambridge) ELF linking: what it means and why it matters PiP
11:35 30m Talk		Philippa Gardner (Imperial) An Infrastructure for Tractable Verification of JavaScript Programs PiP

10:30 - 12:00	Session IIRDP at Salle 107, Barre 44-54 Chair(s): Mooly SagivTel Aviv University

10:30 30m Talk		Verification Challenges in Applications of Blockchain for Business Collaboration RDP Takaaki TateishiIBM Research - Tokyo
11:00 30m Talk		Fiat: A New Take on Domain-Specific Languages by Programming with Specifications RDP Adam ChlipalaMIT
11:30 30m Talk		Parallel-Correctness and Transferability for Conjunctive Queries RDP Frank Neven

10:30 - 12:10	Session TwoOff the Beaten Track at Salle 109, Barre 44-54

10:30 25m Talk		Can we machine-learn programming language semantics? Off the Beaten Track Dan GhicaUniversity of Birmingham, Khulood Alyahya, Victor Patentasu File Attached
10:55 25m Talk		How Far Apart Should Those Programs Be? Off the Beaten Track Ugo Dal LagoUniversity of Bologna, France File Attached
11:20 25m Talk		Programming Quantum Annealers Off the Beaten Track George Stelle, Scott Pakin File Attached
11:45 25m Talk		Understanding the POSIX Shell as a Programming Language Off the Beaten Track Michael GreenbergPomona College File Attached

12:00 - 14:00	BuffetCatering at Catering area

12:00 2h Lunch		Lunch Catering

14:00 - 15:30	Security, Big Code and Synthesis N40AI at Amphitheater 44 Chair(s): Xavier RivalINRIA/CNRS/ENS Paris

14:00 30m Talk		Security N40AI Michael HicksUniversity of Maryland at College Park, USA
14:30 30m Talk		Big Code N40AI Bor-Yuh Evan ChangUniversity of Colorado Boulder
15:00 30m Talk		Program synthesis N40AI Eran YahavTechnion

14:00 - 15:30	Midday SessionCoqPL at Auditorium Chair(s): Sandrine BlazyUniversity of Rennes 1, France

14:00 60m Talk		Invited Talk -- Managing Logical and Computational Complexity using Program Transformations CoqPL I: Nicolas TabareauInria, France
15:00 30m Demonstration		Session with the Coq Development Team CoqPL Matthieu SozeauInria

14:00 - 15:30	Session 3PiP at Salle 105, Barre 44-54

14:00 30m Talk		John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck PiP
14:30 30m Talk		Byron Cook (Amazon) Automated Reasoning about AWS PiP
15:00 30m Talk		Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM PiP

14:00 - 15:30	Session IIIRDP at Salle 107, Barre 44-54 Chair(s): Nate FosterCornell University

14:00 45m Talk		Synthesizing Data-parallel Programs RDP Aws AlbarghouthiUniversity of Wisconsin - Madison
14:45 45m Talk		Cosette: A Solver for SQL Equivalences RDP Alvin CheungUniversity of Washington

14:00 - 15:25	Session ThreeOff the Beaten Track at Salle 109, Barre 44-54

14:00 60m Talk		Keynote talk: Varieties of Programming Experience Off the Beaten Track Alan BlackwellUniversity of Cambridge
15:00 25m Talk		Bootstrapping the next generation of mathematical social machines Off the Beaten Track Ursula Martin, Alison Pease, Joe Corneli File Attached

15:30 - 16:00	Coffee breakCatering at Auditorium Hall

15:30 30m Coffee break		Break Catering

16:00 - 18:30	System Verification and Patrick Cousot's KeynoteN40AI at Amphitheater 44 Chair(s): Francesco RanzatoUniversity of Padova

16:00 30m Talk		System verification N40AI Arie GurfinkelUniversity of Waterloo
16:30 75m Talk		Keynote: the Next 40 years of Abstract Interpretation N40AI Patrick CousotNew York University
17:45 45m Social Event		Concrete Cheese and Wine N40AI

16:00 - 18:05	Afternoon SessionCoqPL at Auditorium Chair(s): Matthieu SozeauInria

16:00 25m Talk		Synthetic topology in HoTT for probabilistic programming CoqPL Florian Faissole, Bas Spitters File Attached
16:25 25m Talk		CertiCoq: A verified compiler for Coq CoqPL Abhishek Anand, Andrew AppelPrinceton, Greg MorrisettCornell University, Zoe ParaskevopoulouPrinceton University, USA, Randy PollackHarvard University, Olivier Savary BelangerPrinceton University, Matthieu SozeauInria, Matthew WeaverPrinceton University File Attached
16:50 25m Talk		CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL CoqPL Izumi AsakuraTokyo Institute of Technology, Japan, Hidehiko MasuharaTokyo Institute of Technology, Tomoyuki AotaniTokyo Institute of Technology File Attached
17:15 25m Talk		Verification of Implementations of Distributed Systems Under Churn CoqPL Ryan DoengesUniversity of Washington, James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Karl Palmskog File Attached
17:40 25m Talk		Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations CoqPL Nicolas Magaud File Attached

16:00 - 18:00	Session 4PiP at Salle 105, Barre 44-54

16:00 30m Talk		Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models PiP
16:30 60m Talk		Discussion: Methods and Tools for large-scale semantics PiP

16:00 - 18:00	Session IVRDP at Salle 107, Barre 44-54 Chair(s): Victor VianuUC San Diego

16:00 30m Talk		Building performance-sensitive systems in high-level languages RDP Christoph E. Koch
16:30 30m Talk		Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data RDP Kathleen FisherTufts University
17:00 30m Talk		Computation with Atoms RDP Szymon Toruńczyk
17:30 30m Talk		Discussion RDP Nate FosterCornell University, Victor VianuUC San Diego, Mooly SagivTel Aviv University

16:00 - 18:05	Session FourOff the Beaten Track at Salle 109, Barre 44-54

16:00 25m Talk		Designing extensible, domain-specific languages for mathematical diagrams Off the Beaten Track Katherine Ye, Keenan Crane, Jonathan AldrichCarnegie Mellon University, Joshua SunshineCarnegie Mellon University File Attached
16:25 25m Talk		Laziness Boxes You In Off the Beaten Track Jose CalderonGalois, Inc., Stephen Magill File Attached
16:50 25m Talk		Programming with Epistemic Logic Off the Beaten Track Markus Eger, Chris MartensCarnegie Mellon University File Attached
17:15 25m Talk		Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach Off the Beaten Track Marco GaboardiSUNY Buffalo, USA File Attached
17:40 25m Talk		Running Incomplete Programs Off the Beaten Track Ian VoyseyCarnegie Mellon University, Cyrus OmarCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder File Attached

19:00 - 21:00	Social EventCoqPL at CoqPL-social-event-room

19:00 2h Social Event		CoqPL Social Event CoqPL

Sun 15 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44				VMCAI Invited talk 1				VMCAI Program Analysis							VMCAI Concurrency 1				VMCAI Decision procedures
Catering area							Catering Coffee break				Catering Buffet							Catering Coffee break
Salle 105, Barre 44-54			TTT First Morning Session					TTT Second Morning Session							TTT First Afternoon Session				TTT Second Afternoon Session
Salle 109, Barre 44-54					SCM Session I			SCM Session II							SCM Session III				SCM Session IV

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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	21:00	30
Amphitheater 44				VMCAI Invited talk 2			VMCAI Numerical domains								VMCAI Model-checking and bug finding				VMCAI Symbolic analysis and invariant synthesis
Auditorium				CPP Invited Talk			CPP Algorithm and library verification								CPP Automated proof and its verification				CPP Formalized mathematics with numerical computations
Auditorium Hall						Catering Coffee break												Catering Coffee break
Catering area										Catering Buffet
Procope													VMCAI Banquet
Salle 105, Barre 44-54				Tutorials Gradual Typing (AM)											Tutorials Gradual Typing (PM)
Salle 107, Barre 44-54				Tutorials Lean (AM)											Tutorials Lean (PM)
Salle 109, Barre 44-54				PEPM Keynote			PEPM Programming languages								PEPM Tutorial (Idris, Inside-Out) and Poster Session				PEPM Transformation (part I)
Salle 112, Barre 44-54				Tutorials Flow (AM)											Tutorials Flow (PM)
Salle 114, Barre 44-54				Tutorials Frama-C (AM)											Tutorials Frama-C (PM)
Salle 116, Barre 44-54			PADL Opening remarks	PADL Invited Talk			PADL Answer Set Programming								PADL Testing and Games				PADL Applications I and Inference

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44				VMCAI Invited talk 3			VMCAI Model Checking and Synthesis							VMCAI Abstract Interpretation				VMCAI Concurrency 2
Auditorium				CPP Invited Talk			CPP Verified programming tools							CPP Homotopy type theory				CPP Formal verification of programming language foundations
Auditorium Hall						Catering Coffee break											Catering Coffee break
Catering area										Catering Buffet
Salle 105, Barre 44-54				PPS Session 1			PPS Session 2							PPS Session 3			PPS Poster Session		PPS Session 5				PPS Session 6
Salle 107, Barre 44-54			PLMW Welcome Session	PLMW Session I			PLMW Session II							PLMW Session III				PLMW Session IV
Salle 109, Barre 44-54				PEPM Tutorial: reversible computing			PEPM Types							PEPM Tutorial: Partial Evaluation for Language Implementation				PEPM Transformation (part II)
Salle 116, Barre 44-54				PADL Applications II			PADL Programming Languages

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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	22:00	30
Amphitheater 44					POPL Abstract Interpretation									POPL Probabilistic Programming					POPL Logic
Auditorium	POPL Opening	POPL Invited speaker			POPL Type Systems 1									POPL Concurrency 1					POPL Compiler Optimisation
Auditorium Hall				Catering Coffee break														Catering Coffee break
Catering area									Catering Buffet
Musée des Arts Forains														Catering Social dinner

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44					POPL Program Analysis									POPL Concurrency 2					POPL Semantic Foundations
Auditorium	POPL ACM and SIGPLAN Awards	POPL Invited speaker			POPL Type Systems 2									POPL Functional Programming with Effects					POPL Logic and Programming		POPL Business meeting
Auditorium Hall				Catering Coffee break														Catering Coffee break						Student Research Competition Poster Session
Catering area									Catering Buffet

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44					POPL Verification and Synthesis									POPL Concurrency 3					POPL Quantum
Auditorium	Student Research Competition Student Competition Award	POPL Invited speaker			POPL Type Systems 3									POPL Gradual Typing and Contracts					POPL Security and Privacy
Auditorium Hall				Catering Coffee break														Catering Coffee break
Catering area									Catering Buffet

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44			N40AI Opening		N40AI Industrial Panel 1			N40AI Industrial Panel 2 & Systems Biology								N40AI Security, Big Code and Synthesis				N40AI System Verification and Patrick Cousot's Keynote
Auditorium					CoqPL Opening Session			CoqPL Morning Session								CoqPL Midday Session				CoqPL Afternoon Session
Auditorium Hall							Catering Coffee break												Catering Coffee break
Catering area											Catering Buffet
CoqPL-social-event-room														CoqPL Social Event
Salle 105, Barre 44-54				PiP Welcome	PiP Session 1			PiP Session 2								PiP Session 3				PiP Session 4
Salle 107, Barre 44-54					RDP Session I			RDP Session II								RDP Session III				RDP Session IV
Salle 109, Barre 44-54					Off the Beaten Track Session One			Off the Beaten Track Session Two								Off the Beaten Track Session Three				Off the Beaten Track Session Four

Sun 15 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44						VMCAI Detecting Strict Aliasing Violations in the Wild 09:00 - 10:00								VMCAI Partitioned Memory Models for Program Analysis. 10:30 - 11:00				VMCAI Property Directed Reachability for Proving Absence of Concurrent Modifi ... 11:00 - 11:30			VMCAI Stabilizing Floating-Point Programs using Provenance Analysis 11:30 - 12:00											VMCAI Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed ... 14:00 - 14:30		VMCAI Independence Abstractions and Models of Concurrency 14:30 - 15:00			VMCAI Static Analysis of Communicating Process using Symbolic Transducers 15:00 - 15:30					VMCAI Synthesising Strategy Improvement and Recursive Algorithms for Solving ... 16:00 - 16:30		VMCAI Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic 16:30 - 17:00			VMCAI Matching multiplications in Bit-Vector formulas 17:00 - 17:30
Catering area												POPL Catering Break 10:00 - 10:30												POPL Catering Lunch 12:00 - 14:00																POPL Catering Break 15:30 - 16:00
Salle 105, Barre 44-54					TTT Welcome 08:50 - 09:00	TTT A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method 09:00 - 09:20		TTT Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding 09:20 - 09:40		TTT Equivalence of System F and λ2 in Abella 09:40 - 10:00				TTT Invited Talk -- Type Theory in the Software Analysis Workbench 10:30 - 11:20						TTT Modelling Program Behaviour within Software Verification Tool LAV 11:20 - 11:40		TTT agdARGS - Declarative Hierarchical Command Line Interfaces 11:40 - 12:00										TTT Invited Talk -- Cubical Type Theory: a constructive interpretation of t ... 14:00 - 14:50				TTT Equations: a tool for dependent pattern-matching 14:50 - 15:10		TTT Coq's Prolog and application to defining semi-automatic tactics 15:10 - 15:30				TTT Invited Talk -- Iris: a framework for higher-order concurrent separatio ... 16:00 - 16:50				TTT Introducing MetaCoq: A Safe Tactic Language for Coq 16:50 - 17:10		TTT COST EUTypes session 17:10 - 18:00
Salle 109, Barre 44-54							SCM What is Secure Compilation? Part I 09:15 - 10:00							SCM What is Secure Compilation? Part II (Short talk) 10:30 - 10:40	SCM Can relational logic facilitate secure compilation? (Short talk) 10:40 - 10:50		SCM Full Abstraction for Language Design (Short talk) 10:50 - 11:00	SCM Cogent: Where we Stand and What Comes Next (Short talk) 11:00 - 11:10	SCM Enforcing Well-Bracketed Control Flow on a Capability Machine using Loc ... 11:15 - 12:00													SCM Linking Types: Secure compilation of multi-language programs 14:00 - 14:45			SCM Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing 14:45 - 15:30							SCM Software Fault Isolation avec CompCert 16:00 - 16:45			SCM Security preserving compilation of low-level programs embedded in F* 16:45 - 17:30

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44						VMCAI Verified Concurrent Code: Tricks of the Trade 09:00 - 10:00						VMCAI Sound Bit-Precise Numerical Domains 10:30 - 11:00		VMCAI Efficient Elimination of Redundancies in Polyhedra using Raytracing 11:00 - 11:30		VMCAI Finding Relevant Templates via the Principal Component Analysis 11:30 - 12:00										VMCAI Effective Bug Finding in C Programs with Shape and Effect Abstraction 14:00 - 14:30		VMCAI Reduction of Workflow Nets for Generalised Soundness Verification 14:30 - 15:00		VMCAI Dynamic Reductions for Model Checking Concurrent Software. 15:00 - 15:30				VMCAI Block-wise abstract interpretation by combining abstract domains with SMT 16:00 - 16:30		VMCAI IC3 - Flipping the E in ICE 16:30 - 17:00		VMCAI Counterexample Validation and Interpolation-Based Refinement for Forest ... 17:00 - 17:30
Auditorium						CPP Porting the HOL Light Analysis Library: Some Lessons 09:00 - 10:00						CPP Verifying a hash table and its iterators in higher-order separation logic 10:30 - 11:00		CPP A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm 11:00 - 11:30		CPP Formal foundations of 3D geometry for modeling robot manipulators 11:30 - 12:00										CPP BliStrTune: Hierarchical Invention of Theorem Proving Strategies 14:00 - 14:30		CPP Automatic Cyclic Termination Proofs for Recursive Procedures in Separat ... 14:30 - 15:00		CPP Formalization of Karp-Miller Tree Construction on Petri Nets 15:00 - 15:30				CPP A Coq Formal Proof of the Lax–Milgram theorem 16:00 - 16:30		CPP A Reflexive Tactic for Polynomial Positivity using Numerical Solvers an ... 16:30 - 17:00		CPP Markov Processes in Isabelle/HOL 17:00 - 17:30		CPP Formalising Real Numbers in Homotopy Type Theory 17:30 - 18:00
Auditorium Hall										POPL Catering Break 10:00 - 10:30																						POPL Catering Break 15:30 - 16:00
Catering area																		POPL Catering Lunch 12:00 - 14:00
Salle 105, Barre 44-54						POPL Tutorials The State of the Art in Gradual Typing 09:00 - 12:00																				POPL Tutorials The State of the Art in Gradual Typing 14:00 - 17:00
Salle 107, Barre 44-54						POPL Tutorials The Lean Theorem Prover 09:00 - 12:00																				POPL Tutorials The Lean Theorem Prover 14:00 - 17:00
Salle 109, Barre 44-54						PEPM Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics ... 09:00 - 10:00						PEPM Lightweight Soundness for Towers of Language Extensions 10:30 - 11:00		PEPM Detecting code clones with gaps by function applications 11:00 - 11:30		PEPMBest Paper PEG Parsing in Less Space Using Progressive Tabling and Dynamic Analysis 11:30 - 12:00										PEPM Idris, Inside-Out: A Tutorial on Extending Idris in Idris 14:00 - 15:00				PEPM Invited posters 15:00 - 15:30 Language-integrated Query with Ordering, Grouping and Outer Joins (poster) 15:00 - 15:30				PEPM Verification of Code Generators via Higher-Order Model Checking 16:00 - 16:30		PEPM Interactive data representation migration: Exploiting program dependenc ... 16:30 - 17:00
Salle 112, Barre 44-54						POPL Tutorials Fast and Precise Type Checking for JavaScript: Are you in Flow? 09:00 - 12:00																				POPL Tutorials Fast and Precise Type Checking for JavaScript: Are you in Flow? 14:00 - 17:00
Salle 114, Barre 44-54						POPL Tutorials Let's Implement Your New Analysis using Industrially Strengthened Frama ... 09:00 - 12:00																				POPL Tutorials Let's Implement Your New Analysis using Industrially Strengthened Frama ... 14:00 - 17:00
Salle 116, Barre 44-54					PADL Opening remarks 08:50 - 09:00	PADL Proof checking and logic programming 09:00 - 10:00						PADL Lowering the learning curve for declarative programming: a Python API f ... 10:30 - 11:00		PADL Extending Answer Set Programs with Interpreted Functions as First-class ... 11:00 - 11:30		PADL Integrating Answer Set Programming with Object-oriented Languages 11:30 - 12:00										PADL Failing Faster: Overlapping Patterns for Property-Based Testing 14:00 - 14:30		PADL Boltzmann Samplers for Closed Simply-Typed Lambda Terms 14:30 - 15:00		PADL Selection Equilibria of Higher-Order Games 15:00 - 15:30				PADL A Domain-Specific Language for Software-Defined Radio 16:00 - 16:30		PADL A Declarative DSL for Customized Rendering of Text-Based Art 16:30 - 17:00		PADL Using Iterative Deepening for Probabilistic Logic Inference 17:00 - 17:30

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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		18:00	15	30		45	19:00		15	30	45
Amphitheater 44						VMCAI Verification of Cancer Programs 09:00 - 10:00						VMCAI Reachability for dynamic parametric processes 10:30 - 11:00			VMCAI Synthesizing Non-Vacuous Systems 11:00 - 11:30			VMCAI Solving Nonlinear Integer Arithmetic with MCSat 11:30 - 12:00											VMCAI Complete Abstractions and Subclassical Modal Logics 14:00 - 14:30			VMCAI Structuring Abstract Interpreters through State and Value Abstractions 14:30 - 15:00			VMCAI Conjunctive Abstract Interpretation using Paramodulation 15:00 - 15:30					VMCAI Using Abstract Interpretation to Correct Synchronization Faults 16:00 - 16:30		VMCAI Detecting All High-Level Dataraces in an RTOS Kernel. 16:30 - 17:00			VMCAI Precise Thread-Modular Abstract Interpretation of Concurrent Programs u ... 17:00 - 17:30
Auditorium						CPP Mechanized verification of preemptive OS kernels 09:00 - 10:00						CPP Verified compilation of CakeML to multiple machine-code targets 10:30 - 11:00			CPP COMPLX: a verification framework for concurrent imperative programs 11:00 - 11:30			CPP Verifying dynamic race detection 11:30 - 12:00											CPP The HoTT library: a formalization of homotopy type theory in Coq 14:00 - 14:30			CPP Lifting proof-relevant unification to higher dimensions 14:30 - 15:00			CPP The Next 700 Syntactical models of type theory 15:00 - 15:30					CPP Type-and-scope safe programs and their proofs 16:00 - 16:30		CPP Formally verified differential dynamic logic 16:30 - 17:00			CPP Equivalence of System F and λ2 in Coq based on context morphism lemmas 17:00 - 17:30
Auditorium Hall										POPL Catering Break 10:00 - 10:30																												POPL Catering Break 15:30 - 16:00
Catering area																					POPL Catering Lunch 12:00 - 14:00
Salle 105, Barre 44-54						PPS Towards a metric semantics for probabilistic programming (invited talk) 09:00 - 10:00						PPS An application of computable distributions to the semantics of probabil ... 10:30 - 10:50		PPS Discussion 1 10:50 - 11:00	PPS Probabilistic programming and a domain theoretic approach to Skorohod's ... 11:00 - 11:20		PPS Discussion 2 11:20 - 11:30	PPS Building inference algorithms from monad transformers 11:30 - 11:50		PPS Discussion 3 11:50 - 12:00									PPS Commutativity logic for probabilistic trace equivalence: complete or not? 14:00 - 14:20		PPS Discussion 4 14:20 - 14:30	PPS Mathematical structures of probabilistic programming 14:30 - 14:50		PPS Discussion 5 14:50 - 15:00	PPS A weakest pre-expectation semantics for mixed-sign expectations 15:00 - 15:20		PPS Discussion 6 15:20 - 15:30	PPS ProbLog and applicative probabilistic programming 15:30 - 16:30 Encapsulating models and approximate inference programs in probabilisti ... 15:30 - 16:30 The extended semantics for probabilistic programming languages 15:30 - 16:30 Synthetic topology in homotopy type theory for probabilistic programming 15:30 - 16:30 Reasoning about inference in probabilistic programs 15:30 - 16:30 On computable representations of exchangeable data 15:30 - 16:30 Probabilistic logic programs: unifying program trace and possible world ... 15:30 - 16:30 Metropolis-Hastings for mixtures of conditional distributions 15:30 - 16:30 Support and influence analysis for visualizing posteriors of probabilis ... 15:30 - 16:30 Efficient exact inference in discrete Anglican programs 15:30 - 16:30				PPS An exponential family basis for probabilistic programming 16:30 - 16:50		PPS Discussion 7 16:50 - 17:00	PPS The semantics of subroutines and iteration in the Bayesian programming ... 17:00 - 17:20		PPS Discussion 8 17:20 - 17:30	PPS Exchangeable random process and data abstraction 17:30 - 17:50		PPS Discussion 9 17:50 - 18:00		PPS Reducing probabilistic choice to nondeterministic choice 18:15 - 18:35		PPS Discussion 10 18:35 - 18:45	PPS GraPPa: spanning the expressivity vs. efficiency continuum 18:45 - 19:05		PPS Discussion 11 19:05 - 19:15
Salle 107, Barre 44-54					PLMW Welcome Sesssion 08:50 - 09:00	PLMW Time management, family and quality of life 09:00 - 09:30		PLMW Abductive Reasoning in Deductive Verification 09:30 - 10:00				PLMW What is research and how to do it? Thinking globally and acting locally. 10:30 - 11:00			PLMW Mechanizing Meta-Theory in Beluga 11:00 - 11:30			PLMW Research: The Industrial Culture 11:30 - 12:00											PLMW Student Interaction Activity 14:00 - 15:00						PLMW How to Give Talks That People Can Follow 15:00 - 15:30					PLMW Machine Learning and Programming Languages: latest directions and resea ... 16:00 - 16:30		PLMW The Curse of Knowledge 16:30 - 17:00			PLMW Young Researcher Panel Session 17:00 - 18:00
Salle 109, Barre 44-54						PEPM Reversible computing from a programming language perspective 09:00 - 10:00						PEPM Cost versus Precision for Approximate Typing for Python 10:30 - 11:00			PEPM Refining types using type guards in TypeScript 11:00 - 11:30			PEPM Predicting Resource Consumption of Higher-Order Workflows 11:30 - 12:00											PEPM Practical Partial Evaluation for Language Implementation with Graal & ... 14:00 - 15:30											PEPM Functional Parallels of Sequential Imperatives 16:00 - 16:30		PEPM A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Tr ... 16:30 - 17:00
Salle 116, Barre 44-54						PADL Funky Grooves: Declarative Programming of Full-Fledged Musical Applications 09:00 - 09:30		PADL DALI for Cognitive Robotics: Principles and Prototype Implementation 09:30 - 10:00				PADL Improving Non-deterministic Computations in Functional Logic Programs 10:30 - 11:00			PADL Canonicalizing High-Level Constructs in Picat 11:00 - 11:30			PADL An Overview of PRhoLog 11:30 - 12:00

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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	21:00	15	30	45	22:00	15	30	45
Amphitheater 44								POPL Ogre and Pythia, An invariance proof method for weak consistency models 10:30 - 10:55		POPL A Posteriori Environment Analysis with Pushdown Delta CFA 10:55 - 11:20			POPL Semantic-Directed Clumping of Disjunctive Abstract States 11:20 - 11:45		POPL Fast Polyhedra Abstract Domain 11:45 - 12:10												POPL Beginner's Luck: A Language for Property-Based Generators 14:20 - 14:45		POPL Exact Bayesian Inference by Symbolic Disintegration 14:45 - 15:10		POPL Stochastic Invariants for Probabilistic Termination 15:10 - 15:35			POPL Coupling proofs are probabilistic product programs 15:35 - 16:00				POPL Monadic second-order logic on finite sequences 16:30 - 16:55		POPL On the Relationship Between Higher-Order Recursion Schemes and Higher-O ... 16:55 - 17:20			POPL Coming to Terms with Quantified Reasoning 17:20 - 17:45
Auditorium	POPL Opening 09:00 - 09:05	POPL The Influence of Dependent Types 09:05 - 10:00						POPL Polymorphism, subtyping and type inference in MLsub 10:30 - 10:55		POPL Java generics are Turing complete 10:55 - 11:20			POPL Hazelnut: A Bidirectionally Typed Structure Editor Calculus 11:20 - 11:45		POPL Modules, Abstraction, and Parametric Polymorphism 11:45 - 12:10												POPL A Promising Semantics for Relaxed-Memory Concurrency 14:20 - 14:45		POPL Automatically Comparing Memory Consistency Models 14:45 - 15:10		POPL Interactive Proofs in Higher-Order Concurrent Separation Logic 15:10 - 15:35			POPL A Relational Model of Types-and-Effects in Higher-Order Concurrent Sepa ... 15:35 - 16:00				POPL A Program Optimization for Automatic Database Result Caching 16:30 - 16:55		POPL Stream Fusion, to Completeness 16:55 - 17:20			POPL Rigorous Floating-point Mixed Precision Tuning 17:20 - 17:45
Auditorium Hall						POPL Catering Break 10:00 - 10:30																														POPL Catering Break 16:00 - 16:30
Catering area																	POPL Catering Lunch 12:10 - 14:20
Musée des Arts Forains																											POPL Catering Social dinner 19:30 - 23:00

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44									POPL Relational Cost Analysis 10:30 - 10:55		POPL Contract-based Resource Verification for Higher-order Functions with Me ... 10:55 - 11:20			POPL Context-sensitive data dependence analysis via Linear Conjunctive Langu ... 11:20 - 11:45		POPL Towards Automatic Resource Bound Analysis for OCaml 11:45 - 12:10												POPL Mixed-size Concurrency: ARM, POWER, C/C++11, and SC 14:20 - 14:45		POPL Dynamic Race Detection For C++11 14:45 - 15:10		POPL Serializability for Eventual Consistency: Criterion, Analysis and Appli ... 15:10 - 15:35			POPL Thread Modularity at Many Levels: a Pearl in Compositional Verification 15:35 - 16:00				POPL A Semantic Account of Metric Preservation 16:30 - 16:55		POPL Cantor Meets Scott: Semantic Foundations for Probabilistic Networks 16:55 - 17:20
Auditorium	POPL Turing Award Video 09:00 - 09:05	POPL Most Influential Paper Award 09:05 - 09:10	POPL Reynolds Doctoral Dissertation Award 09:10 - 09:15	POPL 40 Years of Abstract Interpretation — An Interview with Patrick Cousot 09:15 - 10:00					POPL Deciding equivalence with sums and the empty type 10:30 - 10:55		POPL The exp-log normal form of types: Decomposing extensional equality and ... 10:55 - 11:20			POPL Contextual isomorphisms 11:20 - 11:45		POPL Typed Self-Evaluation via Intensional Type Functions 11:45 - 12:10												POPL Type Directed Compilation of Row-Typed Algebraic Effects 14:20 - 14:45		POPL Do be do be do 14:45 - 15:10		POPL Dijkstra Monads for Free 15:10 - 15:35			POPL Stateful Manifest Contracts 15:35 - 16:00				POPL Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks 16:30 - 16:55		POPL LOIS: syntax and semantics 16:55 - 17:20			POPL PC Chair report 17:20 - 17:40		POPL POPL 2018 presentation 17:40 - 17:50		POPL SIGPLAN business meeting 17:50 - 18:20
Auditorium Hall							POPL Catering Break 10:00 - 10:30																														POPL Catering Break 16:00 - 16:30														POPL Student Research Competition Naturality despite Nontermination: A Logical Relation for Linear Types ... 18:20 - 18:30	POPL Student Research Competition Gradual Type Precision as Retraction 18:30 - 18:40	POPL Student Research Competition Linking Types: Specifying Safe Interoperability and Equivalences 18:40 - 18:50		POPL Student Research Competition A Monadic Framework for Bidirectional Programming 18:50 - 19:00	POPL Student Research Competition Gradual Set-Theoretic Types 19:00 - 19:10	POPL Student Research Competition Abstract Interpretation of High-Level Transformations 19:10 - 19:20		POPL Student Research Competition FairSquare: A Static Analysis Tool for Algorithmic Fairness 19:20 - 19:30	POPL Student Research Competition Toward Type-Preserving Compilation of Coq 19:30 - 19:40	POPL Student Research Competition A Symbolic Execution Framework for Haskell 19:40 - 19:50		POPL Student Research Competition Synthesizing Imperative Programs from Examples for Introductory Program ... 19:50 - 20:00	POPL Student Research Competition Provenance for Configuration Language Security 20:00 - 20:10	POPL Student Research Competition A gradually typed polymorphic lambda calculus 20:10 - 20:20
Catering area																		POPL Catering Lunch 12:10 - 14:20

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Amphitheater 44																			POPL Component-Based Synthesis for Complex APIs 10:30 - 10:55					POPL Learning nominal automata 10:55 - 11:20					POPL On Verifying Causal Consistency 11:20 - 11:45					POPL Complexity Verification Using Guided Theorem Enumeration 11:45 - 12:10																															POPL Parallel Functional Arrays 14:20 - 14:45					POPL A Short Counterexample Property for Safety and Liveness Verification of ... 14:45 - 15:10					POPL Analyzing divergence in bisimulation semantics 15:10 - 15:35

POPL 2017 Program

Filter Program

Program Display Configuration

Sun 15 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

VMCAI

VMCAI

VMCAI

VMCAI

Catering

Catering

Catering

TTT

TTT

TTT

TTT

SCM

SCM

SCM

SCM

Mon 16 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

VMCAI

VMCAI

VMCAI

VMCAI

CPP

CPP

CPP

CPP

Catering

Catering

Catering

VMCAI

Tutorials

Tutorials

Tutorials

Tutorials

PEPM

PEPM

PEPM

PEPM

Tutorials

Tutorials

Tutorials

Tutorials

PADL

PADL

PADL

PADL

PADL

Tue 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

VMCAI

VMCAI

VMCAI

VMCAI

CPP

CPP

CPP

CPP

Catering

Catering

Catering

PPS

PPS

PPS

PPS

PPS

PPS

PLMW

PLMW

PLMW

PLMW

PLMW

PEPM

Sun 15 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change