Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sun 13 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

08:30 - 10:30: Session 1BEAT at Sala VII
Chair(s): Philip WadlerUniversity of Edinburgh, UK
08:30 - 08:40
Day opening
Opening
BEAT
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
BEAT
Peter ThiemannUniversity of Freiburg, Germany
09:30 - 09:50
Talk
Gradual Session Types in Imperative Style
BEAT
Kaede KobayashiKyoto University, Atsushi IgarashiKyoto University, Japan
09:50 - 10:10
Talk
Checking the Equivalence of Context-Free Session Types
BEAT
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
BEAT
Alceste ScalasImperial College London, Elias BenussiImperial College London, Nobuko YoshidaImperial College London
File Attached
09:00 - 10:30: Invited Talk 1VMCAI 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
VMCAI
Sylvie PutotÉcole Polytechnique
09:00 - 10:30: Session 1PriSC 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
PriSC
File Attached
10:00 - 10:30
Talk
Towards Secure Compilation of Power Side-Channel Countermeasures
PriSC
Marc GourjonHamburg University of Technology and NXP Semiconductors Germany GmbH
File Attached
11:00 - 12:30: Session 2PriSC at Sala VI
Chair(s): Dominique DevrieseVrije Universiteit Brussel, Belgium
11:00 - 11:30
Talk
Trestle: Bridging the Performance and Safety Divide in WebAssembly
PriSC
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
PriSC
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
PriSC
Alexander RichardsonUniversity of Cambridge, Robert N. M. WatsonUniversity of Cambridge
File Attached
11:00 - 12:30: Session 2BEAT 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
BEAT
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France
11:50 - 12:10
Talk
Global Types with Internal Delegation
BEAT
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
BEAT
12:30 - 14:00: Sunday LunchWorkshops at Lunch Room
12:30 - 14:00
Lunch
Lunch
Workshops
13:30 - 15:30: Session 3BEAT at Sala VII
Chair(s): Paola GianniniUniversita' del Piemonte Orientale
13:30 - 14:20
Talk
Invited Talk: Resource-Aware Session Types
BEAT
Jan HoffmannCarnegie Mellon University
14:20 - 15:10
Talk
Invited Talk: A Session Type Provider: Compile-time Generation of Session Types with Interaction Refinements
BEAT
Rumyana NeykovaBrunel University London
File Attached
15:10 - 15:30
Talk
Getting Rid of Null-Dereferences – Behavioural Types to the Rescue
BEAT
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: Program SynthesisVMCAI at Sala III
Chair(s): Nuno P. LopesMicrosoft Research
14:00 - 14:30
Talk
Minimal Synthesis of String To String Functions From Examples
VMCAI
Jad HamzaLIAFA, Université Paris Diderot, Viktor KunčakEPFL, Switzerland
14:30 - 15:00
Talk
Lazy but Effective Functional Synthesis
VMCAI
Grigory FedyukovichPrinceton University, Arie GurfinkelUniversity of Waterloo, Aarti GuptaPrinceton University
15:00 - 15:30
Talk
Automatic Program Repair using Formal Verification and Expression Templates
VMCAI
Thanh-Toan Nguyen, Quang-Trung TaNational University of Singapore, Wei-Ngan ChinNational University of Singapore
14:00 - 15:30: Session 3PriSC at Sala VI
Chair(s): Chung-Kil HurSeoul National University
14:00 - 14:30
Talk
Translation Validation for Security Properties
PriSC
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
PriSC
Kedar NamjoshiBell Labs, Nokia, Lucas M. TabajaraRice University
File Attached
15:00 - 15:30
Talk
A Data Layout Description Language for Cogent
PriSC
Zilin ChenData61, CSIRO and UNSW, Matthew Di MeglioUNSW, Liam O'ConnorUNSW, Partha SusarlaData61, CSIRO, Christine RizkallahUNSW, Gabriele KellerUtrecht University
16:00 - 17:30: Abstract Interpretation (2)VMCAI at Sala III
Chair(s): Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France
16:00 - 16:30
Talk
Demand Control-Flow Analysis
VMCAI
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
VMCAI
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
VMCAI
Kimball GermaneUniversity of Utah, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School
16:00 - 18:00: Session 4PriSC at Sala VI
Chair(s): Aslan AskarovAarhus University, David NaumannStevens Institute of Technology
16:00 - 16:30
Other
Short Talks Session
PriSC
16:30 - 17:00
Talk
Modular Security Guarantees for Low-Level Languages with Stack Traversal
PriSC
Mathias Vorreiter PedersenAarhus University, Aslan AskarovAarhus University
File Attached
17:00 - 17:30
Talk
Confidentiality-Preserving Refinement
PriSC
File Attached
17:30 - 18:00
Talk
(Un)Encrypted Computing and Indistinguishability Obfuscation
PriSC
Peter BreuerHecusys LLC, Jonathan BowenLondon South Bank University
File Attached
16:00 - 18:25: Session 4BEAT 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
BEAT
16:50 - 17:10
Talk
Behavioral Types as a Semantic Foundation for the GDPR Notion of Purpose
BEAT
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
BEAT
Daniele Nantes-SobrinhoUniversity of Brasília, Brazil, Jorge A. PérezUniversity of Groningen, The Netherlands
17:30 - 17:40
Break
Short break
BEAT
17:40 - 18:00
Talk
Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs
BEAT
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
BEAT
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
BEAT
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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:30: Invited Talk 2VMCAI at Sala III
Chair(s): Lenore Zuck
09:00 - 10:30
Talk
Designing Self-Certifying Software Systems
VMCAI
Kedar NamjoshiBell Labs, Nokia
09:00 - 10:30: Tutorial 4ATutorialFest at Sala IX
09:00 - 10:30
Talk
[T4] Programming Cyber-Physical Systems with Logic
TutorialFest
André PlatzerCarnegie Mellon University
09:00 - 10:30: Tutorial 1ATutorialFest at Sala V
09:00 - 10:30
Talk
[T1] QuickChick: Property-Based Testing in Coq
TutorialFest
Benjamin C. PierceUniversity of Pennsylvania, Leonidas LampropoulosUniversity of Pennsylvania
09:00 - 10:30: Tutorial 3ATutorialFest at Sala VI
09:00 - 10:30
Talk
[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
TutorialFest
Dominic OrchardUniversity of Kent, UK, Harley D. Eades IIIAugusta University, Vilem-Benjamin LiepeltUniversity of Kent, UK
09:00 - 10:30: Session TypesOPCT at Sala VII
Chair(s): Ilaria CastellaniINRIA Sophia Antipolis, France
09:00 - 09:15
Day opening
Opening
OPCT
09:15 - 09:40
Talk
A Concurrent Functional Language with Session Types and Control Effects Based on Linear Logic
OPCT
Luís CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
09:40 - 10:05
Talk
A Foundation for Runtime Enforcement
OPCT
Adrian FrancalanzaUniversity of Malta
10:05 - 10:30
Talk
Processes as Names?
OPCT
Hans HüttelDepartment of Computer Science, Aalborg University
File Attached
09:00 - 10:30: Tutorial 2ATutorialFest at Sala VIII
09:00 - 10:30
Talk
[T2] Engineering Distributed Systems via Protocols and Commitments
TutorialFest
Amit ChopraLancaster University, UK, Munindar P. SinghNorth Carolina State University
09:00 - 10:30: Keynote 1 and Research PaperCPP at Sala XII
Chair(s): Magnus O. MyreenChalmers University of Technology, Sweden
09:00 - 10:00
Talk
A Linear Logical Framework in Hybrid
CPP
Amy FeltyUniversity of Ottawa
DOI
10:00 - 10:30
Research paper
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
CPP
Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA
DOI
11:00 - 12:30: Decision ProceduresVMCAI at Sala III
Chair(s): Kedar NamjoshiBell Labs, Nokia
11:00 - 11:30
Talk
Solving and Interpolating Constant Arrays Based on Weak Equivalences
VMCAI
Jochen HoenickeUniversität Freiburg, Tanja SchindlerUniversity of Freiburg
11:30 - 12:00
Talk
A Decidable Logic for Tree Data-Structures with Measurements
VMCAI
Xiaokang QiuPurdue University, Yanjun WangPurdue University
File Attached
12:00 - 12:30
Talk
A Practical Algorithm for Structure Embedding
VMCAI
Charlie MurphyPrinceton University, Zachary KincaidPrinceton University
File Attached
11:00 - 12:30: Tutorial 4BTutorialFest at Sala IX
11:00 - 12:30
Talk
[T4] Programming Cyber-Physical Systems with Logic
TutorialFest
André PlatzerCarnegie Mellon University
11:00 - 12:30: Tutorial 1BTutorialFest at Sala V
11:00 - 12:30
Talk
[T1] QuickChick: Property-Based Testing in Coq
TutorialFest
Benjamin C. PierceUniversity of Pennsylvania, Leonidas LampropoulosUniversity of Pennsylvania
11:00 - 12:30: Tutorial 3BTutorialFest at Sala VI
11:00 - 12:30
Talk
[T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning
TutorialFest
Dominic OrchardUniversity of Kent, UK, Harley D. Eades IIIAugusta University, Vilem-Benjamin LiepeltUniversity of Kent, UK
11:00 - 12:30: Tutorial 2BTutorialFest at Sala VIII
11:00 - 12:30
Talk
[T2] Engineering Distributed Systems via Protocols and Commitments
TutorialFest
Amit ChopraLancaster University, UK, Munindar P. SinghNorth Carolina State University
11:00 - 12:30: Session 1PEPM at Sala X
Chair(s): Manuel HermenegildoIMDEA Software Institute and T.U. of Madrid (UPM)
11:00 - 11:05
Day opening
Welcome to PEPM19
PEPM
C: Atsushi IgarashiKyoto University, Japan, C: 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)
PEPM
Christian HumerOracle Labs, Switzerland
File Attached
12:00 - 12:30
Talk
A Simpler Lambda Calculus
PEPM
Barry JayUniversity of Technology Sydney
DOI
11:00 - 12:30: Research Papers: Proof Theory, Theory of Programming LanguagesCPP at Sala XII
Chair(s): Assia MahboubiINRIA
11:00 - 11:30
Research paper
A Proof-Theoretic Approach to Certifying Skolemization
CPP
Kaustuv ChaudhuriInria, France, Matteo ManighettiInria & École Polytechnique, Dale MillerINRIA Saclay and LIX
DOI
11:30 - 12:00
Research paper
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
CPP
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
CPP
Theo WinterhalterGallinette / Inria / LS2N, Nicolas TabareauInria, Matthieu SozeauInria
DOI
11:15 - 12:30: Causality, ReversibilityOPCT at Sala VII
Chair(s): Thomas H. Hildebrandt
11:15 - 11:40
Talk
Causal Reasoning for Safety
OPCT
Georgiana CaltaisUniversity of Konstanz
File Attached
11:40 - 12:05
Talk
A Calculus of Branching Processes
OPCT
12:05 - 12:30
Talk
An Axiomatic Approach to Reversible Computation
OPCT
Irek UlidowskiUniversity of Leicester
12:30 - 14:00: Monday LunchWorkshops at Lunch Room
12:30 - 14:00
Lunch
Lunch
Workshops
13:50 - 15:30: Session Types, Graph-RewritingOPCT 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
OPCT
14:15 - 14:40
Talk
From Testing Preorders to Flaky Tests
OPCT
Giovanni BernardiUniversité Paris Diderot
File Attached
14:40 - 15:05
Talk
Multiparty Reactive Sessions
OPCT
Cinzia Di GiustoLaboratoire I3S
File Attached
15:05 - 15:30
Talk
Independence, Concurrency and Abstraction in Graph-Rewriting Processes
OPCT
14:00 - 15:30: Probabilistic SystemsVMCAI at Sala III
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA
14:00 - 14:30
Talk
Syntactic Partial Order Compression for Probabilistic Reachability
VMCAI
14:30 - 15:00
Talk
Termination of Nondeterministic Probabilistic Programs
VMCAI
Hongfei FuIST Austria, Krishnendu ChatterjeeIST Austria
15:00 - 15:30
Talk
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
VMCAI
Stefan Haar, Juraj KolčákLSV, CNRS & ENS Cachan, University Paris Saclay, Loïc Paulevé
14:00 - 15:30: PADL Session 1PADL at Sala IV
13:50 - 14:00
Day opening
PADL Opening and Welcome
PADL
Moa JohanssonChalmers University of Technology, José Julio AlferesNOVA LINCS -- Universidade Nova de Lisboa
14:00 - 14:30
Talk
Natural Language Generation From Ontologies
PADL
14:30 - 15:00
Talk
Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP
PADL
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
PADL
Michael HanusKiel University
File Attached
14:00 - 15:30: Tutorial 7ATutorialFest at Sala IX
14:00 - 15:30
Talk
[T7] Higher-Order Probabilistic Programming
TutorialFest
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France
Pre-print
14:00 - 15:30: Tutorial 5ATutorialFest at Sala V
14:00 - 15:30
Talk
[T5] Correct-by-Construction Programming in Agda
TutorialFest
Andreas AbelGothenburg University, Jesper CockxChalmers | University of Gothenburg
14:00 - 15:30: Tutorial 8ATutorialFest at Sala VI
14:00 - 15:30
Talk
[T8] Building Your Own Modular Static Analyser with Infer
TutorialFest
Jules VillardFacebook London, Ezgi ÇiçekFacebook London, Mehdi BouazizFacebook London, Nikos Gorogiannis
14:00 - 15:30: Tutorial 6ATutorialFest at Sala VIII
14:00 - 15:30
Talk
[T6] Session-Typed Concurrent Programming
TutorialFest
Stephanie BalzerCarnegie Mellon University, USA
14:00 - 15:30: Session 2PEPM at Sala X
Chair(s): Thomas P. JensenINRIA Rennes
14:00 - 14:30
Talk
Method Name Suggestion with Hierarchical Attention Networks
PEPM
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
PEPM
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
PEPM
Gabriel RadanneUniversity of Freiburg, Germany
DOI Pre-print File Attached
14:00 - 15:30: Research Papers: Program VerificationCPP at Sala XII
Chair(s): Chris HawblitzelMicrosoft Research
14:00 - 14:30
Research paper
Formally Verified Big Step Semantics out of x86-64 Binaries
CPP
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
CPP
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
CPP
Nicolas Koh, Yao LiUniversity of Pennsylvania, Yishuai LiUniversity of Pennsylvania, Li-yao XiaUniversity of Pennsylvania, Lennart BeringerPrinceton University, Wolf Honore, William ManskyUniversity of Illinois at Chicago, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
DOI
16:00 - 17:30: PADL Session 2PADL at Sala IV
16:00 - 16:30
Talk
Faster Coroutine Pipelines: A Reconstruction
PADL
16:30 - 17:00
Talk
Distributed Protocol Combinators
PADL
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
PADL
Alejandro SerranoUtrecht University, Netherlands, Victor Cacciari MiraldoUtrecht University, Netherlands
Link to publication DOI File Attached
16:00 - 17:30: Tutorial 7BTutorialFest at Sala IX
16:00 - 17:30
Talk
[T7] Higher-Order Probabilistic Programming
TutorialFest
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France
Pre-print
16:00 - 17:30: Tutorial 5BTutorialFest at Sala V
16:00 - 17:30
Talk
[T5] Correct-by-Construction Programming in Agda
TutorialFest
Andreas AbelGothenburg University, Jesper CockxChalmers | University of Gothenburg
16:00 - 17:30: Tutorial 8BTutorialFest at Sala VI
16:00 - 17:30
Talk
[T8] Building Your Own Modular Static Analyser with Infer
TutorialFest
Jules VillardFacebook London, Ezgi ÇiçekFacebook London, Mehdi BouazizFacebook London, Nikos Gorogiannis
16:00 - 17:15: Concurrent Programming, Memory ModelsOPCT at Sala VII
Chair(s): Gustavo PetriIRIF, Université Paris Diderot
16:00 - 16:25
Talk
Linearizability in the Context of Weak Memory Models
OPCT
Kirsten WinterThe University of Queensland
File Attached
16:25 - 16:50
Talk
IPA: Invariant-preserving Applications for Weakly Consistent Replicated Databases
OPCT
Carla FerreiraUniversidade Nova Lisboa
16:50 - 17:15
Talk
Compositional Reasoning for Termination of Fine-grained Concurrent Programs
OPCT
Emanuele D'OsualdoImperial College London, UK
Pre-print File Attached
16:00 - 17:30: Tutorial 6BTutorialFest at Sala VIII
16:00 - 17:30
Talk
[T6] Session-Typed Concurrent Programming
TutorialFest
Stephanie BalzerCarnegie Mellon University, USA
16:00 - 17:30: Session 3PEPM at Sala X
Chair(s): Atsushi IgarashiKyoto University, Japan
16:00 - 17:00
Talk
What Is the Type of a Partial Evaluator? (Invited Talk)
PEPM
Jens PalsbergUniversity of California, Los Angeles (UCLA)
File Attached
17:00 - 17:30
Talk
Combining Higher-Order Model Checking with Refinement Type Inference
PEPM
Ryosuke SatoKyushu University, Japan, Naoki IwayamaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan
DOI
16:00 - 17:30: Research Papers: Formalization of Mathematics and Computer AlgebraCPP 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
CPP
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
CPP
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
CPP
DOI
17:30 - 18:30: Monday Social HourWorkshops at Galeria
17:30 - 18:30
Social Event
Social Hour
Workshops

Tue 15 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:30: Invited Talk 3VMCAI at Sala III
Chair(s): Ruzica PiskacYale University, USA
09:00 - 10:30
Talk
Semantics for Compiler IRs: Undefined Behavior is not Evil!
VMCAI
Nuno P. LopesMicrosoft Research
09:00 - 10:30: Keynote 2 and Research PaperCPP at Sala XII
Chair(s): Assia MahboubiINRIA
09:00 - 10:00
Talk
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
CPP
Jasmin BlanchetteVrije Universiteit Amsterdam
DOI
10:00 - 10:30
Research paper
A Verified Prover Based on Ordered Resolution
CPP
Anders SchlichtkrullTechnical University of Denmark, Jasmin BlanchetteVrije Universiteit Amsterdam, Dmitriy TraytelETH Zurich
DOI
11:00 - 12:30: PLMW Session 2PLMW at Sala II
11:00 - 11:30
Talk
Research Skills: How to Choose Research Areas
PLMW
Pre-print File Attached
11:30 - 12:30
Talk
Panel: Grad School and Beyond
PLMW
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: Software Verification and SynthesisVMCAI at Sala III
Chair(s): Ori LahavTel Aviv University
11:00 - 11:30
Talk
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
VMCAI
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
VMCAI
12:00 - 12:30
Talk
Program Synthesis with Equivalence Reduction
VMCAI
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison
11:00 - 12:30: BLAFI at Sala VI
Chair(s): Steven HoltzenUniversity of California, Los Angeles
11:00 - 11:30
Talk
The Geometry of Bayesian Programming
LAFI
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Naohiko HoshinoKyoto University
11:30 - 12:00
Talk
Model and Inference Combinators for Deep Probabilistic Programming
LAFI
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
LAFI
Media Attached
11:00 - 12:30: Session 4PEPM 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)
PEPM
File Attached
12:00 - 12:30
Talk
Control Flow Obfuscation via CPS Transformation
PEPM
Kenny Zhuo Ming LuNanyang Polytechnic, Singapore
DOI
11:00 - 12:30: Research Papers: Rewriting, Automated ReasoningCPP 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
CPP
Kathrin StarkSaarland University, Germany, Steven SchäferSaarland University, Jonas Kaiser
DOI
11:30 - 12:00
Research paper
Certified ACKBO
CPP
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
CPP
DOI
11:15 - 12:30: Cyberphysical Systems, Hybrid SystemsOPCT at Sala VII
Chair(s): Philippa GardnerImperial College London
11:15 - 11:40
Talk
Hybrid Systems Reachability Analysis
OPCT
Erika AbrahamRWTH Aachen University
11:40 - 12:05
Talk
Attribute Based Communication for Collective Adaptive Systems
OPCT
12:05 - 12:30
Talk
Designing Resilient Large Scaled CPS: Models, Languages and Tools
OPCT
Michele LoretiUniversity of Camerino
12:30 - 14:00: Tuesday LunchWorkshops at Lunch Room
12:30 - 14:00
Lunch
Lunch
Workshops
14:00 - 15:30: PLMW Session 3PLMW at Sala II
14:00 - 14:45
Talk
Technical Talk: How to Think about Types
PLMW
Frank PfenningCarnegie Mellon University, USA
Pre-print File Attached
14:45 - 15:30
Talk
Technical Talk: What Is Programming Languages Research?
PLMW
Michael HicksUniversity of Maryland, College Park
Pre-print File Attached
14:00 - 15:30: Software VerificationVMCAI at Sala III
Chair(s): Grigory FedyukovichPrinceton University
14:00 - 14:30
Talk
Type-directed Bounding of Collections in Reactive Programs
VMCAI
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
VMCAI
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
VMCAI
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
14:00 - 15:30: PADL Session 5PADL at Sala IV
14:00 - 14:30
Talk
Composing Syntactical Constructs to Create Domain-Specific Languages
PADL
David BromanKTH Royal Institute of Technology, Viktor PalmkvistKTH Royal Institute of Technology
DOI Media Attached
14:30 - 15:00
Talk
Proof Carrying Plans
PADL
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
PADL
Paul TarauUniversity of North Texas
14:00 - 15:30: Session 5PEPM 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
PEPM
Kenichi AsaiOchanomizu University
DOI File Attached
14:30 - 15:00
Talk
Futures and Promises in Haskell and Scala
PEPM
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
PEPM
Jeremy YallopUniversity of Cambridge, UK, Oleg Kiselyov
DOI Pre-print
15:28 - 15:30
Poster
Advanced Futures and Promises in C++ (poster)
PEPM
Tamino DauthKarlsruhe University of Applied Sciences, Germany, Martin SulzmannKarlsruhe University of Applied Sciences, Germany
14:00 - 15:30: Research Papers: Program VerificationCPP at Sala XII
Chair(s): Nicolas TabareauInria
14:00 - 14:30
Research paper
A Verified Protocol Buffer Compiler
CPP
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
CPP
Véronique BenzakenLRI, Université Paris-Sud, Evelyne Contejean
DOI
15:00 - 15:30
Research paper
Dynamic Class Initialization Semantics: a Jinja Extension
CPP
Susannah Mansky, Elsa GunterUniversity of Illinois
DOI
16:00 - 17:30: PLMW Session 4PLMW at Sala II
16:00 - 16:30
Talk
Research Skills: How to Bootstrap a Research Project
PLMW
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
PLMW
Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon, Deepak GargMax Planck Institute for Software Systems, Philippa GardnerImperial College London, Atsushi IgarashiKyoto University, Japan, Neel KrishnaswamiComputer Laboratory, University of Cambridge
Pre-print
16:00 - 17:30: Networks and ConcurrencyVMCAI at Sala III
Chair(s): Cezara DrăgoiINRIA, ENS, CNRS
16:00 - 16:30
Talk
On the Semantics of Snapshot Isolation
VMCAI
Azalea RaadMPI-SWS, Germany, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, Germany
16:30 - 17:00
Talk
Fast BGP Simulation of Large Datacenters
VMCAI
Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research
17:00 - 17:30
Talk
Parametric Timed Broadcast Protocols
VMCAI
Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye, Paulin Fournier, Didier Lime
File Attached
16:00 - 17:30: DLAFI at Sala VI
16:00 - 16:30
Talk
Probabilistic Programming Inference via Intensional Semantics
LAFI
Simon Castellan, Hugo PaquetUniversity of Cambridge
16:30 - 17:00
Talk
Factorized Exact Inference for Discrete Probabilistic Programs
LAFI
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
LAFI
Matthew HeimerdingerIndiana University, Chung-chieh ShanIndiana University, USA
16:00 - 17:20: Algebra, CoalgebraOPCT at Sala VII
Chair(s): Alexandra SilvaUniversity College London
16:00 - 16:25
Talk
Coalgebra Learning via Duality
OPCT
Jurriaan RotRadboud University Nijmegen
16:25 - 16:50
Talk
A Metric Semantics for Coordination Languages
OPCT
Valentina CastiglioniInria Saclay - Ile de France
File Attached
16:50 - 17:15
Talk
Hybrid System Iteration
OPCT
Renato NevesUniversity of Minho & INESC TEC
File Attached
17:15 - 17:20
Day closing
Closing
OPCT
16:00 - 17:30: Research Papers: Formalization of Mathematics and Computer AlgebraCPP 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
CPP
Yannick ForsterSaarland University, Dominik KirstSaarland University, Gert SmolkaSaarland University
DOI
16:30 - 17:00
Research paper
Verified Solving and Asymptotics of Linear Recurrences
CPP
Manuel EberlTechnische Universität München
DOI
17:00 - 17:30
Meeting
Business Meeting
CPP
Assia MahboubiINRIA, Magnus O. MyreenChalmers University of Technology, Sweden
17:30 - 18:30: Tuesday Social HourWorkshops at Galeria
17:30 - 18:30
Social Event
Social Hour
Workshops

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:05: Welcome & Keynote IResearch Papers at Sala I + II
Chair(s): Peter O'HearnFacebook
09:00 - 09:05
Day opening
Welcome
Research Papers
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
Research Papers
Mark HarmanFacebook and University College London
Media Attached
10:35 - 12:03: Reasoning about Probabilistic ProgramsResearch Papers at Sala I
Chair(s): Jan HoffmannCarnegie Mellon University
10:35 - 10:57
Talk
Formal Verification of Higher-Order Probabilistic Programs
Research Papers
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
Research Papers
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
Research Papers
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
Research Papers
Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison
Link to publication DOI Media Attached
10:35 - 12:03: ConcurrencyResearch Papers at Sala II
Chair(s): Ori LahavTel Aviv University
10:35 - 10:57
Talk
A True Positives Theorem for a Static Race Detector
Research Papers
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
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
11:19 - 11:41
Talk
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Research Papers
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
Research Papers
Michael EmmiSRI International, Constantin EneaUniversité Paris Diderot
Link to publication DOI Media Attached File Attached
12:03 - 13:45: Wednesday LunchResearch Papers at Lunch Room
12:03 - 13:45
Lunch
Lunch
Research Papers
13:45 - 14:51: Probabilistic Programming and SemanticsResearch Papers 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
Research Papers
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
Research Papers
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
Research Papers
Feras SaadMassachusetts Institute of Technology, Marco Cusumano-TownerMIT-CSAIL, Ulrich SchaechtleMassachusetts Institute of Technology, USA, Martin RinardMassachusetts Institute of Technology, Vikash MansinghkaMIT
Link to publication DOI Media Attached File Attached
13:45 - 14:51: CategoriesResearch Papers at Sala II
Chair(s): Nicolas TabareauInria
13:45 - 14:07
Talk
Familial Monads and Structural Operational Semantics
Research Papers
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
Research Papers
Jasmin 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
Research Papers
Paul-André MelliesCNRS and University Paris Diderot
Link to publication DOI Media Attached File Attached
15:21 - 16:27: Machine Learning and Linear AlgebraResearch Papers at Sala I
Chair(s): Aws AlbarghouthiUniversity of Wisconsin-Madison
15:21 - 15:43
Talk
code2vec: Learning Distributed Representations of Code
Research Papers
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
Research Papers
Link to publication DOI Media Attached
16:05 - 16:27
Talk
Closed Forms for Numerical Loops
Research Papers
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
15:21 - 16:27: Capabilities and Session Types IResearch Papers 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
Research Papers
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
Research Papers
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
Research Papers
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
16:37 - 17:43: Quantum ProgrammingResearch Papers at Sala I
Chair(s): Jens PalsbergUniversity of California, Los Angeles (UCLA)
16:37 - 16:59
Talk
Quantitative Robustness Analysis of Quantum Programs
Research Papers
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
Research Papers
Link to publication DOI Media Attached
17:21 - 17:43
Talk
Quantum Relational Hoare Logic
Research Papers
Dominique UnruhUniversity of Tartu
Link to publication DOI Pre-print Media Attached File Attached
16:37 - 17:43: Session Types IIResearch Papers at Sala II
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
16:37 - 16:59
Talk
Interconnectability of Session-Based Logical ProcessesTOPLAS
Research Papers
Bernardo ToninhoImperial College London, 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
Research Papers
David Castro-PerezImperial 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
Research Papers
Alceste ScalasImperial College London, Nobuko YoshidaImperial College London
Link to publication DOI Pre-print Media Attached File Attached
18:00 - 18:30: Wednesday Evening Program IResearch Papers at Sala I
18:00 - 18:30
Talk
Microsoft Research: Engage, Verify, Open
Research Papers
Thomas BallMicrosoft Research
Media Attached
18:30 - 19:30: Wednesday Evening Program IIResearch Papers / Student Research Competition at Galeria
18:30 - 19:30
Social Event
Student Research Competition and Reception supported by Microsoft Research
Student Research Competition

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:06: Type Abstraction and EffectsResearch Papers at Sala I
Chair(s): Benjamin DelawarePurdue University
09:00 - 09:22
Talk
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Yizhou ZhangCornell University, Andrew C. MyersCornell University
Link to publication DOI Media Attached
09:22 - 09:44
Talk
Abstracting Algebraic Effects
Research Papers
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
Research Papers
Karl CraryCarnegie Mellon University
Link to publication DOI Media Attached File Attached
09:00 - 10:06: SynthesisResearch Papers at Sala II
Chair(s): Robbert KrebbersDelft University of Technology
09:00 - 09:22
Talk
Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper
Research Papers
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
Research Papers
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
Research Papers
Farzin HoushmandUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside
Link to publication DOI Media Attached
10:30 - 12:30: Finalist Poster PresentationsStudent Research Competition at Sala III
10:36 - 12:04: Gradual TypesResearch Papers at Sala I
Chair(s): Nikhil SwamyMicrosoft Research
10:36 - 10:58
Talk
Type-Driven Gradual Security with ReferencesTOPLAS
Research Papers
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
Research Papers
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
Research Papers
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
Research Papers
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: Separation Logic and Memory SemanticsResearch Papers 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
Research Papers
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
Research Papers
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
Research Papers
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, Neel 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
Research Papers
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: Thursday LunchResearch Papers at Lunch Room
12:04 - 13:45
Lunch
Lunch
Research Papers
13:45 - 14:51: Type Inference IResearch Papers 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
Research Papers
Jana DunfieldQueen's University, Kingston, Ontario, Neel 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
Research Papers
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
Research Papers
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: Weak MemoryResearch Papers at Sala II
Chair(s): Scott OwensUniversity of Kent, UK
13:45 - 14:07
Talk
On Library Correctness under Weak Memory Consistency
Research Papers
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
Research Papers
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
Research Papers
Soham ChakrabortyMax Planck Institute for Software Systems, Viktor VafeiadisMPI-SWS, Germany
Link to publication DOI Media Attached File Attached
15:21 - 16:49: Type Inference IIResearch Papers at Sala I
Chair(s): Niki VazouIMDEA Software Institute
15:21 - 15:43
Talk
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
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
Research Papers
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
Research Papers
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
Research Papers
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
Link to publication DOI Media Attached File Attached
15:21 - 16:49: TimeResearch Papers at Sala II
Chair(s): Andrew C. MyersCornell University
15:21 - 15:43
Talk
Type-Guided Worst-Case Input Generation
Research Papers
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
Research Papers
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
Research Papers
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
Research Papers
Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Chih-Duo HongUniversity of Oxford
Media Attached File Attached
17:00 - 18:00: Business MeetingResearch Papers at Sala I + II
17:00 - 17:15
Other
PC Chair Report
Research Papers
Stephanie WeirichUniversity of Pennsylvania, USA
Media Attached
17:15 - 17:25
Awards
SIGPLAN Awards
Research Papers
Benjamin C. PierceUniversity of Pennsylvania
Media Attached
17:25 - 17:30
Other
POPL 2020 Announcement
Research Papers
Brigitte PientkaMcGill University, Lars BirkedalAarhus University
Media Attached
17:30 - 17:40
Other
NSF funding for PL
Research Papers
Rance CleavelandUniversity of Maryland
Media Attached
17:40 - 17:50
Other
SIGPLAN Climate Committee Report
Research Papers
Benjamin C. PierceUniversity of Pennsylvania
Media Attached
17:50 - 18:00
Other
State of SIGPLAN
Research Papers
Jens PalsbergUniversity of California, Los Angeles (UCLA)
Media Attached
18:15 - 19:15: Reception supported by FacebookResearch Papers at Galeria
18:15 - 19:15
Social Event
Reception supported by Facebook
Research Papers

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:05: SRC Announcement & Keynote IIResearch Papers / Student Research Competition at Sala I + II
Chair(s): Stephanie WeirichUniversity of Pennsylvania, USA
09:00 - 09:05
Awards
SRC Announcement
Student Research Competition
Niki VazouIMDEA Software Institute
Media Attached
09:05 - 10:05
Talk
Mechanized Metatheory - The Next Chapter
Research Papers
Brigitte PientkaMcGill University
Media Attached File Attached
10:35 - 12:03: Abstract InterpretationResearch Papers at Sala II
Chair(s): David NaumannStevens Institute of Technology
10:35 - 10:57
Talk
A^2 I: Abstract^2 InterpretationDistinguished Paper
Research Papers
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
Research Papers
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
Research Papers
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
Research Papers
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
12:03 - 13:45: Friday LunchResearch Papers at Lunch Room
12:03 - 13:45
Lunch
Lunch
Research Papers
13:45 - 14:51: SemanticsResearch Papers 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
Research Papers
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
Research Papers
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
Research Papers
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
13:45 - 14:51: Model CheckingResearch Papers 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
Research Papers
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
Research Papers
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
Research Papers
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
15:21 - 16:27: Security and Information FlowResearch Papers at Sala I
Chair(s): David WalkerPrinceton University
15:21 - 15:43
Talk
LWeb: Information Flow Security for Multi-Tier Web Applications
Research Papers
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
Research Papers
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
Research Papers
Alex KavvosWesleyan University
Link to publication DOI Pre-print File Attached
15:21 - 16:27: Program Analysis IResearch Papers at Sala II
Chair(s): Michael D. AdamsUniversity of Utah
15:21 - 15:43
Talk
Decidable Verification of Uninterpreted Programs
Research Papers
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
Research Papers
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
Research Papers
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
16:37 - 17:43: Verified Compilation and ConcurrencyResearch Papers 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.
Research Papers
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
Research Papers
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
Research Papers
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
16:37 - 17:43: Program Analysis IIResearch Papers at Sala II
Chair(s): Michael EmmiSRI International
16:37 - 16:59
Talk
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Research Papers
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
Research Papers
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
Research Papers
Valentin TouzeauUniv. Grenoble Alpes, Claire MaizaVerimag, France, David MonniauxCNRS, VERIMAG, Jan ReinekeSaarland University
Link to publication DOI Media Attached File Attached
17:45 - 18:45: Friday Social HourResearch Papers at Galeria
17:45 - 18:45
Social Event
Social Hour
Research Papers

Sat 19 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:30: Keynote & Contributed Talks 1CoqPL at Sala VI
Chair(s): Ilya SergeyYale-NUS College and National University of Singapore
09:00 - 09:05
Day opening
Opening
CoqPL
09:05 - 10:05
Talk
Coq User Interfaces: Past, Present, and Future (Keynote)
CoqPL
10:05 - 10:30
Talk
Counterexamples for Coq Conjectures
CoqPL
Sam GruetterMassachusetts Institute of Technology
File Attached
09:00 - 10:30: KeynoteOff the Beaten Track at Sala VII
Chair(s): Luke Church
09:30 - 10:30
Talk
De-escalating Software (Keynote)
Off the Beaten Track
Stephen KellUniversity of Kent
11:15 - 12:30: Contributed Talks 2CoqPL at Sala VI
Chair(s): Enrico TassiINRIA
11:15 - 11:40
Talk
Towards Mechanising Probabilistic Properties of a Blockchain
CoqPL
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
CoqPL
Karl PalmskogUniversity of Texas at Austin, Milos GligoricUniversity of Texas at Austin, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
File Attached
12:05 - 12:30
Talk
WIP: Formalizing the Concordium Consensus Protocol in Coq
CoqPL
Thomas Dinsdale-Young, Bas SpittersAarhus University, Søren Eller ThomsenAarhus University, Daniel TschudiAarhus University
File Attached
12:30 - 14:00: Saturday LunchWorkshops at Lunch Room
12:30 - 14:00
Lunch
Lunch
Workshops
14:00 - 15:30: Contributed Talks 3 & Coq DevelopersCoqPL 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
CoqPL
Vadim ZalivaCarnegie Mellon University, USA, Matthieu SozeauInria
File Attached
14:25 - 14:50
Talk
Reifying and Translating a Monadic Fragment of Gallina
CoqPL
File Attached
14:50 - 15:30
Demonstration
Session with the Coq Development Team
CoqPL
14:00 - 15:30: Afternoon TalksOff the Beaten Track at Sala VII
Chair(s): Luke Church
14:00 - 14:45
Other
Design Critique and Discussion
Off the Beaten Track
14:45 - 15:30
Talk
F a Language for Music Composition
Off the Beaten Track
Joachim KristensenDIKU, University of Copenhagen, Ken Friis LarsenDIKU, University of Copenhagen
16:00 - 17:30: Informal + Business MeetingOff the Beaten Track at Sala VII
16:00 - 17:30
Meeting
Informal + Business Meeting
Off the Beaten Track