Program - POPL 2019

Filter

Sun 13 Jan

08:30 - 10:30: BEAT 2019 - Session 1 at Sala VII
Chair(s): Philip WadlerUniversity of Edinburgh, UK

08:30 - 08:40
Day opening

Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. PérezUniversity 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

File Attached

10:10 - 10:30
Talk

Effpi: Concurrent Programming with Dependent Behavioural Types

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

File Attached

09:00 - 10:30: VMCAI 2019 - Invited Talk 1 at Sala III
Chair(s): Constantin EneaUniversité Paris Diderot

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 Sala VI
Chair(s): Deepak GargMax Planck Institute for Software Systems

09:00 - 10:00
Talk

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

Benjamin GregoireINRIA

File Attached

10:00 - 10:30
Talk

Towards Secure Compilation of Power Side-Channel Countermeasures

Marc GourjonHamburg University of Technology and NXP Semiconductors Germany GmbH

File Attached

11:00 - 12:30: VMCAI 2019 - Abstract Interpretation (1) at Sala III
Chair(s): Patrick M. Cousot

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

File Attached

11:30 - 12:00
Talk

Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis

Rémy Boutonnet, Nicolas Halbwachs

File Attached

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 Sala VI
Chair(s): Dominique DevrieseVrije Universiteit Brussel, Belgium

11:00 - 11:30
Talk

Trestle: Bridging the Performance and Safety Divide in WebAssembly

Craig DisselkoenUniversity of California San Diego, Tal GarfinkelStanford University, Deian StefanUniversity of California San Diego, Conrad WattUniversity of Cambridge

File Attached

11:30 - 12:00
Talk

Protecting C++ Applications Using CHERI

Khilan GudkaUniversity of Cambridge, Alexander RichardsonUniversity of Cambridge, Robert N. M. WatsonUniversity of Cambridge

File Attached

12:00 - 12:30
Talk

Secure Linking in the CheriBSD Operating System

Alexander RichardsonUniversity of Cambridge, Robert N. M. WatsonUniversity of Cambridge

File Attached

11:00 - 12:30: BEAT 2019 - Session 2 at Sala VII
Chair(s): Dominic OrchardUniversity of Kent, UK

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

File Attached

12:10 - 12:30
Talk

Two Declarative Approaches for Session-Based Concurrency

Mauricio CanoUniversity of Groningen, The Netherlands

12:30 - 14:00: Workshops - Sunday Lunch at Lunch Room

12:30 - 14:00
Lunch

Lunch

13:30 - 15:30: BEAT 2019 - Session 3 at Sala VII
Chair(s): Paola GianniniUniversita' del Piemonte Orientale

13:30 - 14:20
Talk

Invited Talk: Resource-Aware Session Types

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 NeykovaBrunel University London

File Attached

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

File Attached

14:00 - 15:30: VMCAI 2019 - Program Synthesis at Sala III
Chair(s): Nuno P. LopesMicrosoft Research

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 Sala VI
Chair(s): Chung-Kil HurSeoul National University

14:00 - 14:30
Talk

Translation Validation for Security Properties

Matteo BusiUniversità di Pisa - Dipartimento di Informatica, Pierpaolo DeganoUniversità di Pisa - Dipartimento di Informatica, Letterio GallettaIMT School for Advanced Studies

Pre-print File Attached

14:30 - 15:00
Talk

Security Witnesses for Compiler Transformations

Kedar NamjoshiBell Labs, Nokia, Lucas M. TabajaraRice University

File Attached

15:00 - 15:30
Talk

A Data Layout Description Language for Cogent

Zilin ChenData61, CSIRO and UNSW, Matthew Di MeglioUNSW, Liam O'ConnorUNSW, Partha SusarlaData61, CSIRO, Christine RizkallahUNSW, Gabriele KellerUtrecht University

16:00 - 17:30: VMCAI 2019 - Abstract Interpretation (2) at Sala III
Chair(s): Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France

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

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

17:00 - 17:30
Talk

Relatively Complete Pushdown Analysis of Escape Continuations

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

16:00 - 18:00: PriSC 2019 - Session 4 at Sala VI
Chair(s): Aslan AskarovAarhus University, David NaumannStevens Institute of Technology

16:00 - 16:30
Other

Short Talks Session

16:30 - 17:00
Talk

Modular Security Guarantees for Low-Level Languages with Stack Traversal

Mathias Vorreiter PedersenAarhus University, Aslan AskarovAarhus University

File Attached

17:00 - 17:30
Talk

Confidentiality-Preserving Refinement

Roberto GuancialeKTH, Christoph BaumannKTH, Mads DamKTH, Hamed NematiCISPA

File Attached

17:30 - 18:00
Talk

(Un)Encrypted Computing and Indistinguishability Obfuscation

Peter BreuerHecusys LLC, Jonathan BowenLondon South Bank University

File Attached

16:00 - 18:25: BEAT 2019 - Session 4 at Sala VII
Chair(s): Adrian FrancalanzaUniversity of Malta, Jorge A. PérezUniversity of Groningen, The Netherlands

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. PérezUniversity 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

Media Attached

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

File Attached

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. PérezUniversity of Groningen, The Netherlands

Mon 14 Jan

09:00 - 10:30: VMCAI 2019 - Invited Talk 2 at Sala III
Chair(s): Lenore Zuck

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 Sala XII
Chair(s): Magnus O. MyreenChalmers University of Technology, Sweden

09:00 - 10:00
Talk

A Linear Logical Framework in Hybrid

Amy FeltyUniversity of Ottawa

DOI

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

DOI

09:00 - 10:30: OPCT 2019 - Session Types at Sala VII
Chair(s): Ilaria CastellaniINRIA Sophia Antipolis, France

09:00 - 09:15
Day opening

Opening

09:15 - 09:40
Talk

A Concurrent Functional Language with Session Types and Control Effects Based on Linear Logic

Luís CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa

09:40 - 10:05
Talk

A Foundation for Runtime Enforcement

Adrian FrancalanzaUniversity of Malta

10:05 - 10:30
Talk

Processes as Names?

Hans HüttelDepartment of Computer Science, Aalborg University

File Attached

09:00 - 10:30: TutorialFest - Tutorial 1A at Sala V

09:00 - 10:30
Talk

[T1] QuickChick: Property-Based Testing in Coq

Benjamin C. PierceUniversity of Pennsylvania, Leonidas LampropoulosUniversity of Pennsylvania

09:00 - 10:30: TutorialFest - Tutorial 2A at Sala VIII

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: TutorialFest - Tutorial 3A at Sala VI

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 - Tutorial 4A at Sala IX

09:00 - 10:30
Talk

[T4] Programming Cyber-Physical Systems with Logic

André PlatzerCarnegie Mellon University

11:00 - 12:30: VMCAI 2019 - Decision Procedures at Sala III
Chair(s): Kedar NamjoshiBell Labs, Nokia

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 WangPurdue University

File Attached

12:00 - 12:30
Talk

A Practical Algorithm for Structure Embedding

Charlie MurphyPrinceton University, Zachary KincaidPrinceton University

File Attached

11:00 - 12:30: CPP 2019 - Research Papers: Proof Theory, Theory of Programming Languages at Sala XII
Chair(s): Assia MahboubiINRIA

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

DOI

11:30 - 12:00
Research paper

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

Yannick ForsterSaarland University, Steven SchäferSaarland University, Simon SpiesSaarland University, Kathrin StarkSaarland University, Germany

DOI

12:00 - 12:30
Research paper

Eliminating Reflection from Type Theory

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

DOI

11:00 - 12:30: PEPM 2019 - Session 1 at Sala X
Chair(s): Manuel HermenegildoIMDEA Software Institute and T.U. of Madrid (UPM)

11:00 - 11:05
Day opening

Welcome to PEPM19

Atsushi IgarashiKyoto University, Japan, Manuel HermenegildoIMDEA Software Institute and T.U. of Madrid (UPM)

11:05 - 12:00
Talk

Applying Futamura Projections to Compose Languages and Tools in GraalVM (Invited Talk)

Christian HumerOracle Labs, Switzerland

File Attached

12:00 - 12:30
Talk

A Simpler Lambda Calculus

Barry JayUniversity of Technology Sydney

DOI

11:00 - 12:30: TutorialFest - Tutorial 1B at Sala V

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: TutorialFest - Tutorial 2B at Sala VIII

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 - Tutorial 3B at Sala VI

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 - Tutorial 4B at Sala IX

11:00 - 12:30
Talk

[T4] Programming Cyber-Physical Systems with Logic

André PlatzerCarnegie Mellon University

11:15 - 12:30: OPCT 2019 - Causality, Reversibility at Sala VII
Chair(s): Thomas H. Hildebrandt

11:15 - 11:40
Talk

Causal Reasoning for Safety

Georgiana CaltaisUniversity of Konstanz

File Attached

11:40 - 12:05
Talk

A Calculus of Branching Processes

Jean KrivineCNRS

12:05 - 12:30
Talk

An Axiomatic Approach to Reversible Computation

Irek UlidowskiUniversity of Leicester

12:30 - 14:00: Workshops - Monday Lunch at Lunch Room

12:30 - 14:00
Lunch

Lunch

13:50 - 15:30: OPCT 2019 - Session Types, Graph-Rewriting at Sala VII
Chair(s): Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS

13:50 - 14:15
Talk

Taming Concurrency for Verification using Multiparty Session Types

Kirstin PetersTU Berlin

14:15 - 14:40
Talk

From Testing Preorders to Flaky Tests

Giovanni BernardiUniversité Paris Diderot

File Attached

14:40 - 15:05
Talk

Multiparty Reactive Sessions

Cinzia Di GiustoLaboratoire I3S

File Attached

15:05 - 15:30
Talk

Independence, Concurrency and Abstraction in Graph-Rewriting Processes

Malte Lochau

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

13:50 - 14:00
Day opening

PADL Opening and Welcome

Moa JohanssonChalmers University of Technology, José Julio AlferesNOVA LINCS -- Universidade Nova de Lisboa

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 AriasUniversidad Politécnica de Madrid and IMDEA Software Institute, Manuel CarroIMDEA Software Institute and T.U. of Madrid (UPM)

File Attached

15:00 - 15:30
Talk

Improving Residuation in Declarative Programs

Michael HanusKiel University

File Attached

14:00 - 15:30: VMCAI 2019 - Probabilistic Systems at Sala III
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA

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 Sala XII
Chair(s): Chris HawblitzelMicrosoft Research

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

DOI

14:30 - 15:00
Research paper

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

Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes

DOI

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

DOI

14:00 - 15:30: PEPM 2019 - Session 2 at Sala X
Chair(s): Thomas P. JensenINRIA Rennes

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

DOI

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

DOI

15:00 - 15:30
Talk

Typed Parsing and Unparsing for Untyped Regular Expression Engines

Gabriel RadanneUniversity of Freiburg, Germany

DOI Pre-print File Attached

14:00 - 15:30: TutorialFest - Tutorial 5A at Sala V

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 - Tutorial 6A at Sala VIII

14:00 - 15:30
Talk

[T6] Session-Typed Concurrent Programming

Stephanie BalzerCarnegie Mellon University, USA

14:00 - 15:30: TutorialFest - Tutorial 7A at Sala IX

14:00 - 15:30
Talk

[T7] Higher-Order Probabilistic Programming

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France

Pre-print

14:00 - 15:30: TutorialFest - Tutorial 8A at Sala VI

14:00 - 15:30
Talk

[T8] Building Your Own Modular Static Analyser with Infer

Jules VillardFacebook London, Ezgi ÇiçekFacebook London, Mehdi BouazizFacebook London, Nikos Gorogiannis

16:00 - 17:15: OPCT 2019 - Concurrent Programming, Memory Models at Sala VII
Chair(s): Gustavo PetriIRIF, Université Paris Diderot

16:00 - 16:25
Talk

Linearizability in the Context of Weak Memory Models

Kirsten WinterThe University of Queensland

File Attached

16:25 - 16:50
Talk

IPA: Invariant-preserving Applications for Weakly Consistent Replicated Databases

Carla FerreiraUniversidade Nova Lisboa

16:50 - 17:15
Talk

Compositional Reasoning for Termination of Fine-grained Concurrent Programs

Emanuele D'OsualdoImperial College London, UK

Pre-print File Attached

16:00 - 17:30: VMCAI 2019 - Model Checking at Sala III
Chair(s): Xiaokang QiuPurdue University

16:00 - 16: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:30 - 17:00
Talk

A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization

Alfons LaarmanLeiden University, Richard Huybers

File Attached

17:00 - 17:30
Talk

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

Normann Decker, Anton Pirogov

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

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 and National University of Singapore

Pre-print

17:00 - 17:30
Talk

Classes of Arbitrary Kind

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

Link to publication DOI File Attached

16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at Sala XII
Chair(s): Georges GonthierInria

16:00 - 16:30
Research paper

A Formal Proof of Hensel's Lemma over the p-adic Integers

Robert Y. LewisVrije Universiteit Amsterdam

DOI

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

DOI

17:00 - 17:30
Research paper

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

Fabian Immler, Bohua Zhan

DOI

16:00 - 17:30: PEPM 2019 - Session 3 at Sala X
Chair(s): Atsushi IgarashiKyoto University, Japan

16:00 - 17:00
Talk

What Is the Type of a Partial Evaluator? (Invited Talk)

Jens PalsbergUniversity of California, Los Angeles (UCLA)

File Attached

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

DOI

16:00 - 17:30: TutorialFest - Tutorial 5B at Sala V

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 - Tutorial 6B at Sala VIII

16:00 - 17:30
Talk

[T6] Session-Typed Concurrent Programming

Stephanie BalzerCarnegie Mellon University, USA

16:00 - 17:30: TutorialFest - Tutorial 7B at Sala IX

16:00 - 17:30
Talk

[T7] Higher-Order Probabilistic Programming

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France

Pre-print

16:00 - 17:30: TutorialFest - Tutorial 8B at Sala VI

16:00 - 17:30
Talk

[T8] Building Your Own Modular Static Analyser with Infer

Jules VillardFacebook London, Ezgi ÇiçekFacebook London, Mehdi BouazizFacebook London, Nikos Gorogiannis

17:30 - 18:30: Workshops - Monday Social Hour at Galeria

17:30 - 18:30
Social Event

Social Hour

Tue 15 Jan

09:00 - 10:30: LAFI (né PPS) - A at Sala VI

09:00 - 09:30
Talk

Probabilistic Lambda Calculus: Beyond Deterministic Evaluation

Claudia FaggianIRIF, Simona Ronchi Della RoccaUniversity of Torino

File Attached

09:30 - 10:30
Talk

Invited talk: Connecting Probabilistic Programming Theory to Applications in Stan

Matthijs VákárUniversity of Oxford

File Attached

09:00 - 10:30: OPCT 2019 - Equational Characterisations, Transactions at Sala VII
Chair(s): Mohammad MousaviUniversity of Leicester, UK

09:15 - 09:40
Talk

Revised Semantics for Sequential Composition in the Presence of Successful Termination (Tentative)

Bas LuttikEindhoven University of Technology

File Attached

09:40 - 10:05
Talk

ULTraS at Work: Compositionality and Equational Characterization of Behavioral Metaequivalences

Marco BernardoUniversity of Urbino

10:05 - 10:30
Talk

A Uniform Framework of Transactional Consistency Models for Protocol Verification and Program Analysis

Andrea CeroneImperial College London

09:00 - 10:30: VMCAI 2019 - Invited Talk 3 at Sala III
Chair(s): Ruzica PiskacYale University, USA

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 Sala XII
Chair(s): Assia MahboubiINRIA

09:00 - 10:00
Talk

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

Jasmin Christian BlanchetteVrije Universiteit Amsterdam

DOI

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

DOI

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

09:30 - 10:00
Talk

Personalized Course Schedule Planning using Answer Set Programming

Esra ErdemSabanci University, Turkey, Muhammed Kerem Kahraman

File Attached

10:00 - 10:30
Talk

Static Partitioning of Spreadsheets for Parallel Execution

Alexander Asp Bock

File Attached

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

09:00 - 09:15
Day opening

PLMW Welcome

Pre-print

09:15 - 10:00
Talk

Technical Talk: Verification of Distributed Protocols Using Decidable Logic

Sharon ShohamTel Aviv university

Pre-print File Attached

10:00 - 10:30
Talk

Research Skills: How to Give a Talk

Chung-chieh ShanIndiana University, USA

Pre-print File Attached

11:00 - 12:30: LAFI (né PPS) - B at Sala VI
Chair(s): Steven HoltzenUniversity of California, Los Angeles

11:00 - 11:30
Talk

The Geometry of Bayesian Programming

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

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

File Attached

12:00 - 12:30
Talk

Server-side Probabilistic Programming

David TolpinPUB+

Media Attached

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

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 Sala II

11:00 - 11:30
Talk

Research Skills: How to Choose Research Areas

Catuscia PalamidessiINRIA and LIX

Pre-print File Attached

11:30 - 12:30
Talk

Panel: Grad School and Beyond

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

Pre-print

11:00 - 12:30: CPP 2019 - Research Papers: Rewriting, Automated Reasoning at Sala XII
Chair(s): Andrei PopescuMiddlesex University, London

11:00 - 11:30
Research paper

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

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

DOI

11:30 - 12:00
Research paper

Certified ACKBO

Alexander Lochmann, Christian SternagelUniversity of Innsbruck, Austria

DOI

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

DOI

11:00 - 12:30: PEPM 2019 - Session 4 at Sala X
Chair(s): Roberto GiacobazziUniversity of Verona and IMDEA Software Institute

11:00 - 12:00
Talk

Making Proofs Easy: Horn Clause Transformations to the Aid of Program Verification (Invited Talk)

Maurizio Proietti

File Attached

12:00 - 12:30
Talk

Control Flow Obfuscation via CPS Transformation

Kenny Zhuo Ming LuNanyang Polytechnic, Singapore

DOI

11:00 - 12:30: VMCAI 2019 - Software Verification and Synthesis at Sala III
Chair(s): Ori LahavTel Aviv University

11:00 - 11:30
Talk

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

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

Link to publication DOI Pre-print File Attached

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

11:15 - 12:30: OPCT 2019 - Cyberphysical Systems, Hybrid Systems at Sala VII
Chair(s): Philippa GardnerImperial College London

11:15 - 11:40
Talk

Hybrid Systems Reachability Analysis

Erika AbrahamRWTH Aachen University

11:40 - 12:05
Talk

Attribute Based Communication for Collective Adaptive Systems

Rocco De Nicola

12:05 - 12:30
Talk

Designing Resilient Large Scaled CPS: Models, Languages and Tools

Michele LoretiUniversity of Camerino

12:30 - 14:00: Workshops - Tuesday Lunch at Lunch Room

12:30 - 14:00
Lunch

Lunch

13:50 - 15:30: OPCT 2019 - Algebra, Coalgebra, Model Checking at Sala VII
Chair(s): Barbara KönigUniversity of Duisburg-Essen

13:50 - 14:15
Talk

Bayes meets Dijkstra: Verifying Bayes Networks by Program Verification

Joost-Pieter KatoenRWTH Aachen University

File Attached

14:15 - 14:40
Talk

Model Checking True Concurrency Properties

Paolo BaldanUniversity of Padova

File Attached

14:40 - 15:05
Talk

A (Co)algebraic Approach to Hennessy-Milner Theorems for Weakly Expressive Logics

Helle Hvid HansenDelft University of Technology

File Attached

15:05 - 15:30
Talk

Weak Bisimulation Metrics in Models with Nondeterminism and Continuous States Space: A Logical Characterization

Simone TiniUniversity of Insubria

14:00 - 15:30: LAFI (né PPS) - C at Sala VI
Chair(s): Sophia GoldTezos

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

File Attached

15:00 - 15:30
Talk

Probabilistic Programming with CuPPL

Alexander CollinsNVIDIA, Vinod GroverNVIDIA

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

14:00 - 14:30
Talk

Composing Syntactical Constructs to Create Domain-Specific Languages

David BromanKTH Royal Institute of Technology, Viktor PalmkvistKTH Royal Institute of Technology

DOI Media Attached

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 Sala II

14:00 - 14:45
Talk

Technical Talk: How to Think about Types

Frank PfenningCarnegie Mellon University, USA

Pre-print File Attached

14:45 - 15:30
Talk

Technical Talk: What Is Programming Languages Research?

Michael HicksUniversity of Maryland, College Park

Pre-print File Attached

14:00 - 15:30: CPP 2019 - Research Papers: Program Verification at Sala XII
Chair(s): Nicolas TabareauInria

14:00 - 14:30
Research paper

A Verified Protocol Buffer Compiler

Qianchuan YePurdue University, Benjamin DelawarePurdue University

DOI

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

DOI

15:00 - 15:30
Research paper

Dynamic Class Initialization Semantics: a Jinja Extension

Susannah Mansky, Elsa GunterUniversity of Illinois

DOI

14:00 - 15:30: PEPM 2019 - Session 5 at Sala X
Chair(s): Alberto PettorossiUniversity of Rome Tor Vergata, Italy

14:00 - 14:30
Talk

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

Kenichi AsaiOchanomizu University

DOI File Attached

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

DOI File Attached

15:00 - 15:28
Talk

Generating Mutually Recursive Definitions

Jeremy YallopUniversity of Cambridge, UK, Oleg Kiselyov

DOI Pre-print

15:28 - 15:30
Poster

Advanced Futures and Promises in C++ (poster)

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

14:00 - 15:30: VMCAI 2019 - Software Verification at Sala III
Chair(s): Grigory FedyukovichPrinceton University

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

File Attached

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:20: OPCT 2019 - Algebra, Coalgebra at Sala VII
Chair(s): Alexandra SilvaUniversity College London

16:00 - 16:25
Talk

Coalgebra Learning via Duality

Jurriaan RotRadboud University Nijmegen

16:25 - 16:50
Talk

A Metric Semantics for Coordination Languages

Valentina CastiglioniInria Saclay - Ile de France

File Attached

16:50 - 17:15
Talk

Hybrid System Iteration

Renato NevesUniversity of Minho & INESC TEC

File Attached

17:15 - 17:20
Day closing

Closing

16:00 - 17:30: LAFI (né PPS) - D at Sala VI

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 Sala III
Chair(s): Cezara DrăgoiINRIA, ENS, CNRS

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

Parametric Timed Broadcast Protocols

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

File Attached

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

16:00 - 16:30
Talk

Research Skills: How to Bootstrap a Research Project

Ilya SergeyYale-NUS College and National University of Singapore

Pre-print File Attached

16:30 - 17:30
Talk

Panel: How to Do Good 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

Pre-print

16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at Sala XII
Chair(s): Zhong ShaoYale University

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

DOI

16:30 - 17:00
Research paper

Verified Solving and Asymptotics of Linear Recurrences

Manuel EberlTechnische Universität München

DOI

17:00 - 17:30
Meeting

Business Meeting

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

17:30 - 18:30: Workshops - Tuesday Social Hour at Galeria

17:30 - 18:30
Social Event

Social Hour

Wed 16 Jan

09:00 - 10:05: Research Papers - Welcome & Keynote I at Sala I + II
Chair(s): Peter O'HearnFacebook

09:00 - 09:05
Day opening

Welcome

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

Media Attached

09:05 - 10:05
Talk

Automated Fault-Finding and Fixing at Facebook

Mark HarmanFacebook and University College London

Media Attached

10:35 - 12:03: Research Papers - Concurrency at Sala II
Chair(s): Ori LahavTel Aviv University

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 and National University of Singapore

Link to publication DOI Pre-print Media Attached File Attached

10:57 - 11:19
Talk

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

Roland Meyer, Sebastian WolffTU Braunschweig

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Media Attached

11:41 - 12:03
Talk

Weak-Consistency Specification via Visibility Relaxation

Michael EmmiSRI International, Constantin EneaUniversité Paris Diderot

Link to publication DOI Media Attached File Attached

10:35 - 12:03: Research Papers - Reasoning about Probabilistic Programs at Sala I
Chair(s): Jan HoffmannCarnegie Mellon University

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

Link to publication DOI Media Attached File Attached

10:57 - 11:19
Talk

A Separation Logic for Concurrent Randomized Programs

Joseph TassarottiCarnegie Mellon University, Robert Harper

Link to publication DOI Media Attached File Attached

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 MathejaRWTH Aachen University, Thomas NollRWTH Aachen University

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached

12:03 - 13:45: Research Papers - Wednesday Lunch at Lunch Room

12:03 - 13:45
Lunch

Lunch

13:45 - 14:51: Research Papers - Categories at Sala II
Chair(s): Nicolas TabareauInria

13:45 - 14:07
Talk

Familial Monads and Structural Operational Semantics

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

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

14:29 - 14:51
Talk

Categorical Combinatorics of Scheduling and Synchronization in Game Semantics

Paul-André MelliesCNRS and University Paris Diderot

Link to publication DOI Media Attached File Attached

13:45 - 14:51: Research Papers - Probabilistic Programming and Semantics at Sala I
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA

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

Link to publication DOI Pre-print Media Attached File Attached

14:07 - 14:29
Talk

A Domain Theory for Statistical Probabilistic ProgrammingDistinguished Paper

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

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

15:21 - 16:27: Research Papers - Capabilities and Session Types I at Sala II
Chair(s): Dominic OrchardUniversity of Kent, UK

15:21 - 15:43
Talk

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

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

Link to publication DOI Media Attached File Attached

15:43 - 16:05
Talk

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

Simon CastellanImperial College London, UK, Nobuko YoshidaImperial College London

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Pre-print Media Attached File Attached

15:21 - 16:27: Research Papers - Machine Learning and Linear Algebra at Sala I
Chair(s): Aws AlbarghouthiUniversity of Wisconsin-Madison

15:21 - 15:43
Talk

code2vec: Learning Distributed Representations of Code

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

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Media Attached

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.

Link to publication DOI Media Attached File Attached

16:37 - 17:43: Research Papers - Quantum Programming at Sala I
Chair(s): Jens PalsbergUniversity of California, Los Angeles (UCLA)

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

Link to publication DOI Media Attached

16:59 - 17:21
Talk

Game Semantics for Quantum Programming

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

Link to publication DOI Media Attached

17:21 - 17:43
Talk

Quantum Relational Hoare Logic

Dominique UnruhUniversity of Tartu

Link to publication DOI Pre-print Media Attached File Attached

16:37 - 17:43: Research Papers - Session Types II at Sala II
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh

16:37 - 16:59
Talk

Interconnectability of Session-Based Logical ProcessesTOPLAS

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

Link to publication DOI Pre-print Media Attached

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

Link to publication DOI Pre-print Media Attached File Attached

17:21 - 17:43
Talk

Less is More: Multiparty Session Types Revisited

Alceste ScalasImperial College London, Nobuko YoshidaImperial College London

Link to publication DOI Pre-print Media Attached File Attached

18:00 - 18:30: Research Papers - Wednesday Evening Program I at Sala I

18:00 - 18:30
Talk

Microsoft Research: Engage, Verify, Open

Thomas BallMicrosoft Research

Media Attached

18:30 - 19:30: Research Papers - Wednesday Evening Program II at Galeria

18:30 - 19:30
Social Event

Student Research Competition and Reception supported by Microsoft Research

Thu 17 Jan

09:00 - 10:06: Research Papers - Synthesis at Sala II
Chair(s): Robbert KrebbersDelft University of Technology

09:00 - 09:22
Talk

Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper

Nadia PolikarpovaUniversity of California, San Diego, Ilya SergeyYale-NUS College and National University of Singapore

Link to publication DOI Pre-print Media Attached File Attached

09:22 - 09:44
Talk

FrAngel: Component-Based Synthesis with Control Structures

Kensen ShiStanford University, Jacob SteinhardtStanford University, Percy LiangStanford University

Link to publication DOI Pre-print Media Attached File Attached

09:44 - 10:06
Talk

Hamsaz: Replication Coordination Analysis and Synthesis

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

Link to publication DOI Media Attached

09:00 - 10:06: Research Papers - Type Abstraction and Effects at Sala I
Chair(s): Benjamin DelawarePurdue University

09:00 - 09:22
Talk

Abstraction-Safe Effect Handlers via Tunneling

Yizhou ZhangCornell University, Andrew MyersCornell University

Link to publication DOI Media Attached

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

Link to publication DOI Media Attached

09:44 - 10:06
Talk

Fully Abstract Module Compilation

Karl CraryCarnegie Mellon University

Link to publication DOI Media Attached File Attached

10:30 - 12:30: Student Research Competition - Finalist Poster Presentations at Sala III

10:36 - 12:04: Research Papers - Gradual Types at Sala I
Chair(s): Nikhil SwamyMicrosoft Research

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

DOI Media Attached File Attached

10:58 - 11:20
Talk

Gradual Type Theory

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

Link to publication DOI Media Attached File Attached

11:20 - 11:42
Talk

Gradual Parametricity, RevisitedDistinguished Paper

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

Link to publication DOI Pre-print Media Attached File Attached

11:42 - 12:04
Talk

Live Functional Programming with Typed Holes

Cyrus OmarUniversity of Chicago, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago, Matthew HammerNone

Link to publication DOI Pre-print Media Attached File Attached

10:36 - 12:04: Research Papers - Separation Logic and Memory Semantics at Sala II
Chair(s): Ilya SergeyYale-NUS College and National University of Singapore

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

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

11:20 - 11:42
Talk

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

Alasdair ArmstrongUniversity of Cambridge, 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

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

12:04 - 13:45: Research Papers - Thursday Lunch at Lunch Room

12:04 - 13:45
Lunch

Lunch

13:45 - 14:51: Research Papers - Type Inference I at Sala I
Chair(s): Michael HicksUniversity of Maryland, College Park

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

Link to publication DOI Media Attached

14:07 - 14:29
Talk

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

J. Garrett MorrisUniversity of Kansas, USA, James McKinna

Link to publication DOI Media Attached

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

Link to publication DOI Media Attached File Attached

13:45 - 14:51: Research Papers - Weak Memory at Sala II
Chair(s): Scott OwensUniversity of Kent, UK

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

Link to publication DOI Pre-print Media Attached File Attached

14:07 - 14:29
Talk

Bridging the Gap Between Programming Languages and Hardware Weak Memory Models

Anton PodkopaevHigher School of Economics, JetBrains Research, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, Germany

Link to publication DOI Pre-print Media Attached File Attached

14:29 - 14:51
Talk

Grounding Thin-Air Reads with Event Structures

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

Link to publication DOI Media Attached File Attached

15:21 - 16:49: Research Papers - Time at Sala II
Chair(s): Andrew MyersCornell University

15:21 - 15:43
Talk

Type-Guided Worst-Case Input Generation

Di WangCarnegie Mellon University, Jan HoffmannCarnegie Mellon University

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

16:05 - 16:27
Talk

Modular Quantitative Monitoring

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

Link to publication DOI Media Attached File Attached

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

Media Attached File Attached

15:21 - 16:49: Research Papers - Type Inference II at Sala I
Chair(s): Niki VazouIMDEA Software Institute

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

Link to publication DOI Pre-print Media Attached File Attached

15:43 - 16:05
Talk

Gradual Typing: A New Perspective

Giuseppe CastagnaCNRS - Université Paris Diderot, France, Victor LanvinIRIF, Université Paris Diderot, France, Tommaso PetruccianiDIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. SiekIndiana University, USA

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

16:27 - 16:49
Talk

Principality and Approximation under Dimensional Bound

Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund

Link to publication DOI Media Attached File Attached

17:00 - 18:00: Research Papers - Business Meeting at Sala I + II

17:00 - 17:15
Other

PC Chair Report

Stephanie WeirichUniversity of Pennsylvania, USA

Media Attached

17:15 - 17:25
Awards

SIGPLAN Awards

Benjamin C. PierceUniversity of Pennsylvania

Media Attached

17:25 - 17:30
Other

POPL 2020 Announcement

Brigitte PientkaMcGill University, Lars BirkedalAarhus University

Media Attached

17:30 - 17:40
Other

NSF funding for PL

Rance CleavelandUniversity of Maryland

Media Attached

17:40 - 17:50
Other

SIGPLAN Climate Committee Report

Benjamin C. PierceUniversity of Pennsylvania

Media Attached

17:50 - 18:00
Other

State of SIGPLAN

Jens PalsbergUniversity of California, Los Angeles (UCLA)

Media Attached

18:15 - 19:15: Research Papers - Reception supported by Facebook at Galeria

18:15 - 19:15
Social Event

Reception supported by Facebook

Fri 18 Jan

09:00 - 10:05: Research Papers - SRC Announcement & Keynote II at Sala I + II
Chair(s): Stephanie WeirichUniversity of Pennsylvania, USA

09:00 - 09:05
Awards

SRC Announcement

Niki VazouIMDEA Software Institute

Media Attached

09:05 - 10:05
Talk

Mechanized Metatheory - The Next Chapter

Brigitte PientkaMcGill University

Media Attached File Attached

10:35 - 12:03: Research Papers - Abstract Interpretation at Sala II
Chair(s): David NaumannStevens Institute of Technology

10:35 - 10:57
Talk

A^2 I: Abstract^2 InterpretationDistinguished Paper

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

Link to publication DOI Media Attached File Attached

10:57 - 11:19
Talk

Concerto: A Framework for Combined Concrete and Abstract Interpretation

John TomanUniversity of Washington, Seattle, Dan GrossmanUniversity of Washington

Link to publication DOI Media Attached

11:19 - 11:41
Talk

Skeletal Semantics and their Interpretations

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

Link to publication DOI Pre-print Media Attached File Attached

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.

Link to publication DOI Media Attached File Attached

10:35 - 12:03: Research Papers - Dependent Types at Sala I
Chair(s): Andreas AbelGothenburg University

10:35 - 10:57
Talk

Higher Inductive Types in Cubical Computational Type Theory

Evan CavalloCarnegie Mellon University, Robert Harper

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

11:19 - 11:41
Talk

Definitional Proof-Irrelevance without K

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

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

12:03 - 13:45: Research Papers - Friday Lunch at Lunch Room

12:03 - 13:45
Lunch

Lunch

13:45 - 14:51: Research Papers - Model Checking at Sala II
Chair(s): P. MadhusudanUniversity of Illinois at Urbana-Champaign

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

Link to publication DOI Media Attached File Attached

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)

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached

13:45 - 14:51: Research Papers - Semantics at Sala I
Chair(s): Noam ZeilbergerUniversity of Birmingham, UK

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

Link to publication DOI Media Attached

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

Link to publication DOI Media Attached

14:29 - 14:51
Talk

Fixpoint Games on Continuous Lattices

Paolo BaldanUniversity of Padova, Barbara KönigUniversity of Duisburg-Essen, Christina Mika-MichalskiUniversity of Duisburg-Essen, Tommaso PadoanUniversity of Padova

Link to publication DOI Media Attached File Attached

15:21 - 16:27: Research Papers - Program Analysis I at Sala II
Chair(s): Michael D. AdamsUniversity of Utah

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

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Pre-print Media Attached File Attached

16:05 - 16:27
Talk

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

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

Link to publication DOI Pre-print Media Attached File Attached

15:21 - 16:27: Research Papers - Security and Information Flow at Sala I
Chair(s): David WalkerPrinceton University

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

Link to publication DOI Media Attached File Attached

15:43 - 16:05
Talk

From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper

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

Link to publication DOI Media Attached File Attached

16:05 - 16:27
Talk

Modalities, Cohesion, and Information Flow

G. A. KavvosWesleyan University

Link to publication DOI Pre-print File Attached

16:37 - 17:43: Research Papers - Program Analysis II at Sala II
Chair(s): Michael EmmiSRI International

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

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Pre-print Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

16:37 - 17:43: Research Papers - Verified Compilation and Concurrency at Sala I
Chair(s): Michael GreenbergPomona College

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

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

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

Link to publication DOI Media Attached File Attached

17:45 - 18:45: Research Papers - Friday Social Hour at Galeria

17:45 - 18:45
Social Event

Social Hour

Sat 19 Jan

09:00 - 10:30: Off the Beaten Track 2019 - Keynote at Sala VII
Chair(s): Luke Church

09:30 - 10:30
Talk

De-escalating Software (Keynote)

Stephen KellUniversity of Kent

09:00 - 10:30: CoqPL - Keynote & Contributed Talks 1 at Sala VI
Chair(s): Ilya SergeyYale-NUS College and National University of Singapore

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:00 - 12:30: Off the Beaten Track 2019 - Morning Papers at Sala VII
Chair(s): Michael GreenbergPomona College

11:00 - 11:45
Talk

Facile : A Domain Specific Language and Compiler for Program Analysis and Optimization

Madhur Amilkanthwar

File Attached

11:45 - 12:30
Talk

From Tactics to Structure Editors for Proofs

Xuanrui (Ray) QiTufts University

Pre-print

11:15 - 12:30: CoqPL - Contributed Talks 2 at Sala VI
Chair(s): Enrico TassiINRIA

11:15 - 11:40
Talk

Towards Mechanising Probabilistic Properties of a Blockchain

Kiran GopinathanUniversity College London, Ilya SergeyYale-NUS College and National University of Singapore

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

12:30 - 14:00: Workshops - Saturday Lunch at Lunch Room

12:30 - 14:00
Lunch

Lunch

14:00 - 15:30: Off the Beaten Track 2019 - Afternoon Talks at Sala VII
Chair(s): Luke Church

14:00 - 14:45
Other

Design Critique and Discussion

Luke Church

14:45 - 15:30
Talk

F a Language for Music Composition

Joachim KristensenDIKU, University of Copenhagen, Ken Friis LarsenDIKU, University of Copenhagen

14:00 - 15:30: CoqPL - Contributed Talks 3 & Coq Developers at Sala VI
Chair(s): Qinxiang CaoShanghai Jiao Tong University

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 Torrini

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 Sala VI
Chair(s): Robbert KrebbersDelft University of Technology

16:00 - 16:25
Talk

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

Qinxiang CaoShanghai Jiao Tong University

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

16:00 - 17:30: Off the Beaten Track 2019 - Informal + Business Meeting at Sala VII

16:00 - 17:30
Meeting

Informal + Business Meeting

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
Lunch Room										POPL Workshops Sunday Lunch 12:30 - 14:00
Sala III			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
Sala VI			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 - 18:00
Sala VII		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

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	18:00	30
Galeria														POPL Workshops Monday Social Hour 17:30 - 18:30
Lunch Room									POPL Workshops Monday Lunch 12:30 - 14:00
Sala III	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
Sala IV	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
Sala IX	POPL TutorialFest Tutorial 4A 09:00 - 10:30				POPL TutorialFest Tutorial 4B 11:00 - 12:30								POPL TutorialFest Tutorial 7A 14:00 - 15:30					POPL TutorialFest Tutorial 7B 16:00 - 17:30
Sala V	POPL TutorialFest Tutorial 1A 09:00 - 10:30				POPL TutorialFest Tutorial 1B 11:00 - 12:30								POPL TutorialFest Tutorial 5A 14:00 - 15:30					POPL TutorialFest Tutorial 5B 16:00 - 17:30
Sala VI	POPL TutorialFest Tutorial 3A 09:00 - 10:30				POPL TutorialFest Tutorial 3B 11:00 - 12:30								POPL TutorialFest Tutorial 8A 14:00 - 15:30					POPL TutorialFest Tutorial 8B 16:00 - 17:30
Sala VII	OPCT Session Types 09:00 - 10:30					OPCT Causality, Reversibility 11:15 - 12:30						OPCT Session Types, Graph-Rewriting 13:50 - 15:30						OPCT Concurrent Programming, Memory Models 16:00 - 17:15
Sala VIII	POPL TutorialFest Tutorial 2A 09:00 - 10:30				POPL TutorialFest Tutorial 2B 11:00 - 12:30								POPL TutorialFest Tutorial 6A 14:00 - 15:30					POPL TutorialFest Tutorial 6B 16:00 - 17:30
Sala X	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
Sala XII	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

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	18:00	30
Galeria														POPL Workshops Tuesday Social Hour 17:30 - 18:30
Lunch Room									POPL Workshops Tuesday Lunch 12:30 - 14:00
Sala II	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
Sala III	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
Sala IV	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
Sala VI	LAFI A 09:00 - 10:30				LAFI B 11:00 - 12:30								LAFI C 14:00 - 15:30					LAFI D 16:00 - 17:30
Sala VII	OPCT Equational Characterisations, Transactions 09:00 - 10:30					OPCT Cyberphysical Systems, Hybrid Systems 11:15 - 12:30						OPCT Algebra, Coalgebra, Model Checking 13:50 - 15:30						OPCT Algebra, Coalgebra 16:00 - 17:20
Sala X	PEPM 09:00 - 10:30				PEPM Session 4 11:00 - 12:30								PEPM Session 5 14:00 - 15:30					PEPM 16:00 - 17:30
Sala XII	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

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	18:00	30	19:00	30
Galeria															POPL Research Papers Wednesday Evening Program II 18:30 - 19:30
Lunch Room									POPL Research Papers Wednesday Lunch 12:03 - 13:45
Sala I					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 Research Papers Wednesday Evening Program I 18:00 - 18:30
Sala I + II	POPL Research Papers Welcome & Keynote I 09:00 - 10:05
Sala II					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	19:00	30
Galeria															POPL Research Papers Reception supported by Facebook 18:15 - 19:15
Lunch Room									POPL Research Papers Thursday Lunch 12:04 - 13:45
Sala I	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
Sala I + II															POPL Research Papers Business Meeting 17:00 - 18:00
Sala II	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
Sala III

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

POPL Workshops

VMCAI

VMCAI

VMCAI

VMCAI

PriSC

PriSC

PriSC

PriSC

BEAT

BEAT

BEAT

BEAT

Mon 14 Jan 2019

POPL Workshops

POPL Workshops

VMCAI

VMCAI

VMCAI

VMCAI

PADL

PADL

PADL

PADL

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

OPCT

OPCT

OPCT

OPCT

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

POPL TutorialFest

PEPM

PEPM

PEPM

PEPM

CPP

CPP

CPP

CPP

Tue 15 Jan 2019

POPL Workshops

POPL Workshops

PLMW

PLMW

PLMW

PLMW

VMCAI

VMCAI

VMCAI

VMCAI

PADL

PADL

PADL

PADL

LAFI

LAFI

LAFI

LAFI