Program - POPL 2017

Filter

Badges

Your Program

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

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: (GMT+01:00) 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 - 09:00 Day opening		Welcome TTT
	09:00 - 09:20 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 - 09:40 Talk		Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT Steven Keuchel, Klara Mardirosian, Tom SchrijversKU Leuven
	09:40 - 10:00 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 - 10:00 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 - 10:00 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 - 10:30 Coffee break		Break Catering

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

	10:30 - 11:00 Talk		Partitioned Memory Models for Program Analysis. VMCAI Wei WangGoogle, Inc., Clark BarrettStanford University, Thomas WiesNew York University File Attached
	11:00 - 11:30 Talk		Property Directed Reachability for Proving Absence of Concurrent Modification Errors VMCAI Asya FrumkinTel Aviv University, Yotam 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 - 12:00 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 - 11:20 Talk		Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron TombGalois, Inc.
	11:20 - 11:40 Talk		Modelling Program Behaviour within Software Verification Tool LAV TTT Milena Vujosevic Janicic
	11:40 - 12:00 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 - 10:40 Talk		What is Secure Compilation? Part II (Short talk) SCM Cătălin HriţcuInria Paris Link to publication
	10:40 - 10:50 Talk		Can relational logic facilitate secure compilation? (Short talk) SCM David NaumannStevens Institute of Technology File Attached
	10:50 - 11:00 Talk		Full Abstraction for Language Design (Short talk) SCM Gabriel SchererNortheastern University File Attached
	11:00 - 11:10 Talk		Cogent: Where we Stand and What Comes Next (Short talk) SCM Christine RizkallahUniversity of Pennsylvania, USA File Attached
	11:15 - 12:00 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 - 14:00 Lunch		Lunch Catering

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

	14:00 - 14:30 Talk		Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI Igor KonnovTU Wien, Josef WidderTU Wien, Francesco Spegni, Luca Spalazzi
	14:30 - 15:00 Talk		Independence Abstractions and Models of Concurrency VMCAI Vijay D'SilvaGoogle Inc., Daniel KroeningUniversity of Oxford, Marcelo SousaUniversity of Oxford
	15:00 - 15:30 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 - 14:50 Talk		Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders MörtbergInria
	14:50 - 15:10 Talk		Equations: a tool for dependent pattern-matching TTT Cyprien Mangin, Matthieu SozeauInria File Attached
	15:10 - 15:30 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 - 14:45 Talk		Linking Types: Secure compilation of multi-language programs SCM Daniel PattersonNortheastern University File Attached
	14:45 - 15:30 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 - 16:00 Coffee break		Break Catering

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

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

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

	16:00 - 16:45 Talk		Software Fault Isolation avec CompCert SCM Frédéric Besson File Attached
	16:45 - 17:30 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: (GMT+01:00) 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 - 09:00 Talk		Opening remarks PADL

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

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

	09:00 - 10:00: Invited TalkCPP at Auditorium

	09:00 - 10:00 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 - 12:00 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 - 12:00 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 SchultzUniversity of Southern Denmark

	09:00 - 10:00 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 - 12:00 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 - 12:00 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 - 10:00 Talk		Proof checking and logic programming PADL Dale MillerINRIA Saclay and LIX

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

	10:00 - 10:30 Coffee break		Break Catering

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

	10:30 - 11:00 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 - 11:30 Talk		Efficient Elimination of Redundancies in Polyhedra using Raytracing VMCAI Alexandre Maréchal, Michael Perin Media Attached File Attached
	11:30 - 12:00 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 - 11:00 Talk		Verifying a hash table and its iterators in higher-order separation logic CPP François Pottier
	11:00 - 11:30 Talk		A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm CPP Jose Divasón, Sebastiaan Joosten, René ThiemannUniversity of Innsbruck, Akihisa Yamada
	11:30 - 12:00 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 - 11:00 Talk		Lightweight Soundness for Towers of Language Extensions PEPM Alejandro SerranoUtrecht University, Jurriaan HageUtrecht University
	11:00 - 11:30 Talk		Detecting code clones with gaps by function applications PEPM Tsubasa MatsushitaShibaura Institute of Technology, Isao SasanoShibaura Institute of Technology
	11:30 - 12:00 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 - 11:00 Talk		Lowering the learning curve for declarative programming: a Python API for the IDP system PADL Joost VennekensKU Leuven
	11:00 - 11:30 Talk		Extending Answer Set Programs with Interpreted Functions as First-class Citizens PADL Christoph RedlVienna University of Technology
	11:30 - 12:00 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 - 14:00 Lunch		Lunch Catering

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

	14:00 - 14:30 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 - 15:00 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 - 15:30 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 - 14:30 Talk		BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP Jan Jakubuv, Josef Urban
	14:30 - 15:00 Talk		Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP Reuben RoweUniversity College London, James Brotherston
	15:00 - 15:30 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 - 17:00 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 - 17:00 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 SchultzUniversity of Southern Denmark, Jeremy YallopUniversity of Cambridge, UK

	14:00 - 15:00 Talk		Idris, Inside-Out: A Tutorial on Extending Idris in Idris PEPM David Thrane ChristiansenIndiana University
	15:00 - 15:30 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 - 15:30 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 - 17:00 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 - 17:00 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 - 14:30 Talk		Failing Faster: Overlapping Patterns for Property-Based Testing PADL Jonathan FowlerUniversity of Nottingham, Graham HuttonUniversity of Nottingham
	14:30 - 15:00 Talk		Boltzmann Samplers for Closed Simply-Typed Lambda Terms PADL Maciej BendkowskiJagiellonian University, Katarzyna GrygielJagiellonian University, Paul TarauUniversity of North Texas
	15:00 - 15:30 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 - 16:00 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 - 16:30 Talk		Block-wise abstract interpretation by combining abstract domains with SMT VMCAI Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang
	16:30 - 17:00 Talk		IC3 - Flipping the E in ICE VMCAI Yakir Vizel, Arie GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University
	17:00 - 17:30 Talk		Counterexample Validation and Interpolation-Based Refinement for Forest Automata VMCAI Lukáš Holík, Martin HruskaBrno University of Technology , Ondrej LengalBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomas VojnarBrno University of Technology

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

	16:00 - 16:30 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 - 17:00 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 - 17:30 Talk		Markov Processes in Isabelle/HOL CPP Johannes HölzlTechnische Universität München DOI Pre-print File Attached
	17:30 - 18:00 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 - 16:30 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 - 17:00 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 - 16:30 Talk		A Domain-Specific Language for Software-Defined Radio PADL Geoffrey MainlandDrexel University
	16:30 - 17:00 Talk		A Declarative DSL for Customized Rendering of Text-Based Art PADL Felix Klock
	17:00 - 17:30 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: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

	08:50 - 09:00 Day opening		Welcome Sesssion PLMW

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

	09:00 - 10:00 Talk		Verification of Cancer Programs VMCAI Jasmin FisherMicrosoft Research

	09:00 - 10:00: Invited TalkCPP at Auditorium

	09:00 - 10:00 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 - 10:00 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 - 09:30 Talk		Time management, family and quality of life PLMW Kathleen FisherTufts University File Attached
	09:30 - 10:00 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 SchultzUniversity of Southern Denmark

	09:00 - 10:00 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 - 09:30 Talk		Funky Grooves: Declarative Programming of Full-Fledged Musical Applications PADL Henrik Nilsson, Guerric ChupinENSTA ParisTech
	09:30 - 10:00 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 - 10:30 Coffee break		Break Catering

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

	10:30 - 11:00 Talk		Reachability for dynamic parametric processes VMCAI Anca MuschollUniversité de Bordeaux / LaBRI, Helmut SeidlTechnische Universität München, Igor WalukiewiczCNRS, LaBRI
	11:00 - 11:30 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 - 12:00 Talk		Solving Nonlinear Integer Arithmetic with MCSat VMCAI Dejan JovanovićSRI International

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

	10:30 - 11:00 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 - 11:30 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 - 12:00 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 - 10:50 Talk		An application of computable distributions to the semantics of probabilistic programs: part 2 PPS Daniel HuangHarvard University, Greg MorrisettCornell University
	10:50 - 11:00 Meeting		Discussion 1 PPS
	11:00 - 11:20 Talk		Probabilistic programming and a domain theoretic approach to Skorohod's theorem PPS Michael MisloveTulane
	11:20 - 11:30 Meeting		Discussion 2 PPS
	11:30 - 11:50 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 - 12:00 Meeting		Discussion 3 PPS

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

	10:30 - 11:00 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 - 11:30 Talk		Mechanizing Meta-Theory in Beluga PLMW Brigitte PientkaMcGill University File Attached
	11:30 - 12:00 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 - 11:00 Talk		Cost versus Precision for Approximate Typing for Python PEPM Levin FritzUtrecht University, Jurriaan HageUtrecht University
	11:00 - 11:30 Talk		Refining types using type guards in TypeScript PEPM Ivo Gabe de WolffUtrecht University, Jurriaan HageUtrecht University
	11:30 - 12:00 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 - 11:00 Talk		Improving Non-deterministic Computations in Functional Logic Programs PADL Sergio AntoyKiel University, Michael HanusKiel University
	11:00 - 11:30 Talk		Canonicalizing High-Level Constructs in Picat PADL Neng-Fa ZhouCUNY Brooklyn College and Graduate Center, Jonathan FruhmanCUNY Brooklyn College
	11:30 - 12:00 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 - 14:00 Lunch		Lunch Catering

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

	14:00 - 14:30 Talk		Complete Abstractions and Subclassical Modal Logics VMCAI Vijay D'SilvaGoogle, Marcelo SousaUniversity of Oxford
	14:30 - 15:00 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 - 15:30 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 - 14:30 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 - 15:00 Talk		Lifting proof-relevant unification to higher dimensions CPP Jesper CockxiMinds, Belgium, Dominique DevrieseiMinds - Distrinet, KU Leuven
	15:00 - 15:30 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 - 14:20 Talk		Commutativity logic for probabilistic trace equivalence: complete or not? PPS Paul Blain Levy, Nathan BowlerUniversität Hamburg
	14:20 - 14:30 Meeting		Discussion 4 PPS
	14:30 - 14:50 Talk		Mathematical structures of probabilistic programming PPS Ilias GarnierUniversity of Edinburgh, Fredrik DahlqvistUniversity College London, Florence ClercMcGill University, Vincent DanosENS Paris/CNRS
	14:50 - 15:00 Meeting		Discussion 5 PPS
	15:00 - 15:20 Talk		A weakest pre-expectation semantics for mixed-sign expectations PPS Benjamin Lucien KaminskiRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University
	15:20 - 15:30 Meeting		Discussion 6 PPS

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

	14:00 - 15:00 Talk		Student Interaction Activity PLMW Eva DarulovaMPI-SWS, Loris D'AntoniUniversity of Wisconsin–Madison, Alexandra SilvaUniversity College London, Dimitrios VytiniotisMicrosoft Research, Cambridge
	15:00 - 15:30 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 - 15:30 Talk		Practical Partial Evaluation for Language Implementation with Graal & Truffle PEPM Gilles Duboscq

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

	15:30 - 16:00 Coffee break		Break Catering

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

	15:30 - 16:30 Meeting		ProbLog and applicative probabilistic programming PPS Alexander VandenbrouckeKU Leuven, Belgium, Tom SchrijversKU Leuven
	15:30 - 16:30 Meeting		Encapsulating models and approximate inference programs in probabilistic modules PPS Marco Cusumano-TownerMIT-CSAIL, Vikash MansinghkaMassachusetts Institute of Technology
	15:30 - 16:30 Meeting		The extended semantics for probabilistic programming languages PPS Siddharth SrivastavaUTRC Berkeley, Nicholas HayVicarious, Yi WUUC Berkeley, Stuart RussellUniversity of California, Berkeley
	15:30 - 16:30 Meeting		Synthetic topology in homotopy type theory for probabilistic programming PPS Florian Faissole, Bas Spitters
	15:30 - 16:30 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 - 16:30 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 - 16:30 Meeting		Probabilistic logic programs: unifying program trace and possible world semantics PPS Angelika KimmigKU Leuven, Luc De RaedtKU Leuven
	15:30 - 16:30 Meeting		Metropolis-Hastings for mixtures of conditional distributions PPS Oleg Kiselyov
	15:30 - 16:30 Meeting		Support and influence analysis for visualizing posteriors of probabilistic programs PPS Long OuyangStanford University
	15:30 - 16:30 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 - 16:30 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 - 17:00 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 - 17:30 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 - 16:30 Talk		Type-and-scope safe programs and their proofs CPP Guillaume AllaisRadboud University Nijmegen, James Chapman, Conor McBride, James McKinnaUniversity of Edinburgh
	16:30 - 17:00 Talk		Formally verified differential dynamic logic CPP Brandon Bohrer, Vincent RahliSnT, Ivana Vukotic, Marcus Voelp, André Platzer
	17:00 - 17:30 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 - 16:30 Talk		Machine Learning and Programming Languages: latest directions and research opportunities PLMW Martin VechevETH Zurich File Attached
	16:30 - 17:00 Talk		The Curse of Knowledge PLMW Benjamin C. PierceUniversity of Pennsylvania File Attached
	17:00 - 18:00 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 - 16:30 Talk		Functional Parallels of Sequential Imperatives PEPM Tiark RompfPurdue University, Kevin J. BrownStanford University
	16:30 - 17:00 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 - 16:50 Talk		An exponential family basis for probabilistic programming PPS Chad ScherrerGalois, Inc.
	16:50 - 17:00 Meeting		Discussion 7 PPS
	17:00 - 17:20 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 - 17:30 Meeting		Discussion 8 PPS
	17:30 - 17:50 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 - 18:00 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 - 18:35 Talk		Reducing probabilistic choice to nondeterministic choice PPS Ernie CohenAmazon Web Services
	18:35 - 18:45 Meeting		Discussion 10 PPS
	18:45 - 19:05 Talk		GraPPa: spanning the expressivity vs. efficiency continuum PPS Edwin WestbrookGalois, Inc., Chad ScherrerGalois, Inc., Nathan CollinsGalois, Inc., Eric MertensGalois, Inc.
	19:05 - 19:15 Meeting		Discussion 11 PPS

Wed 18 Jan
Times are displayed in time zone: (GMT+01:00) 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 - 09:05 Day opening		Opening POPL

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

	09:05 - 10:00 Talk		The Influence of Dependent Types POPL Stephanie WeirichUniversity of Pennsylvania

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

	10:00 - 10:30 Coffee break		Break Catering

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

	10:30 - 10:55 Talk		Ogre and Pythia, An invariance proof method for weak consistency models POPL Jade AlglaveUniversity College London, Patrick CousotNew York University
	10:55 - 11:20 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 - 11:45 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 - 12:10 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 - 10:55 Talk		Polymorphism, subtyping and type inference in MLsub POPL Stephen Dolan, Alan MycroftUniversity of Cambridge
	10:55 - 11:20 Talk		Java generics are Turing complete POPL Radu GrigoreUniversity of Kent
	11:20 - 11:45 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 - 12:10 Talk		Modules, Abstraction, and Parametric Polymorphism POPL Karl CraryCarnegie Mellon University

	12:10 - 14:20: BuffetCatering at Catering area

	12:10 - 14:20 Lunch		Lunch Catering

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

	14:20 - 14:45 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 - 15:10 Talk		Exact Bayesian Inference by Symbolic Disintegration POPL Chung-chieh ShanIndiana University, USA, Norman Ramsey Pre-print
	15:10 - 15:35 Talk		Stochastic Invariants for Probabilistic Termination POPL Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria, Djordje ZikelicUniversity of Cambridge
	15:35 - 16:00 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 - 14:45 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 - 15:10 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 - 15:35 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 - 16:00 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 - 16:30 Coffee break		Break Catering

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

	16:30 - 16:55 Talk		Monadic second-order logic on finite sequences POPL Loris D'AntoniUniversity of Wisconsin–Madison, Margus VeanesMicrosoft Research
	16:55 - 17:20 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 - 17:45 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 MyersCornell University

	16:30 - 16:55 Talk		A Program Optimization for Automatic Database Result Caching POPL Ziv ScullyCarnegie Mellon University, Adam ChlipalaMIT
	16:55 - 17:20 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 - 17:45 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 - 23:00 Dinner		Social dinner Catering

Thu 19 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

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

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

	09:15 - 10:00 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 - 10:30 Coffee break		Break Catering

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

	10:30 - 10:55 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 - 11:20 Talk		Contract-based Resource Verification for Higher-order Functions with Memoization POPL Ravichandhran MadhavanEPFL, Sumith KulalIIT Bombay, Viktor KunčakEPFL, Switzerland
	11:20 - 11:45 Talk		Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability POPL Qirun ZhangUniversity of California, Davis, Zhendong SuUniversity of California, Davis
	11:45 - 12:10 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 - 10:55 Talk		Deciding equivalence with sums and the empty type POPL Gabriel SchererNortheastern University
	10:55 - 11:20 Talk		The exp-log normal form of types: Decomposing extensional equality and representing terms compactly POPL Danko IlikTrusted Labs
	11:20 - 11:45 Talk		Contextual isomorphisms POPL Paul Blain Levy
	11:45 - 12:10 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 - 14:20 Lunch		Lunch Catering

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

	14:20 - 14:45 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 - 15:10 Talk		Dynamic Race Detection For C++11 POPL Christopher LidburyImperial College London, Alastair DonaldsonImperial College London
	15:10 - 15:35 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 - 16:00 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 - 14:45 Talk		Type Directed Compilation of Row-Typed Algebraic Effects POPL Daan LeijenMicrosoft Research
	14:45 - 15:10 Talk		Do be do be do POPL Sam LindleyUniversity of Edinburgh, Conor McBride, Craig McLaughlinThe University of Edinburgh
	15:10 - 15:35 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 - 16:00 Talk		Stateful Manifest Contracts POPL Taro Sekiyama, Atsushi IgarashiKyoto University

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

	16:00 - 16:30 Coffee break		Break Catering

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

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

Fri 20 Jan
Times are displayed in time zone: (GMT+01:00) 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 - 09:05 Awards		Student Competition Award Student Research Competition

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

	09:05 - 10:00 Talk		Rust: from POPL to practice POPL Aaron TuronMPI-SWS

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

	10:00 - 10:30 Coffee break		Break Catering

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

	10:30 - 10:55 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 - 11:20 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 - 11:45 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 - 12:10 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 - 10:55 Talk		Intersection Type Calculi of Bounded Dimension POPL Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
	10:55 - 11:20 Talk		Type Soundness Proofs with Definitional Interpreters POPL Nada AminEPFL, Tiark RompfPurdue University
	11:20 - 11:45 Talk		Computational Higher-Dimensional Type Theory POPL Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno
	11:45 - 12:10 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 - 14:20 Lunch		Lunch Catering

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

	14:20 - 14:45 Talk		Parallel Functional Arrays POPL Ananya Kumar, Guy E. BlellochCarnegie Mellon University, Robert Harper
	14:45 - 15:10 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 - 15:35 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 - 16:00 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 - 14:45 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 - 15:10 Talk		Gradual Refinement Types POPL Nicolás Lehmann, Éric TanterUniversity of Chile, Chile Link to publication DOI Pre-print
	15:10 - 15:35 Talk		Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL Matteo CiminiIndiana University, USA, Jeremy G. SiekIndiana University Bloomington
	15:35 - 16:00 Talk		Sums of Uncertainty: Refinements go gradual POPL Khurram A. JaferyUniversity of British Columbia, Joshua DunfieldUniversity of British Columbia

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

	16:00 - 16:30 Coffee break		Break Catering

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

	16:30 - 16:55 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 - 17:20 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 - 17:45 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 - 16:55 Talk		LMS-Verify: Abstraction Without Regret for Verified Systems Programming POPL Nada AminEPFL, Tiark RompfPurdue University
	16:55 - 17:20 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 - 17:45 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: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

	08:45 - 09:00 Day opening		Opening N40AI

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

	08:55 - 09:00 Talk		Welcome PiP

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

	09:00 - 09:30 Talk		Abstract Interpretation in Absint N40AI Christian FerdinandAbsInt
	09:30 - 10:00 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 - 10:00 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 - 09:30 Talk		Andrew Kennedy (Facebook) Static type checking for PHP PiP
	09:30 - 10:00 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 - 09:15 Talk		Welcome RDP Nate FosterCornell University, Mooly SagivTel Aviv University, Victor VianuUC San Diego
	09:15 - 10:00 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 - 10:00 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 - 10:30 Coffee break		Break Catering

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

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

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

	10:30 - 10:55 Talk		IxFree: Step-Indexed Logical Relations in Coq CoqPL Piotr Polesiuk File Attached
	10:55 - 11:20 Talk		Logical Relations in Iris CoqPL Amin Timanyimec - Distrinet, KU Leuven, Robbert KrebbersDelft University of Technology, Netherlands, Lars BirkedalAarhus University File Attached
	11:20 - 11:45 Talk		Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting CoqPL Edwin WestbrookGalois, Inc., Gregory MalechaUCSD File Attached
	11:45 - 12:10 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 - 10:35 Talk		Peter Sewell (Cambridge) REMS Short Introduction PiP
	10:35 - 11:05 Talk		Simon Moore (Cambridge) Experiences of Formal Modelling in the CHERI Computer Architecture Research Project PiP
	11:05 - 11:35 Talk		Stephen Kell/Dominic Mulligan (Cambridge) ELF linking: what it means and why it matters PiP
	11:35 - 12:05 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 - 11:00 Talk		Verification Challenges in Applications of Blockchain for Business Collaboration RDP Takaaki TateishiIBM Research - Tokyo
	11:00 - 11:30 Talk		Fiat: A New Take on Domain-Specific Languages by Programming with Specifications RDP Adam ChlipalaMIT
	11:30 - 12:00 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 - 10:55 Talk		Can we machine-learn programming language semantics? Off the Beaten Track Dan GhicaUniversity of Birmingham, Khulood Alyahya, Victor Patentasu File Attached
	10:55 - 11:20 Talk		How Far Apart Should Those Programs Be? Off the Beaten Track Ugo Dal LagoUniversity of Bologna, France File Attached
	11:20 - 11:45 Talk		Programming Quantum Annealers Off the Beaten Track George Stelle, Scott Pakin File Attached
	11:45 - 12:10 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 - 14:00 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 - 14:30 Talk		Security N40AI Michael HicksUniversity of Maryland at College Park, USA
	14:30 - 15:00 Talk		Big Code N40AI Bor-Yuh Evan ChangUniversity of Colorado Boulder
	15:00 - 15:30 Talk		Program synthesis N40AI Eran YahavTechnion

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

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

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

	14:00 - 14:30 Talk		John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck PiP
	14:30 - 15:00 Talk		Byron Cook (Amazon) Automated Reasoning about AWS PiP
	15:00 - 15:30 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 - 14:45 Talk		Synthesizing Data-parallel Programs RDP Aws AlbarghouthiUniversity of Wisconsin - Madison
	14:45 - 15:30 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 - 15:00 Talk		Keynote talk: Varieties of Programming Experience Off the Beaten Track Alan BlackwellUniversity of Cambridge
	15:00 - 15:25 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 - 16:00 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 - 16:30 Talk		System verification N40AI Arie GurfinkelUniversity of Waterloo
	16:30 - 17:45 Talk		Keynote: the Next 40 years of Abstract Interpretation N40AI Patrick CousotNew York University
	17:45 - 18:30 Social Event		Concrete Cheese and Wine N40AI

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

	16:00 - 16:25 Talk		Synthetic topology in HoTT for probabilistic programming CoqPL Florian Faissole, Bas Spitters File Attached
	16:25 - 16:50 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 - 17:15 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 - 17:40 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 - 18:05 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 - 16:30 Talk		Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models PiP
	16:30 - 17:30 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 - 16:30 Talk		Building performance-sensitive systems in high-level languages RDP Christoph E. Koch
	16:30 - 17:00 Talk		Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data RDP Kathleen FisherTufts University
	17:00 - 17:30 Talk		Computation with Atoms RDP Szymon Toruńczyk
	17:30 - 18:00 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 - 16:25 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 - 16:50 Talk		Laziness Boxes You In Off the Beaten Track Jose CalderonGalois, Inc., Stephen Magill File Attached
	16:50 - 17:15 Talk		Programming with Epistemic Logic Off the Beaten Track Markus Eger, Chris MartensCarnegie Mellon University File Attached
	17:15 - 17:40 Talk		Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach Off the Beaten Track Marco GaboardiSUNY Buffalo, USA File Attached
	17:40 - 18:05 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 - 21:00 Social Event		CoqPL Social Event CoqPL

Sun 15 Jan
Times are displayed in time zone: (GMT+01:00) 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
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: (GMT+01:00) 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	22: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: (GMT+01:00) 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: (GMT+01:00) 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	23: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: (GMT+01:00) 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 2017 Program

Program Display Configuration

Sun 15 Jan Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan Times are displayed in time zone: (GMT+01:00) 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: (GMT+01:00) 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: (GMT+01:00) 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

PEPM

Sun 15 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Times are displayed in time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change