Program - POPL 2019

Filter

Sun 13 Jan

08:30 - 10:30: BEAT 2019 - Session 1 at BEAT

08:30 - 08:40
Day opening

Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. PerezUniversity of Groningen, The Netherlands

08:40 - 09:30
Talk

Invited Talk: Gradual Session Types — an Ongoing Journey

Peter ThiemannUniversity of Freiburg, Germany

09:30 - 09:50
Talk

Gradual Session Types in Imperative Style

Kaede KobayashiKyoto University, Atsushi IgarashiKyoto University, Japan

09:50 - 10:10
Talk

Checking the equivalence of context-free session types

Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon

10:10 - 10:30
Talk

Effpi: concurrent programming with dependent behavioural types

Alceste ScalasImperial College London, Elias BenussiImperial College London, Nobuko YoshidaImperial College London

09:00 - 10:30: VMCAI 2019 - Invited Talk 1 at VMCAI

09:00 - 10:30
Talk

Under and Over Approximated Reachability Analysis for the Verifcation of Control Systems

Sylvie PutotÉcole Polytechnique

09:00 - 10:30: PriSC 2019 - Session 1 at PriSC

09:00 - 10:00
Talk

PriSC Keynote - Jasmin: A Compiler and Framework for High-Assurance and High-Speed Cryptography

Benjamin GregoireINRIA

11:00 - 12:30: VMCAI 2019 - Abstract interpretation (1) at VMCAI

11:00 - 11:30
Talk

Static Analysis Of Binary Code With Memory Indirections Using Polyhedra

Clément Ballabriga, Julien Forget, Laure GonnordUniversity of Lyon & LIP, France, Giuseppe Lipari, Jordy Ruiz

11:30 - 12:00
Talk

Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis

Rémy Boutonnet, Nicolas Halbwachs

12:00 - 12:30
Talk

Application of Abstract Interpretation to the Automotive Electronic Control System

Tomoya Yamaguchi, Martin Brain, Chris Ryder, Yosikazu Imai, Yoshiumi Kawamura

11:00 - 12:30: PriSC 2019 - Session 2 at PriSC

11:00 - 12:30: BEAT 2019 - Session 2 at BEAT

11:00 - 11:50
Talk

Invited Talk: On Type-Based Complexity Analysis of Programs and Processes

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France

11:50 - 12:10
Talk

Global Types with Internal Delegation

Ilaria CastellaniINRIA Sophia Antipolis, France, Mariangiola DezaniUniversità di Torino, Paola GianniniUniversita' del Piemonte Orientale, Ross HorneComputer Science and Communications Research Unit, University of Luxembourg

12:10 - 12:30
Talk

Two Declarative Approaches for Session-Based Concurrency

Mauricio CanoUniversity of Groningen, The Netherlands

13:30 - 15:30: BEAT 2019 - Session 3 at BEAT

13:30 - 14:20
Talk

Invited Talk: TBA

Jan HoffmannCarnegie Mellon University

14:20 - 15:10
Talk

Invited Talk: A Session Type Provider: Compile-time Generation of Session Types with Interaction Refinements

Rumyana NeykovaImperial College London, UK

15:10 - 15:30
Talk

Getting rid of null-dereferences – Behavioural types to the rescue

Hans HüttelDepartment of Computer Science, Aalborg University, Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Adrian FrancalanzaUniversity of Malta, Mario BravettiUniversità di Bologna

14:00 - 15:30: VMCAI 2019 - Program Synthesis at VMCAI

14:00 - 14:30
Talk

Minimal Synthesis of String To String Functions From Examples

Jad HamzaLIAFA, Université Paris Diderot, Viktor KuncakEPFL, Switzerland

14:30 - 15:00
Talk

Lazy but Effective Functional Synthesis

Grigory FedyukovichPrinceton University, Arie GurfinkelUniversity of Waterloo, Aarti GuptaPrinceton University

15:00 - 15:30
Talk

Automatic Program Repair using Formal Verification and Expression Templates

Thanh-Toan Nguyen, Quang-Trung TaNational University of Singapore, Wei-Ngan ChinNational University of Singapore

14:00 - 15:30: PriSC 2019 - Session 3 at PriSC

16:00 - 17:30: VMCAI 2019 - Abstract Interpretation (2) at VMCAI

16:00 - 16:30
Talk

Demand Control-Flow Analysis

Kimball GermaneUniversity of Utah, Jay McCarthyUniversity of Massachusetts Lowell, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School

16:30 - 17:00
Talk

Relatively Complete Pushdown Analysis of Escape Continuations

Kimball GermaneUniversity of Utah, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School

17:00 - 17:30
Talk

Effect-driven Flow Analysis

Jens NicolayVrije Universiteit Brussel, Belgium, Quentin StiévenartVrije Universiteit Brussel, Belgium, Wolfgang De MeuterVrije Universiteit Brussel, Coen De RooverVrije Universiteit Brussel

16:00 - 17:30: PriSC 2019 - Session 4 at PriSC

16:00 - 18:25: BEAT 2019 - Session 4 at BEAT

16:00 - 16:50
Talk

Invited Talk: Session Types for Fault-Tolerant Distributed Algorithms

Kirstin PetersTU Berlin

16:50 - 17:10
Talk

Behavioral Types as a Semantic Foundation for the GDPR notion of Purpose

Evangelia VaneziUniversity of Cyprus, Dimitrios KouzapasUniversity of Cyprus, Anna PhilippouUniversity of Cyprus

17:10 - 17:30
Talk

Relating Process Languages for Security and Communication Correctness

Daniele Nantes-SobrinhoUniversity of Brasília, Brazil, Jorge A. PerezUniversity of Groningen, The Netherlands

17:30 - 17:40
Break

Short break

17:40 - 18:00
Talk

Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs

Søren DeboisIT University of Copenhagen, Thomas H. Hildebrandt, Hugo LópezIT University of Copenhagen, Denmark & DCR Solutions A/S

18:00 - 18:20
Talk

Hardware interactions as behavioural types

Carlos Mão de FerroLASIGE, Faculty of Sciences, University of Lisbon, Francisco MartinsLaSIGE, University of Lisbon, Tiago CogumbreiroUniversity of Massachusetts Boston

18:20 - 18:25
Day closing

Closing

Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. PerezUniversity of Groningen, The Netherlands

Mon 14 Jan

09:00 - 10:30: TutorialFest - Engineering Distributed Systems via Protocols and Commitments I at TutorialFest 2

09:00 - 10:30
Talk

[T2] Engineering Distributed Systems via Protocols and Commitments

Amit ChopraLancaster University, UK, Munindar P. SinghNorth Carolina State University

09:00 - 10:30: VMCAI 2019 - Invited Talk 2 at VMCAI

09:00 - 10:30
Talk

Designing Self-Certifying Software Systems

Kedar NamjoshiBell Labs, Nokia

09:00 - 10:30: CPP 2019 - Keynote 1 and Research Paper at CPP

09:00 - 10:00
Talk

A Linear Logical Framework in Hybrid

Amy FeltyUniversity of Ottawa

10:00 - 10:30
Research paper

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines

Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA

09:00 - 10:30: TutorialFest - Linear and Graded Modal Types for Fine-Grained Program Reasoning I at TutorialFest 3

09:00 - 10:30
Talk

[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning

Dominic OrchardUniversity of Kent, UK, Harley D. Eades IIIAugusta University, Vilem-Benjamin LiepeltUniversity of Kent, UK

09:00 - 10:30: TutorialFest - Programming Cyber-Physical Systems With Logic I at TutorialFest 4

09:00 - 10:30
Talk

[T4] Programming Cyber-Physical Systems With Logic

André PlatzerCarnegie Mellon University

09:00 - 10:30: TutorialFest - QuickChick: Property-Based Testing in Coq I at TutorialFest 1

09:00 - 10:30
Talk

[T1] QuickChick: Property-Based Testing in Coq

Benjamin C. PierceUniversity of Pennsylvania, Leonidas LampropoulosUniversity of Pennsylvania

11:00 - 12:30: VMCAI 2019 - Decision Procedures at VMCAI

11:00 - 11:30
Talk

Solving and Interpolating Constant Arrays Based on Weak Equivalences

Jochen HoenickeUniversität Freiburg, Tanja SchindlerUniversity of Freiburg

11:30 - 12:00
Talk

A Decidable Logic for Tree Data-Structures with Measurements

Xiaokang QiuPurdue University, Yanjun Wang

12:00 - 12:30
Talk

A Practical Algorithm for Structure Embedding

Charlie MurphyPrinceton University, Zachary KincaidPrinceton University

11:00 - 12:30: TutorialFest - Engineering Distributed Systems via Protocols and Commitments II at TutorialFest 2

11:00 - 12:30
Talk

[T2] Engineering Distributed Systems via Protocols and Commitments

Amit ChopraLancaster University, UK, Munindar P. SinghNorth Carolina State University

11:00 - 12:30: TutorialFest - Linear and Graded Modal Types for Fine-Grained Program Reasoning II at TutorialFest 3

11:00 - 12:30
Talk

[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning

Dominic OrchardUniversity of Kent, UK, Harley D. Eades IIIAugusta University, Vilem-Benjamin LiepeltUniversity of Kent, UK

11:00 - 12:30: TutorialFest - Programming Cyber-Physical Systems With Logic II at TutorialFest 4

11:00 - 12:30
Talk

[T4] Programming Cyber-Physical Systems With Logic

André PlatzerCarnegie Mellon University

11:00 - 12:30: TutorialFest - QuickChick: Property-Based Testing in Coq II at TutorialFest 1

11:00 - 12:30
Talk

[T1] QuickChick: Property-Based Testing in Coq

Benjamin C. PierceUniversity of Pennsylvania, Leonidas LampropoulosUniversity of Pennsylvania

11:00 - 12:30: CPP 2019 - Research Papers: Proof Theory, Theory of Programming Languages at CPP

11:00 - 11:30
Research paper

A proof-theoretic approach to certifying skolemization

Kaustuv ChaudhuriInria, France, Matteo ManighettiInria & École Polytechnique, Dale MilerINRIA Saclay and LIX

11:30 - 12:00
Research paper

Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory

Yannick ForsterSaarland University, Steven Schäfer, Simon Spies, Kathrin StarkSaarland University, Germany

12:00 - 12:30
Research paper

Eliminating Reflection from Type Theory

Theo WinterhalterGallinette / Inria / LS2N, Nicolas TabareauInria, Matthieu SozeauInria

11:00 - 12:30: PEPM 2019 - Session 1 at PEPM

11:00 - 12:00
Talk

Applying Futamura projections to compose languages and tools in GraalVM (Invited Talk)

Christian HumerOracle Labs, Switzerland

12:00 - 12:30
Talk

A Simpler Lambda Calculus

Barry JayUniversity of Technology Sydney

14:00 - 15:30: TutorialFest - Building Your Own Modular Static Analyser with Infer I at TutorialFest 4

14:00 - 15:30
Talk

[T8] Building Your Own Modular Static Analyser with Infer

Jules Villard, Ezgi ÇiçekFacebook London, Dino DistefanoFacebook London, Nikos Gorogiannis, Peter O'HearnFacebook

14:00 - 15:30: TutorialFest - Correct-by-Construction Programming in Agda I at TutorialFest 1

14:00 - 15:30
Talk

[T5] Correct-by-Construction Programming in Agda

Andreas AbelGothenburg University, Jesper CockxChalmers | University of Gothenburg

14:00 - 15:30: TutorialFest - Higher-Order Probabilistic Programming I at TutorialFest 3

14:00 - 15:30
Talk

[T7] Higher-Order Probabilistic Programming

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France

14:00 - 15:30: PADL 2019 - PADL Session 1 at PADL

14:00 - 14:30
Talk

Natural Language Generation From Ontologies

Van Nguyen, Tran Cao Son, Enrico Pontelli

14:30 - 15:00
Talk

Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP

Joaquin Arias, Manuel CarroIMDEA Software Institute and T.U. of Madrid (UPM)

15:00 - 15:30
Talk

Improving Residuation in Declarative Programs

Michael HanusKiel University

14:00 - 15:30: VMCAI 2019 - Probabilistic Systems at VMCAI

14:00 - 14:30
Talk

Syntactic Partial Order Compression for Probabilistic Reachability

Gereon Fox, Daniel Stan, Holger HermannsSaarland University

14:30 - 15:00
Talk

Termination of Nondeterministic Probabilistic Programs

Hongfei FuIST Austria, Krishnendu ChatterjeeIST Austria

15:00 - 15:30
Talk

Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics

Stefan Haar, Juraj KolčákLSV, CNRS & ENS Cachan, University Paris Saclay, Loïc Paulevé

14:00 - 15:30: CPP 2019 - Research Papers: Program Verification at CPP

14:00 - 14:30
Research paper

Formally Verified Big Step Semantics out of x86-64 Binaries

Ian RoessleVirginia Tech, USA, Freek VerbeekOpen University of the Netherlands, The Netherlands, Binoy RavindranVirginia Tech

14:30 - 15:00
Research paper

Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions

Sandrine BlazyUniv Rennes- IRISA, Rémi Hutin

15:00 - 15:30
Research paper

From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server

Nicolas Koh, Yao LiUniversity of Pennsylvania, Yishuai LiUniversity of Pennsylvania, Li-yao Xia, Lennart BeringerPrinceton University, Wolf Honore, William ManskyUniversity of Illinois at Chicago, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania

14:00 - 15:30: PEPM 2019 - Session 2 at PEPM

14:00 - 14:30
Talk

Method Name Suggestion with Hierarchical Attention Networks

Sihan XuNankai University, China, Sen ZhangNankai University, China, Weijing WangNankai University, China, Xinya CaoNankai University, China, Chenkai GuoNankai University, China, Jing XuNankai University, China

14:30 - 15:00
Talk

Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking

Keiichi WatanabeUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Hiroki OshikawaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan

15:00 - 15:30
Talk

Typed Parsing and Unparsing for Untyped Regular Expression Engines

Gabriel RadanneUniversity of Freiburg, Germany

14:00 - 15:30: TutorialFest - Session-Typed Concurrent Programming I at TutorialFest 2

14:00 - 15:30
Talk

[T6] Session-Typed Concurrent Programming

Stephanie BalzerCarnegie Mellon University, USA

16:00 - 17:30: TutorialFest - Building Your Own Modular Static Analyser with Infer II at TutorialFest 4

16:00 - 17:30
Talk

[T8] Building Your Own Modular Static Analyser with Infer

Jules Villard, Ezgi ÇiçekFacebook London, Dino DistefanoFacebook London, Nikos Gorogiannis, Peter O'HearnFacebook

16:00 - 17:30: TutorialFest - Correct-by-Construction Programming in Agda II at TutorialFest 1

16:00 - 17:30
Talk

[T5] Correct-by-Construction Programming in Agda

Andreas AbelGothenburg University, Jesper CockxChalmers | University of Gothenburg

16:00 - 17:30: TutorialFest - Higher-Order Probabilistic Programming II at TutorialFest 3

16:00 - 17:30
Talk

[T7] Higher-Order Probabilistic Programming

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France

16:00 - 17:30: VMCAI 2019 - Model Checking at VMCAI

16:00 - 16:30
Talk

Parametric Timed Broadcast Protocols

Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye, Paulin Fournier, Didier Lime

16:30 - 17:00
Talk

Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic

Normann Decker, Anton Pirogov

17:00 - 17:30
Talk

A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization

Alfons LaarmanVienna University of Technology, Richard Huybers

16:00 - 17:30: PADL 2019 - PADL Session 2 at PADL

16:00 - 16:30
Talk

Faster Coroutine Pipelines: A Reconstruction

Ruben P. Pieters, Tom SchrijversKU Leuven

16:30 - 17:00
Talk

Distributed Protocol Combinators

Kristoffer Just Arndal AndersenAarhus University, Ilya SergeyYale-NUS College

17:00 - 17:30
Talk

Classes of Arbitrary Kind

Alejandro SerranoUtrecht University, Netherlands, Victor Cacciari MiraldoUtrecht University, Netherlands

16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at CPP

16:00 - 16:30
Research paper

A formal proof of Hensel's lemma over the p-adic integers

Robert Y. LewisVrije Universiteit Amsterdam

16:30 - 17:00
Research paper

Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem

Wenda LiUniversity of Cambridge, Lawrence PaulsonUniversity of Cambridge

17:00 - 17:30
Research paper

Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL

Fabian Immler, Bohua Zhan

16:00 - 17:30: PEPM 2019 - Session 3 at PEPM

16:00 - 17:00
Talk

What is the type of a partial evaluator? (Invited Talk)

Jens PalsbergUniversity of California, Los Angeles (UCLA)

17:00 - 17:30
Talk

Combining Higher-Order Model Checking with Refinement Type Inference

Ryosuke SatoKyushu University, Japan, Naoki IwayamaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan

16:00 - 17:30: TutorialFest - Session-Typed Concurrent Programming II at TutorialFest 2

16:00 - 17:30
Talk

[T6] Session-Typed Concurrent Programming

Stephanie BalzerCarnegie Mellon University, USA

Tue 15 Jan

09:00 - 10:30: LAFI (né PPS) - Archimedes at LAFI

09:00 - 09:10
Talk

Probabilistic Lambda Calculus: Beyond Deterministic Evaluation

Claudia FaggianIRIF, Simona Ronchi Della RoccaUniversity of Torino

09:10 - 09:30
Talk

The Geometry of Bayesian Programming

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Naohiko HoshinoKyoto University

09:30 - 10:30
Talk

Invited talk: Connecting probabilistic programming theory to applications in Stan

Matthijs VákárUniversity of Oxford

09:00 - 10:30: VMCAI 2019 - Invited Talk 3 at VMCAI

09:00 - 10:30
Talk

Semantics for Compiler IRs: Undefined Behavior is not Evil!

Nuno P. LopesMicrosoft Research

09:00 - 10:30: CPP 2019 - Keynote 2 and Research Paper at CPP

09:00 - 10:00
Talk

Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL

Jasmin Christian BlanchetteVrije Universiteit Amsterdam

10:00 - 10:30
Research paper

A Verified Prover Based on Ordered Resolution

Anders SchlichtkrullTechnical University of Denmark, Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich

09:00 - 10:30: PADL 2019 - PADL Session 3 at PADL

09:30 - 10:00
Talk

Personalized Course Schedule Planning using Answer Set Programming

Esra ErdemSabanci University, Turkey, Muhammed Kerem Kahraman

10:00 - 10:30
Talk

Static Partitioning of Spreadsheets for Parallel Execution

Alexander Asp Bock

09:00 - 10:30: PLMW@POPL - PLMW Session 1 at PLMW

09:00 - 09:15
Day opening

PLMW Welcome

09:15 - 10:00
Talk

Technical Talk: Verification of Distributed Protocols Using Decidable Logic

Sharon ShohamTel Aviv university

10:00 - 10:30
Talk

Research Skills: How to Give a Talk

Chung-chieh ShanIndiana University, USA

11:00 - 12:30: LAFI (né PPS) - Borel at LAFI

11:00 - 11:30
Talk

Strongly typed tracing of probabilistic programs

Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Michael ThomasIndependent Researcher

11:30 - 12:00
Talk

Model and Inference Combinators for Deep Probabilistic Programming

Eli SenneshNortheastern University, Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Hao WuNortheastern University, Jan-Willem van de MeentNortheastern University

12:00 - 12:30
Talk

Server-side Probabilistic Programming

David TolpinPUB+

11:00 - 12:30: PADL 2019 - PADL Session 4 at PADL

11:00 - 11:30
Talk

An ASP-based Approach to Representing and Querying Textual Knowledge

Dhruva Pendharkar, Gopal Gupta

11:30 - 12:00
Talk

Strong Equivalence and Program's Structure in Arguing Essential Equivalence

Yuliya LierlerUniversity of Nebraska

12:00 - 12:30
Talk

Automatic Program Rewriting in Non-Ground Answer Set Programs

Nick Hippen, Yuliya LierlerUniversity of Nebraska

11:00 - 12:30: PLMW@POPL - PLMW Session 2 at PLMW

11:00 - 11:30
Talk

Research Skills: Work/Life Balance

Catuscia PalamidessiINRIA and LIX

11:30 - 12:30
Talk

Panel: Grad School and Beyond

Dominic OrchardUniversity of Kent, UK, Jorge A. PerezUniversity of Groningen, The Netherlands, Azalea RaadMPI-SWS, Germany, Max NewNortheastern University, Stephanie BalzerCarnegie Mellon University, USA

11:00 - 12:30: CPP 2019 - Research Papers: Rewriting, Automated Reasoning at CPP

11:00 - 11:30
Research paper

Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions

Kathrin StarkSaarland University, Germany, Steven Schäfer, Jonas Kaiser

11:30 - 12:00
Research paper

Certified ACKBO

Alexander Lochmann, Christian SternagelUniversity of Innsbruck, Austria

12:00 - 12:30
Research paper

A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL

Bertram Felgenhauer, aart Middeldorp, Turaga Prathamesh, Franziska Rapp

11:00 - 12:30: PEPM 2019 - Session 4 at PEPM

11:00 - 12:00
Talk

Making proofs easy: Horn clause transformations to the aid of program verification (Invited Talk)

Maurizio Proietti

12:00 - 12:30
Talk

Control Flow Obfuscation via CPS Transformation

Kenny Zhuo Ming LuNanyang Polytechnic, Singapore

11:00 - 12:30: VMCAI 2019 - Software Verification and Synthesis at VMCAI

11:00 - 11:30
Talk

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

Viorel Preoteasa, Iulia Dragomir, Stavros TripakisAalto University and UC Berkeley

11:30 - 12:00
Talk

euforia: Complete Software Model Checking with Uninterpreted Functions

Denis Bueno, Karem A. Sakallah

12:00 - 12:30
Talk

Program Synthesis with Equivalence Reduction

Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison

14:00 - 15:30: LAFI (né PPS) - Cauchy at LAFI

14:00 - 14:30
Talk

A Nuts-and-Bolts Differential Geometric Perspective on Automatic Differentiation

Barak A. PearlmutterMaynooth University

14:30 - 15:00
Talk

Kotlin∇: Differentiable functional programming with algebraic data types

Breandan ConsidineUniversité de Montréal

15:00 - 15:30
Talk

Probabilistic Programming with CuPPL

Alexander CollinsNVIDIA, Vinod GroverNVIDIA

14:00 - 15:30: PADL 2019 - PADL Session 5 at PADL

14:00 - 14:30
Talk

Composing Syntactical Constructs to Create Domain-Specific Languages

Viktor Palmkvist, David BromanKTH Royal Institute of Technology

14:30 - 15:00
Talk

Proof Carrying Plans

Christopher SchwaabUniversity of St Andrews, Ekaterina KomendantskayaHeriot-Watt University, UK, Alasdair Hill, Frantisek Farka, Ron Petrick, Joe Wells, Kevin HammondUniversity of St. Andrews, UK

15:00 - 15:30
Talk

A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers

Paul TarauUniversity of North Texas

14:00 - 15:30: PLMW@POPL - PLMW Session 3 at PLMW

14:00 - 14:45
Talk

Technical Talk: How to Think about Types

Frank PfenningCarnegie Mellon University, USA

14:45 - 15:30
Talk

Technical Talk: What Is Programming Languages Research?

Michael HicksUniversity of Maryland, College Park

14:00 - 15:30: CPP 2019 - Research Papers: Program Verification at CPP

14:00 - 14:30
Research paper

A Verified Protocol Buffer Compiler

Qianchuan Ye, Benjamin DelawarePurdue University

14:30 - 15:00
Research paper

A Coq mechanised formal semantics for realistic SQL queries - Formally reconciling SQL and bag relational algebra

Véronique BenzakenLRI, Université Paris-Sud, Evelyne Contejean

15:00 - 15:30
Research paper

Dynamic Class Initialization Semantics: a Jinja Extension

Susannah Mansky, Elsa GunterUniversity of Illinois

14:00 - 15:30: PEPM 2019 - Session 5 at PEPM

14:00 - 14:30
Talk

Extracting a Call-by-Name Partial Evaluator from a Proof of Termination

Kenichi AsaiOchanomizu University

14:30 - 15:00
Talk

Futures and Promises in Haskell and Scala

Tamino DauthKarlsruhe University of Applied Sciences, Germany, Martin SulzmannKarlsruhe University of Applied Sciences, Germany

15:00 - 15:30
Talk

Generating Mutually Recursive Definitions

Jeremy YallopUniversity of Cambridge, UK, Oleg Kiselyov

14:00 - 15:30: VMCAI 2019 - Software Verification at VMCAI

14:00 - 14:30
Talk

Type-directed Bounding of Collections in Reactive Programs

Tianhan LuUniversity of Colorado Boulder, Pavol CernyUniversity of Colorado Boulder, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Ashutosh Trivedi

14:30 - 15:00
Talk

Exploiting Pointer Analysis in Memory Models for Deductive Verification

Quentin Bouillaguet, François BobotCEA, Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France, Boris YakobowskiCEA - LIST

15:00 - 15:30
Talk

Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs

Anja KarlInstitute of Applied Information Processing and Communications, Graz University of Technology, Robert Schilling, Roderick BloemInstitute of Software Technology, Graz University of Technology , Stefan Mangard

16:00 - 17:30: LAFI (né PPS) - Dirichlet at LAFI

16:00 - 16:30
Talk

Probabilistic Programming Inference via Intensional Semantics

Simon Castellan, Hugo PaquetUniversity of Cambridge

16:30 - 17:00
Talk

Factorized Exact Inference for Discrete Probabilistic Programs

Steven HoltzenUniversity of California, Los Angeles, Joe QianUniversity of California, Los Angeles, Todd MillsteinUniversity of California, Los Angeles, Guy Van den BroeckUniversity of California, Los Angeles

17:00 - 17:30
Talk

Verified equational reasoning on a little language of measures

Matthew HeimerdingerIndiana University, Chung-chieh ShanIndiana University, USA

16:00 - 17:30: VMCAI 2019 - Networks and Concurrency at VMCAI

16:00 - 16:30
Talk

On the Semantics of Snapshot Isolation

Azalea RaadMPI-SWS, Germany, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, Germany

16:30 - 17:00
Talk

Fast BGP Simulation of Large Datacenters

Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research

17:00 - 17:30
Talk

Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking

Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Laurent Fribourg, Romain Soulat, Jean-Marc Mota

16:00 - 17:30: PLMW@POPL - PLMW Session 4 at PLMW

16:00 - 16:30
Talk

Panel: How to Do Great PL Research

Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon, Deepak GargMax Planck Institute for Software Systems, Philippa GardnerImperial College London, Atsushi IgarashiKyoto University, Japan, Neelakantan R. KrishnaswamiComputer Laboratory, University of Cambridge

16:30 - 17:30
Talk

Research Skills: How to Bootstrap a Research Project

Ilya SergeyYale-NUS College

16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at CPP

16:00 - 16:30
Research paper

On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem

Yannick ForsterSaarland University, Dominik KirstSaarland University, Gert SmolkaSaarland University

16:30 - 17:00
Research paper

Verified Solving and Asymptotics of Linear Recurrences

Manuel EberlTechnische Universität München

17:00 - 17:30
Meeting

Business Meeting

Assia MahboubiINRIA, Magnus O. MyreenChalmers University of Technology, Sweden

16:00 - 17:30: PEPM 2019 - Session 6 at PEPM

16:00 - 17:30
Poster

PEPM Poster Session

Wed 16 Jan

09:00 - 10:05: Research Papers - Welcome & Keynote I at POPL

09:00 - 09:05
Day opening

Welcome

Fritz HengleinDepartment of Computer Science, University of Copenhagen (DIKU), Stephanie WeirichUniversity of Pennsylvania, USA

09:05 - 10:05
Talk

Automated Fault-Finding and Fixing at Facebook

Mark HarmanFacebook and University College London

10:35 - 12:03: Research Papers - Concurrency at POPL Track 2

10:35 - 10:57
Talk

A True Positives Theorem for a Static Race Detector

Nikos Gorogiannis, Peter W. O'HearnFacebook and University College London, Ilya SergeyYale-NUS College

DOI Pre-print

10:57 - 11:19
Talk

Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis

Roland Meyer, Sebastian WolffTU Braunschweig

11:19 - 11:41
Talk

Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs

Klaus v. GleissenthallUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA, Alexander Bakst, Deian StefanUniversity of California San Diego, Ranjit JhalaUniversity of California, San Diego

11:41 - 12:03
Talk

Weak-Consistency Specification via Visibility Relaxation

Michael EmmiSRI International, Constantin EneaUniversité Paris Diderot

10:35 - 12:03: Research Papers - Reasoning about Probabilistic Programs at POPL Track 1

10:35 - 10:57
Talk

Formal verification of higher-order probabilistic programs

Tetsuya SatoUniversity at Buffalo, SUNY, USA, Alejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Justin HsuUniversity of Wisconsin-Madison, USA

10:57 - 11:19
Talk

A Separation Logic for Concurrent Randomized Programs

Joseph TassarottiCarnegie Mellon University, Robert Harper

11:19 - 11:41
Talk

Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs

Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University, Christoph Matheja, Thomas NollRWTH Aachen University

11:41 - 12:03
Talk

Trace Abstraction Modulo Probability

Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison

13:45 - 14:51: Research Papers - Categories at POPL Track 2

13:45 - 14:07
Talk

Familial monads and structural operational semantics

Tom HirschowitzUniv. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry

14:07 - 14:29
Talk

Bindings as Bounded Natural Functors

Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Lorenzo GheriMiddlesex University London, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH Zurich

14:29 - 14:51
Talk

Categorical combinatorics of scheduling and synchronization in game semantics

MelliesCNRS and University Paris Diderot

13:45 - 14:51: Research Papers - Probabilistic Programming and Semantics at POPL Track 1

13:45 - 14:07
Talk

Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic

Maria I. GorinovaThe University of Edinburgh, Andrew D. GordonMicrosoft Research and University of Edinburgh, Charles SuttonUniversity of Edinburgh

DOI Pre-print

14:07 - 14:29
Talk

A Domain Theory for Statistical Probabilistic Programming

Matthijs VákárUniversity of Oxford, Ohad KammarUniversity of Oxford, Sam StatonUniversity of Oxford

Pre-print

14:29 - 14:51
Talk

Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling

Feras SaadMassachusetts Institute of Technology, Marco Cusumano-TownerMIT-CSAIL, Ulrich SchaechtleMassachusetts Institute of Technology, USA, Martin RinardMassachusetts Institute of Technology, Vikash MansingkhaMIT

Pre-print

15:21 - 16:27: Research Papers - Capabilities and Session Types I at POPL Track 2

15:21 - 15:43
Talk

StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities

Lau Skorstengaard, Dominique DevrieseVrije Universiteit Brussel, Belgium, Lars BirkedalAarhus University

15:43 - 16:05
Talk

Two sides of the same coin: Session Types and Game Semantics

Simon CastelanImperial College London, UK, Nobuko YoshidaImperial College London

DOI Pre-print

16:05 - 16:27
Talk

Exceptional Asynchronous Session Types: Session Types without Tiers

Simon FowlerThe University of Edinburgh, Sam LindleyUniversity of Edinburgh, UK, J. Garrett MorrisUniversity of Kansas, USA, Sara Décova

Pre-print

15:21 - 16:27: Research Papers - Machine Learning and Linear Algebra at POPL Track 1

15:21 - 15:43
Talk

code2vec: Learning Distributed Representations of Code

Uri AlonTechnion, Meital ZilbersteinTechnion, Omer LevyUniversity of Washington, USA, Eran YahavTechnion

15:43 - 16:05
Talk

An Abstract Domain for Certifying Neural Networks

Gagandeep Singh, Timon Gehr, Markus PüschelETH Zürich, Martin VechevETH Zürich

16:05 - 16:27
Talk

Closed Forms for Numerical Loops

Zachary KincaidPrinceton University, Jason BreckUniversity of Wisconsin - Madison, John CyphertUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.

16:37 - 17:43: Research Papers - Quantum Programming at POPL Track 1

16:37 - 16:59
Talk

Quantitative Robustness Analysis of Quantum Programs

Shih-Han HungUniversity of Maryland, Kesha HietalaUniversity of Maryland, Shaopeng ZhuUniversity of Maryland, Mingsheng YingUniversity of Technology Sydney, Michael HicksUniversity of Maryland, College Park, Xiaodi WuUniversity of Oregon, USA

16:59 - 17:21
Talk

Game Semantics for Quantum Programming

Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon, Glynn Winskel

17:21 - 17:43
Talk

Quantum Relational Hoare Logic

Dominique UnruhUniversity of Tartu

16:37 - 17:43: Research Papers - Session Types II at POPL Track 2

16:37 - 16:59
Talk

Interconnectability of Session-Based Logical ProcessesTOPLAS

Bernardo ToninhoNOVA-LINCS, FCT/UNL, Nobuko YoshidaImperial College London

DOI Pre-print

16:59 - 17:21
Talk

Distributed Programming using Role-Parametric Session Types in Go

David CastroImperial College London, Raymond HuImperial College London, Sung-Shik JongmansOpen University of the Netherlands, Nicholas NgImperial College London, Nobuko YoshidaImperial College London

DOI Pre-print

17:21 - 17:43
Talk

Less is More: Multiparty Session Types Revisited

Alceste ScalasImperial College London, Nobuko YoshidaImperial College London

DOI Pre-print

Thu 17 Jan

09:00 - 10:06: Research Papers - Synthesis at POPL Track 2

09:00 - 09:22
Talk

Structuring the Synthesis of Heap-Manipulating Programs

Nadia PolikarpovaUniversity of California, San Diego, Ilya SergeyYale-NUS College

DOI Pre-print

09:22 - 09:44
Talk

FrAngel: Component-Based Synthesis with Control Structures

Kensen ShiStanford University, Jacob SteinhardtStanford University, Percy LiangStanford University

09:44 - 10:06
Talk

Hamsaz: Replication Coordination Analysis and Synthesis

Farzin HoushmandUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside

09:00 - 10:06: Research Papers - Type Abstraction and Effects at POPL Track 1

09:00 - 09:22
Talk

Abstraction-Safe Effect Handlers via Tunneling

Yizhou ZhangCornell University, Andrew MyersCornell University

09:22 - 09:44
Talk

Abstracting Algebraic Effects

Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław

09:44 - 10:06
Talk

Fully Abstract Module Compilation

Karl CraryCarnegie Mellon University

10:36 - 12:04: Research Papers - Gradual Types at POPL Track 1

10:36 - 10:58
Talk

Type-Driven Gradual Security with ReferencesTOPLAS

Matías ToroUniversity of Chile, Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile & Inria Paris

10:58 - 11:20
Talk

Gradual Type Theory

Max S. NewNortheastern University, Dan LicataWesleyan University, Amal AhmedNortheastern University, USA

11:20 - 11:42
Talk

Gradual Parametricity, Revisited

Matías ToroUniversity of Chile, Elizabeth LabradaUniversity of Chile, Éric TanterUniversity of Chile & Inria Paris

DOI Pre-print

11:42 - 12:04
Talk

Live Functional Programming with Typed Holes

Cyrus OmarUniversity of Chicago, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago, Matthew HammerUniversity of Colorado, Boulder

Pre-print

10:36 - 12:04: Research Papers - Separation Logic and Memory Semantics at POPL Track 2

10:36 - 10:58
Talk

Iron: Managing Obligations in Higher-Order Concurrent Separation Logic

Aleš BizjakAarhus University, Daniel Gratzer, Robbert KrebbersDelft University of Technology, Lars BirkedalAarhus University

10:58 - 11:20
Talk

JaVerT 2.0: Compositional Symbolic Execution for JavaScript

José Fragoso SantosImperial College London, Petar MaksimovićImperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela SampaioImperial College London, UK, Philippa GardnerImperial College London

11:20 - 11:42
Talk

ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS

Alasdair Armstrong, Thomas BauereissUniversity of Cambridge, Brian CampbellUniversity of Edinburgh, Alastair ReidArm Ltd, Kathryn E. GrayUniversity of Cambridge, Robert M. NortonUniversity of Cambridge, Prashanth MundkurSRI International, Mark WassellUniversity of Cambridge, Jon FrenchUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Shaked FlurUniversity of Cambridge, Ian StarkThe University of Edinburgh, Neelakantan R. KrishnaswamiComputer Laboratory, University of Cambridge, Peter SewellUniversity of Cambridge

11:42 - 12:04
Talk

Exploring C Semantics and Pointer Provenance

Kayvan MemarianUniversity of Cambridge, Victor B. F. GomesUniversity of Cambridge, UK, Brooks DavisSRI International, Stephen KellUniversity of Kent, Alexander RichardsonUniversity of Cambridge, Robert N. M. WatsonUniversity of Cambridge, Peter SewellUniversity of Cambridge

13:45 - 14:51: Research Papers - Type Inference I at POPL Track 1

13:45 - 14:07
Talk

Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types

Joshua DunfieldQueen's University, Kingston, Ontario, Neelakantan R. KrishnaswamiComputer Laboratory, University of Cambridge

14:07 - 14:29
Talk

Abstracting Extensible Data Types; Or, Rows By Any Other Name

J. Garrett MorrisUniversity of Kansas, USA, James McKinna

14:29 - 14:51
Talk

Polymorphic Symmetric Multiple Dispatch with Variance

Gyunghee ParkKAIST, Oracle Labs, Jaemin HongKAIST, South Korea, Guy L. Steele Jr.Oracle Labs, Sukyoung RyuKAIST, South Korea

13:45 - 14:51: Research Papers - Weak Memory at POPL Track 2

13:45 - 14:07
Talk

On Library Correctness under Weak Memory Consistency

Azalea RaadMPI-SWS, Germany, Marko DokoMPI-SWS, Germany, Lovro RožićMPI-SWS, Germany, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, Germany

14:07 - 14:29
Talk

Bridging the Gap Between Programming Languages and Hardware Weak Memory Models

Anton PodkopaevJetBrains Resereach, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, Germany

14:29 - 14:51
Talk

Grounding Thin-Air Reads with Event Structures

Soham ChakrabortyMax Planck Institute for Software Systems, Viktor VafeiadisMPI-SWS, Germany

15:21 - 16:49: Research Papers - Time at POPL Track 2

15:21 - 15:43
Talk

Type-Guided Worst-Case Input Generation

Di WangCarnegie Mellon University, Jan HoffmannCarnegie Mellon University

Pre-print

15:43 - 16:05
Talk

CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem

Conrad WattUniversity of Cambridge, John RennerUniversity of California, San Diego, Natalie PopescuUniversity of California San Diego, Sunjay CauligiUCSD, Deian StefanUniversity of California San Diego

16:05 - 16:27
Talk

Modular Quantitative Monitoring

Rajeev AlurUniversity of Pennsylvania, Konstantinos MamourasUniversity of Pennsylvania, Caleb StanfordUniversity of Pennsylvania

16:27 - 16:49
Talk

CSS Minification via Constraint SolvingTOPLAS

Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Chih-Duo HongUniversity of Oxford

15:21 - 16:49: Research Papers - Type Inference II at POPL Track 1

15:21 - 15:43
Talk

Dynamic Type Inference for Gradual Hindley–Milner Typing

Yusuke MiyazakiKyoto University, Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan

15:43 - 16:05
Talk

Gradual Typing: A New Perspective

Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France, Tommaso PetruccianiDIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. SiekIndiana University, USA

16:05 - 16:27
Talk

Intersection Types and Runtime Errors in the Pi-Calculus

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Marc De VismeENS Lyon, Damiano MazzaCNRS, Akira YoshimizuINRIA

16:27 - 16:49
Talk

Principality and Approximation under Dimensional Bound

Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund

17:00 - 18:00: Research Papers - Business Meeting at POPL

17:00 - 17:15
Other

PC Chair Report

Stephanie WeirichUniversity of Pennsylvania, USA

17:15 - 17:25
Awards

SIGPLAN Awards

17:25 - 17:30
Other

POPL 2020 Announcement

Brigitte PientkaMcGill University, Lars BirkedalAarhus University

17:30 - 17:40
Other

NSF funding for PL

Rance CleavelandUniversity of Maryland

17:40 - 17:50
Other

SIGPLAN Climate Committee Report

Benjamin C. PierceUniversity of Pennsylvania

17:50 - 18:00
Meeting

Town Hall

Fri 18 Jan

09:00 - 10:05: Research Papers - SRC Announcement & Keynote II at POPL

09:00 - 09:05
Awards

SRC Announcement

09:05 - 10:05
Talk

Mechanized Metatheory - The Next Chapter

Brigitte PientkaMcGill University

10:35 - 12:03: Research Papers - Abstract Interpretation at POPL Track 2

10:35 - 10:57
Talk

A$^2$I: Abstract$^2$ Interpretation

Patrick Cousot, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Francesco RanzatoUniversity of Padova

10:57 - 11:19
Talk

Concerto: A Framework for Combined Concrete and Abstract Interpretation

John TomanUniversity of Washington, Seattle, Dan GrossmanUniversity of Washington

11:19 - 11:41
Talk

Skeletal Semantics and their Interpretations

Martin BodinImperial College London, Philippa GardnerImperial College London, Thomas P. JensenINRIA Rennes, Alan SchmittInria

DOI Pre-print

11:41 - 12:03
Talk

Refinement of Path Expressions for Static Analysis

John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Zachary KincaidPrinceton University, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.

10:35 - 12:03: Research Papers - Dependent Types at POPL Track 1

10:35 - 10:57
Talk

Higher Inductive Types in Cubical Computational Type Theory

Evan CavalloCarnegie Mellon University, Robert Harper

10:57 - 11:19
Talk

Constructing Quotient Inductive-Inductive Types

Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham, András KovácsEötvös Loránd University

11:19 - 11:41
Talk

Definitional Proof-Irrelevance without K

Gaetan Gilbert, Jesper CockxChalmers | University of Gothenburg, Matthieu SozeauInria, Nicolas TabareauInria

11:41 - 12:03
Talk

Bisimulation as path type for guarded recursive types

Rasmus Ejlers MøgelbergIT University of Copenhagen, Niccolò VeltriIT University of Copenhagen

13:45 - 14:51: Research Papers - Model Checking at POPL Track 2

13:45 - 14:07
Talk

Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations

Taolue ChenBirkbeck, University of London, Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Philipp RuemmerUppsala University, Zhilin WuState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

14:07 - 14:29
Talk

Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation

Kyungmin BaePohang University of Science and Technology (POSTECH), Jia LeePohang University of Science and Technology (POSTECH)

14:29 - 14:51
Talk

Adventures in Monitorability: From Branching to Linear Time and Back Again

Luca AcetoReykjavik University, Antonis AchilleosReykjavik University, Adrian FrancalanzaUniversity of Malta, Anna IngolfsdottirReykjavik University, Karoliina LehtinenUniversity of Kiel and University of Liverpool

13:45 - 14:51: Research Papers - Semantics at POPL Track 1

13:45 - 14:07
Talk

Better Late Than Never: A Fully Abstract Semantics for Classical Processes

Wen KokkeUniversity of Edinburgh, Fabrizio MontesiUniversity of Southern Denmark, Marco PeressottiUniversity of Southern Denmark

DOI

14:07 - 14:29
Talk

Diagrammatic Algebra: From Linear to Concurrent Systems

Filippo BonchiUniversity of Pisa, Joshua HollandUniversity of Southampton, Robin PiedeleuUniversity of Oxford, Pawel SobocinskiUniversity of Southampton, Fabio ZanasiUniversity College London

14:29 - 14:51
Talk

Fixpoint Games on Continuous Lattices

Paolo Baldan, Barbara KoenigUniversity of Duisburg-Essen, Christina Mika-MichalskiUniversity of Duisburg-Essen, Tommaso PadoanUniversity of Padova

15:21 - 16:27: Research Papers - Program Analysis I at POPL Track 2

15:21 - 15:43
Talk

Decidable Verification of Uninterpreted Programs

Umang MathurUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign

Pre-print

15:43 - 16:05
Talk

Inferring frame conditions with static correlation analysis

Oana-Fabiana AndreescuInternet of Trust, Thomas P. JensenINRIA Rennes, Stéphane LescuyerProve & Run, Benoît MontaguProve & Run

16:05 - 16:27
Talk

Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems

Johannes SpäthFraunhofer IEM, Karim AliUniversity of Alberta, Eric BoddenHeinz Nixdorf Institut, Paderborn University and Fraunhofer IEM

Pre-print

15:21 - 16:27: Research Papers - Security and Information Flow at POPL Track 1

15:21 - 15:43
Talk

LWeb: Information Flow Security for Multi-Tier Web Applications

James ParkerUniversity of Maryland, Niki VazouIMDEA Software Institute, Michael HicksUniversity of Maryland, College Park

15:43 - 16:05
Talk

From Fine- to Coarse-Grained Dynamic Information Flow Control and Back

Marco VassenaChalmers University of Technology, Alejandro RussoChalmers University of Technology, Sweden, Deepak GargMax Planck Institute for Software Systems, Vineet RajaniMPI-SWS, Deian StefanUniversity of California San Diego

16:05 - 16:27
Talk

Modalities, Cohesion, and Information Flow

G. A. KavvosWesleyan University

DOI Pre-print

16:37 - 17:43: Research Papers - Program Analysis II at POPL Track 2

16:37 - 16:59
Talk

Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries

Xin YiNational University of Defense Technology, Liqian ChenNational University of Defense Technology, Xiaoguang MaoNational University of Defense Technology, Tao JiNational University of Defense Technology

16:59 - 17:21
Talk

Efficient Parameterized Algorithms for Data Packing

Krishnendu ChatterjeeIST Austria, Amir Kafshdar GoharshadyIST Austria, Nastaran OkatiFerdowsi University of Mashhad, Andreas PavlogiannisEPFL, Switzerland

17:21 - 17:43
Talk

Fast and exact analysis for LRU caches

Valentin TouzeauUniv. Grenoble Alpes, Claire MaizaVerimag, France, David MonniauxCNRS, VERIMAG, Jan ReinekeSaarland University

16:37 - 17:43: Research Papers - Verified Compilation and Concurrency at POPL Track 1

16:37 - 16:59
Talk

A Calculus for Esterel: If can, can. If no can, no can.

Spencer P. FlorenceNorthwestern University, USA, Shu-Hung YouNorthwestern University, USA, Jesse A. TovNorthwestern University, Department of Electrical Engineering and Computer Science, Robby FindlerNorthwestern University, USA

16:59 - 17:21
Talk

An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code

Yuting WangYale University, Pierre WilkeYale University, Zhong ShaoYale University

17:21 - 17:43
Talk

A Verified, Efficient Embedding of a Verifiable Assembly Language

Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research

Sat 19 Jan

09:00 - 10:30: CoqPL - Keynote & Contributed talks 1 at CoqPL

09:00 - 09:05
Day opening

Opening

09:05 - 10:05
Talk

Coq User Interfaces: Past, Present, and Future (Keynote)

Emilio Jesús Gallego AriasMINES ParisTech

10:05 - 10:30
Talk

Counterexamples for Coq Conjectures

Sam GruetterMassachusetts Institute of Technology

File Attached

11:15 - 12:30: CoqPL - Contributed talks 2 at CoqPL
Chair(s): Robbert KrebbersDelft University of Technology

11:15 - 11:40
Talk

Towards Mechanising Probabilistic Properties of a Blockchain

Kiran GopinathanUniversity College London, Ilya SergeyYale-NUS College

File Attached

11:40 - 12:05
Talk

Verifying Finality for Blockchain Systems

Karl PalmskogUniversity of Texas at Austin, Milos GligoricUniversity of Texas at Austin, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-Champaign

File Attached

12:05 - 12:30
Talk

WIP: Formalizing the Concordium consensus protocol in Coq

Thomas Dinsdale-Young, Bas Spitters, Søren Eller ThomsenAarhus University, Daniel TschudiAarhus University

File Attached

14:00 - 15:30: CoqPL - Contributed talks 3 & Coq developers at CoqPL

14:00 - 14:25
Talk

Reification of shallow-embedded DSLs in Coq with automated verification

Vadim ZalivaCarnegie Mellon University, USA, Matthieu SozeauInria

File Attached

14:25 - 14:50
Talk

Reifying and translating a monadic fragment of Gallina

Paolo TorriniSwansea University

File Attached

14:50 - 15:30
Demonstration

Session with the Coq Development Team

Maxime DénèsINRIA, Matthieu SozeauInria

16:00 - 17:40: CoqPL - Contributed talks 4 at CoqPL

16:00 - 16:25
Talk

Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs

Qinxiang Cao

File Attached

16:25 - 16:50
Talk

Teaching Discrete Mathematics to Early Undergraduates with Software Foundations

Michael GreenbergPomona College, Joseph C. OsbornPomona College

File Attached

16:50 - 17:15
Talk

Ltac2: Tactical Warfare

Pierre-Marie Pédrot

File Attached

17:15 - 17:40
Talk

Towards a Coq Formalisation of Build Systems

Georgy LukyanovNewcastle University, UK, Andrey MokhovNewcastle University, UK

File Attached

Sun 13 Jan 2019


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
BEAT		BEAT Session 1 08:30 - 10:30					BEAT Session 2 11:00 - 12:30					BEAT Session 3 13:30 - 15:30					BEAT Session 4 16:00 - 18:25
PriSC			PriSC Session 1 09:00 - 10:30				PriSC Session 2 11:00 - 12:30						PriSC Session 3 14:00 - 15:30				PriSC Session 4 16:00 - 17:30
VMCAI			VMCAI Invited Talk 1 09:00 - 10:30				VMCAI Abstract interpretation (1) 11:00 - 12:30						VMCAI Program Synthesis 14:00 - 15:30				VMCAI Abstract Interpretation (2) 16:00 - 17:30

Mon 14 Jan 2019


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
CPP	CPP Keynote 1 and Research Paper 09:00 - 10:30				CPP Research Papers: Proof Theory, Theory of Programming Languages 11:00 - 12:30						CPP Research Papers: Program Verification 14:00 - 15:30				CPP Research Papers: Formalization of Mathematics and Computer Algebra 16:00 - 17:30
OPCT	OPCT 09:00 - 10:30				OPCT 11:00 - 12:30						OPCT 14:00 - 15:30				OPCT 16:00 - 17:30
PADL	PADL 09:00 - 10:30				PADL 11:00 - 12:30						PADL PADL Session 1 14:00 - 15:30				PADL PADL Session 2 16:00 - 17:30
PEPM	PEPM 09:00 - 10:30				PEPM Session 1 11:00 - 12:30						PEPM Session 2 14:00 - 15:30				PEPM Session 3 16:00 - 17:30
TutorialFest 1	POPL TutorialFest QuickChick: Property-Based Testing in Coq I 09:00 - 10:30				POPL TutorialFest QuickChick: Property-Based Testing in Coq II 11:00 - 12:30						POPL TutorialFest Correct-by-Construction Programming in Agda I 14:00 - 15:30				POPL TutorialFest Correct-by-Construction Programming in Agda II 16:00 - 17:30
TutorialFest 2	POPL TutorialFest Engineering Distributed Systems via Protocols and Commitments I 09:00 - 10:30				POPL TutorialFest Engineering Distributed Systems via Protocols and Commitments II 11:00 - 12:30						POPL TutorialFest Session-Typed Concurrent Programming I 14:00 - 15:30				POPL TutorialFest Session-Typed Concurrent Programming II 16:00 - 17:30
TutorialFest 3	POPL TutorialFest Linear and Graded Modal Types for Fine-Grained Program Reasoning I 09:00 - 10:30				POPL TutorialFest Linear and Graded Modal Types for Fine-Grained Program Reasoning II 11:00 - 12:30						POPL TutorialFest Higher-Order Probabilistic Programming I 14:00 - 15:30				POPL TutorialFest Higher-Order Probabilistic Programming II 16:00 - 17:30
TutorialFest 4	POPL TutorialFest Programming Cyber-Physical Systems With Logic I 09:00 - 10:30				POPL TutorialFest Programming Cyber-Physical Systems With Logic II 11:00 - 12:30						POPL TutorialFest Building Your Own Modular Static Analyser with Infer I 14:00 - 15:30				POPL TutorialFest Building Your Own Modular Static Analyser with Infer II 16:00 - 17:30
VMCAI	VMCAI Invited Talk 2 09:00 - 10:30				VMCAI Decision Procedures 11:00 - 12:30						VMCAI Probabilistic Systems 14:00 - 15:30				VMCAI Model Checking 16:00 - 17:30

Tue 15 Jan 2019


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
CPP	CPP Keynote 2 and Research Paper 09:00 - 10:30				CPP Research Papers: Rewriting, Automated Reasoning 11:00 - 12:30						CPP Research Papers: Program Verification 14:00 - 15:30				CPP Research Papers: Formalization of Mathematics and Computer Algebra 16:00 - 17:30
LAFI	LAFI Archimedes 09:00 - 10:30				LAFI Borel 11:00 - 12:30						LAFI Cauchy 14:00 - 15:30				LAFI Dirichlet 16:00 - 17:30
OPCT	OPCT 09:00 - 10:30				OPCT 11:00 - 12:30						OPCT 14:00 - 15:30				OPCT 16:00 - 17:30
PADL	PADL PADL Session 3 09:00 - 10:30				PADL PADL Session 4 11:00 - 12:30						PADL PADL Session 5 14:00 - 15:30				PADL 16:00 - 17:30
PEPM	PEPM 09:00 - 10:30				PEPM Session 4 11:00 - 12:30						PEPM Session 5 14:00 - 15:30				PEPM Session 6 16:00 - 17:30
PLMW	PLMW PLMW Session 1 09:00 - 10:30				PLMW PLMW Session 2 11:00 - 12:30						PLMW PLMW Session 3 14:00 - 15:30				PLMW PLMW Session 4 16:00 - 17:30
VMCAI	VMCAI Invited Talk 3 09:00 - 10:30				VMCAI Software Verification and Synthesis 11:00 - 12:30						VMCAI Software Verification 14:00 - 15:30				VMCAI Networks and Concurrency 16:00 - 17:30

Wed 16 Jan 2019


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
POPL	POPL Research Papers Welcome & Keynote I 09:00 - 10:05
POPL Track 1					POPL Research Papers Reasoning about Probabilistic Programs 10:35 - 12:03							POPL Research Papers Probabilistic Programming and Semantics 13:45 - 14:51				POPL Research Papers Machine Learning and Linear Algebra 15:21 - 16:27				POPL Research Papers Quantum Programming 16:37 - 17:43
POPL Track 2					POPL Research Papers Concurrency 10:35 - 12:03							POPL Research Papers Categories 13:45 - 14:51				POPL Research Papers Capabilities and Session Types I 15:21 - 16:27				POPL Research Papers Session Types II 16:37 - 17:43

Thu 17 Jan 2019


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
POPL														POPL Research Papers Business Meeting 17:00 - 18:00
POPL Track 1	POPL Research Papers Type Abstraction and Effects 09:00 - 10:06				POPL Research Papers Gradual Types 10:36 - 12:04							POPL Research Papers Type Inference I 13:45 - 14:51					POPL Research Papers Type Inference II 15:21 - 16:49
POPL Track 2	POPL Research Papers Synthesis 09:00 - 10:06				POPL Research Papers Separation Logic and Memory Semantics 10:36 - 12:04							POPL Research Papers Weak Memory 13:45 - 14:51					POPL Research Papers Time 15:21 - 16:49

Fri 18 Jan 2019


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
POPL	POPL Research Papers SRC Announcement & Keynote II 09:00 - 10:05
POPL Track 1					POPL Research Papers Dependent Types 10:35 - 12:03							POPL Research Papers Semantics 13:45 - 14:51				POPL Research Papers Security and Information Flow 15:21 - 16:27				POPL Research Papers Verified Compilation and Concurrency 16:37 - 17:43
POPL Track 2					POPL Research Papers Abstract Interpretation 10:35 - 12:03							POPL Research Papers Model Checking 13:45 - 14:51				POPL Research Papers Program Analysis I 15:21 - 16:27				POPL Research Papers Program Analysis II 16:37 - 17:43

Sat 19 Jan 2019


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
CoqPL	CoqPL Keynote & Contributed talks 1 09:00 - 10:30					CoqPL Contributed talks 2 11:15 - 12:30						CoqPL Contributed talks 3 & Coq developers 14:00 - 15:30				CoqPL Contributed talks 4 16:00 - 17:40
OBT	Off the Beaten Track 09:00 - 10:30				Off the Beaten Track 11:00 - 12:30							Off the Beaten Track 14:00 - 15:30				Off the Beaten Track 16:00 - 17:30

Sun 13 Jan 2019


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
BEAT			BEAT Opening 08:30 - 08:40	BEAT Invited Talk: Gradual Session Types — an Ongoing Journey 08:40 - 09:30				BEAT Gradual Session Types in Imperative Style 09:30 - 09:50		BEAT Checking the equivalence of context-free session types 09:50 - 10:10		BEAT Effpi: concurrent programming with dependent behavioural types 10:10 - 10:30				BEAT Invited Talk: On Type-Based Complexity Analysis of Programs and Processes 11:00 - 11:50				BEAT Global Types with Internal Delegation 11:50 - 12:10		BEAT Two Declarative Approaches for Session-Based Concurrency 12:10 - 12:30						BEAT Invited Talk: TBA 13:30 - 14:20				BEAT Invited Talk: A Session Type Provider: Compile-time Generation of Sessi ... 14:20 - 15:10				BEAT Getting rid of null-dereferences – Behavioural types to the rescue 15:10 - 15:30				BEAT Invited Talk: Session Types for Fault-Tolerant Distributed Algorithms 16:00 - 16:50				BEAT Behavioral Types as a Semantic Foundation for the GDPR notion of Purpose 16:50 - 17:10		BEAT Relating Process Languages for Security and Communication Correctness 17:10 - 17:30		BEAT Short break 17:30 - 17:40	BEAT Towards Legally Compliant Governmental Case Work with Dynamic Condition ... 17:40 - 18:00		BEAT Hardware interactions as behavioural types 18:00 - 18:20		BEAT Closing 18:20 - 18:25
PriSC						PriSC PriSC Keynote - Jasmin: A Compiler and Framework for High-Assurance and ... 09:00 - 10:00
VMCAI						VMCAI Under and Over Approximated Reachability Analysis for the Verifcation o ... 09:00 - 10:30										VMCAI Static Analysis Of Binary Code With Memory Indirections Using Polyhedra 11:00 - 11:30		VMCAI Disjunctive Relational Abstract Interpretation for Interprocedural Prog ... 11:30 - 12:00			VMCAI Application of Abstract Interpretation to the Automotive Electronic Con ... 12:00 - 12:30									VMCAI Minimal Synthesis of String To String Functions From Examples 14:00 - 14:30			VMCAI Lazy but Effective Functional Synthesis 14:30 - 15:00		VMCAI Automatic Program Repair using Formal Verification and Expression Templates 15:00 - 15:30					VMCAI Demand Control-Flow Analysis 16:00 - 16:30		VMCAI Relatively Complete Pushdown Analysis of Escape Continuations 16:30 - 17:00			VMCAI Effect-driven Flow Analysis 17:00 - 17:30

Mon 14 Jan 2019


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
CPP	CPP A Linear Logical Framework in Hybrid 09:00 - 10:00				CPP Certified Undecidability of Intuitionistic Linear Logic via Binary Stac ... 10:00 - 10:30				CPP A proof-theoretic approach to certifying skolemization 11:00 - 11:30		CPP Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory 11:30 - 12:00		CPP Eliminating Reflection from Type Theory 12:00 - 12:30								CPP Formally Verified Big Step Semantics out of x86-64 Binaries 14:00 - 14:30		CPP Formal Verification of a Program Obfuscation Based on Mixed Boolean-Ari ... 14:30 - 15:00		CPP From C to Interaction Trees: Specifying, Verifying, and Testing a Netwo ... 15:00 - 15:30				CPP A formal proof of Hensel's lemma over the p-adic integers 16:00 - 16:30		CPP Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan- ... 16:30 - 17:00		CPP Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL 17:00 - 17:30
PADL																					PADL Natural Language Generation From Ontologies 14:00 - 14:30		PADL Incremental Evaluation of Lattice-Based Aggregates in Logic Programming ... 14:30 - 15:00		PADL Improving Residuation in Declarative Programs 15:00 - 15:30				PADL Faster Coroutine Pipelines: A Reconstruction 16:00 - 16:30		PADL Distributed Protocol Combinators 16:30 - 17:00		PADL Classes of Arbitrary Kind 17:00 - 17:30
PEPM									PEPM Applying Futamura projections to compose languages and tools in GraalVM ... 11:00 - 12:00				PEPM A Simpler Lambda Calculus 12:00 - 12:30								PEPM Method Name Suggestion with Hierarchical Attention Networks 14:00 - 14:30		PEPM Reduction from Branching-Time Property Verification of Higher-Order Pro ... 14:30 - 15:00		PEPM Typed Parsing and Unparsing for Untyped Regular Expression Engines 15:00 - 15:30				PEPM What is the type of a partial evaluator? (Invited Talk) 16:00 - 17:00				PEPM Combining Higher-Order Model Checking with Refinement Type Inference 17:00 - 17:30
TutorialFest 1	POPL TutorialFest [T1] QuickChick: Property-Based Testing in Coq 09:00 - 10:30								POPL TutorialFest [T1] QuickChick: Property-Based Testing in Coq 11:00 - 12:30												POPL TutorialFest [T5] Correct-by-Construction Programming in Agda 14:00 - 15:30								POPL TutorialFest [T5] Correct-by-Construction Programming in Agda 16:00 - 17:30
TutorialFest 2	POPL TutorialFest [T2] Engineering Distributed Systems via Protocols and Commitments 09:00 - 10:30								POPL TutorialFest [T2] Engineering Distributed Systems via Protocols and Commitments 11:00 - 12:30												POPL TutorialFest [T6] Session-Typed Concurrent Programming 14:00 - 15:30								POPL TutorialFest [T6] Session-Typed Concurrent Programming 16:00 - 17:30
TutorialFest 3	POPL TutorialFest [T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning 09:00 - 10:30								POPL TutorialFest [T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning 11:00 - 12:30												POPL TutorialFest [T7] Higher-Order Probabilistic Programming 14:00 - 15:30								POPL TutorialFest [T7] Higher-Order Probabilistic Programming 16:00 - 17:30
TutorialFest 4	POPL TutorialFest [T4] Programming Cyber-Physical Systems With Logic 09:00 - 10:30								POPL TutorialFest [T4] Programming Cyber-Physical Systems With Logic 11:00 - 12:30												POPL TutorialFest [T8] Building Your Own Modular Static Analyser with Infer 14:00 - 15:30								POPL TutorialFest [T8] Building Your Own Modular Static Analyser with Infer 16:00 - 17:30
VMCAI	VMCAI Designing Self-Certifying Software Systems 09:00 - 10:30								VMCAI Solving and Interpolating Constant Arrays Based on Weak Equivalences 11:00 - 11:30		VMCAI A Decidable Logic for Tree Data-Structures with Measurements 11:30 - 12:00		VMCAI A Practical Algorithm for Structure Embedding 12:00 - 12:30								VMCAI Syntactic Partial Order Compression for Probabilistic Reachability 14:00 - 14:30		VMCAI Termination of Nondeterministic Probabilistic Programs 14:30 - 15:00		VMCAI Combining Refinement of Parametric Models with Goal-Oriented Reduction ... 15:00 - 15:30				VMCAI Parametric Timed Broadcast Protocols 16:00 - 16:30		VMCAI Flat Model Checking for Counting LTL using Quantifier-free Presburger A ... 16:30 - 17:00		VMCAI A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization 17:00 - 17:30

Tue 15 Jan 2019


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
CPP	CPP Formalizing the Metatheory of Logical Calculi and Automatic Provers in ... 09:00 - 10:00					CPP A Verified Prover Based on Ordered Resolution 10:00 - 10:30				CPP Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Sub ... 11:00 - 11:30		CPP Certified ACKBO 11:30 - 12:00		CPP A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite ... 12:00 - 12:30								CPP A Verified Protocol Buffer Compiler 14:00 - 14:30		CPP A Coq mechanised formal semantics for realistic SQL queries - Formally ... 14:30 - 15:00		CPP Dynamic Class Initialization Semantics: a Jinja Extension 15:00 - 15:30				CPP On Synthetic Undecidability in Coq, with an Application to the Entschei ... 16:00 - 16:30		CPP Verified Solving and Asymptotics of Linear Recurrences 16:30 - 17:00		CPP Business Meeting 17:00 - 17:30
LAFI	LAFI Probabilistic Lambda Calculus: Beyond Deterministic Evaluation 09:00 - 09:10	LAFI The Geometry of Bayesian Programming 09:10 - 09:30		LAFI Invited talk: Connecting probabilistic programming theory to applicatio ... 09:30 - 10:30						LAFI Strongly typed tracing of probabilistic programs 11:00 - 11:30		LAFI Model and Inference Combinators for Deep Probabilistic Programming 11:30 - 12:00		LAFI Server-side Probabilistic Programming 12:00 - 12:30								LAFI A Nuts-and-Bolts Differential Geometric Perspective on Automatic Differ ... 14:00 - 14:30		LAFI Kotlin∇: Differentiable functional programming with algebraic data types 14:30 - 15:00		LAFI Probabilistic Programming with CuPPL 15:00 - 15:30				LAFI Probabilistic Programming Inference via Intensional Semantics 16:00 - 16:30		LAFI Factorized Exact Inference for Discrete Probabilistic Programs 16:30 - 17:00		LAFI Verified equational reasoning on a little language of measures 17:00 - 17:30
PADL				PADL Personalized Course Schedule Planning using Answer Set Programming 09:30 - 10:00		PADL Static Partitioning of Spreadsheets for Parallel Execution 10:00 - 10:30				PADL An ASP-based Approach to Representing and Querying Textual Knowledge 11:00 - 11:30		PADL Strong Equivalence and Program's Structure in Arguing Essential Equivalence 11:30 - 12:00		PADL Automatic Program Rewriting in Non-Ground Answer Set Programs 12:00 - 12:30								PADL Composing Syntactical Constructs to Create Domain-Specific Languages 14:00 - 14:30		PADL Proof Carrying Plans 14:30 - 15:00		PADL A Combinatorial Testing Framework for Intuitionistic Propositional Theo ... 15:00 - 15:30
PEPM										PEPM Making proofs easy: Horn clause transformations to the aid of program v ... 11:00 - 12:00				PEPM Control Flow Obfuscation via CPS Transformation 12:00 - 12:30								PEPM Extracting a Call-by-Name Partial Evaluator from a Proof of Termination 14:00 - 14:30		PEPM Futures and Promises in Haskell and Scala 14:30 - 15:00		PEPM Generating Mutually Recursive Definitions 15:00 - 15:30				PEPM PEPM Poster Session 16:00 - 17:30
PLMW	PLMW PLMW Welcome 09:00 - 09:15		PLMW Technical Talk: Verification of Distributed Protocols Using Decidable Logic 09:15 - 10:00			PLMW Research Skills: How to Give a Talk 10:00 - 10:30				PLMW Research Skills: Work/Life Balance 11:00 - 11:30		PLMW Panel: Grad School and Beyond 11:30 - 12:30										PLMW Technical Talk: How to Think about Types 14:00 - 14:45			PLMW Technical Talk: What Is Programming Languages Research? 14:45 - 15:30					PLMW Panel: How to Do Great PL Research 16:00 - 16:30		PLMW Research Skills: How to Bootstrap a Research Project 16:30 - 17:30
VMCAI	VMCAI Semantics for Compiler IRs: Undefined Behavior is not Evil! 09:00 - 10:30									VMCAI Mechanically Proving Determinacy of Hierarchical Block Diagram Translations 11:00 - 11:30		VMCAI euforia: Complete Software Model Checking with Uninterpreted Functions 11:30 - 12:00		VMCAI Program Synthesis with Equivalence Reduction 12:00 - 12:30								VMCAI Type-directed Bounding of Collections in Reactive Programs 14:00 - 14:30		VMCAI Exploiting Pointer Analysis in Memory Models for Deductive Verification 14:30 - 15:00		VMCAI Small Faults Grow Up - Verification of Error Masking Robustness in Arit ... 15:00 - 15:30				VMCAI On the Semantics of Snapshot Isolation 16:00 - 16:30		VMCAI Fast BGP Simulation of Large Datacenters 16:30 - 17:00		VMCAI Verification of an Industrial Asynchronous Leader Election Algorithm Us ... 17:00 - 17:30

Wed 16 Jan 2019


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
POPL	POPL Research Papers Welcome 09:00 - 09:05	POPL Research Papers Automated Fault-Finding and Fixing at Facebook 09:05 - 10:05
POPL Track 1									POPL Research Papers Formal verification of higher-order probabilistic programs 10:35 - 10:57		POPL Research Papers A Separation Logic for Concurrent Randomized Programs 10:57 - 11:19			POPL Research Papers Quantitative Separation Logic - A Logic for Reasoning about Probabilist ... 11:19 - 11:41		POPL Research Papers Trace Abstraction Modulo Probability 11:41 - 12:03									POPL Research Papers Probabilistic Programming with Densities in SlicStan: Efficient, Flexib ... 13:45 - 14:07		POPL Research Papers A Domain Theory for Statistical Probabilistic Programming 14:07 - 14:29		POPL Research Papers Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling 14:29 - 14:51				POPL Research Papers code2vec: Learning Distributed Representations of Code 15:21 - 15:43		POPL Research Papers An Abstract Domain for Certifying Neural Networks 15:43 - 16:05		POPL Research Papers Closed Forms for Numerical Loops 16:05 - 16:27			POPL Research Papers Quantitative Robustness Analysis of Quantum Programs 16:37 - 16:59		POPL Research Papers Game Semantics for Quantum Programming 16:59 - 17:21		POPL Research Papers Quantum Relational Hoare Logic 17:21 - 17:43
POPL Track 2									POPL Research Papers A True Positives Theorem for a Static Race Detector 10:35 - 10:57		POPL Research Papers Decoupling Lock-Free Data Structures from Memory Reclamation for Static ... 10:57 - 11:19			POPL Research Papers Pretend Synchrony: Synchronous Verification of Asynchronous Distributed ... 11:19 - 11:41		POPL Research Papers Weak-Consistency Specification via Visibility Relaxation 11:41 - 12:03									POPL Research Papers Familial monads and structural operational semantics 13:45 - 14:07		POPL Research Papers Bindings as

POPL 2019 Program

Sun 13 Jan

Mon 14 Jan

Tue 15 Jan

Wed 16 Jan

Thu 17 Jan

Fri 18 Jan

Sat 19 Jan

Sun 13 Jan 2019

BEAT

BEAT

BEAT

BEAT

PriSC

PriSC

PriSC

PriSC

VMCAI

VMCAI

VMCAI

VMCAI

Mon 14 Jan 2019

CPP

CPP

CPP

CPP

OPCT

OPCT

OPCT

OPCT

PADL

PADL

PADL

PADL

PEPM

PEPM

PEPM

PEPM

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

VMCAI

VMCAI

VMCAI

VMCAI

Tue 15 Jan 2019

CPP

CPP

CPP

CPP

LAFI

LAFI

LAFI

LAFI

OPCT

OPCT

OPCT

OPCT

PADL

PADL

PADL

PADL

PEPM

PEPM

PEPM

PEPM

PLMW