POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
VenueInstitution of Engineering and Technology
Room nameHaslett Room
Floor0
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 14 Jan

Displayed time zone: London change

09:00 - 10:30
Morning Track 1TutorialFest at Haslett Room
09:00
90m
Tutorial
Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-CompletenessRemote
TutorialFest
P. Madhusudan University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign
11:00 - 12:30
Morning Track 1TutorialFest at Haslett Room
11:00
90m
Tutorial
Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-CompletenessRemote
TutorialFest
P. Madhusudan University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign
14:00 - 15:30
Afternoon Track 1TutorialFest at Haslett Room
14:00
90m
Tutorial
Scaling Verification of Concurrent Programs with the Civl Verifier
TutorialFest
Constantin Enea Ecole Polytechnique / LIX / CNRS, Shaz Qadeer Facebook
16:00 - 17:30
Afternoon Track 1TutorialFest at Haslett Room
16:00
90m
Tutorial
Scaling Verification of Concurrent Programs with the Civl Verifier
TutorialFest
Constantin Enea Ecole Polytechnique / LIX / CNRS, Shaz Qadeer Facebook

Mon 15 Jan

Displayed time zone: London change

09:00 - 10:30
Morning Track 1TutorialFest at Haslett Room
09:00
90m
Tutorial
Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
TutorialFest
Jade Alglave Arm and University College London, Artem Khyzha Tel Aviv University, Israel, Luc Maranget Inria, Nikos Nikoleris Arm Research, Hugo O'Keeffe ARM, Hadrien Renaud UCL
11:00 - 12:30
Morning Track 1TutorialFest at Haslett Room
11:00
90m
Tutorial
Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
TutorialFest
Jade Alglave Arm and University College London, Artem Khyzha Tel Aviv University, Israel, Luc Maranget Inria, Nikos Nikoleris Arm Research, Hugo O'Keeffe ARM, Hadrien Renaud UCL
14:00 - 15:30
Afternoon Track 1TutorialFest at Haslett Room
14:00
90m
Tutorial
Machine Learning Meets Program Synthesis
TutorialFest
Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute
16:00 - 17:30
Afternoon Track 1TutorialFest at Haslett Room
16:00
90m
Tutorial
Machine Learning Meets Program Synthesis
TutorialFest
Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
Keynote & Termination analysis PEPM at Haslett Room
Chair(s): Meng Wang University of Bristol
09:00
5m
Talk
Opening
PEPM
Meng Wang University of Bristol, Gabriele Keller Utrecht University
09:05
60m
Keynote
From Theory to Practice: Crafting Differential Privacy Systems with Haskell
PEPM
Alejandro Russo Chalmers University of Technology, Sweden
10:05
25m
Talk
Productivity Verification for Functional Programs by Reduction to Termination Verification
PEPM
Ren Fukaishi The University of Tokyo, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo
DOI
11:00 - 12:30
Program Inversion & DSLsPEPM at Haslett Room
Chair(s): Youyou Cong Tokyo Institute of Technology
11:00
25m
Talk
Complete Stream Fusion for Software-Defined RadioDistinguished Paper
PEPM
Tomoaki Kobayashi Tohoku University, Oleg Kiselyov Tohoku University
DOI
11:25
25m
Talk
A Case Study in Functional Conversion and Mode Inference in miniKanren
PEPM
Ekaterina Verbitskaia JetBrains Research; Constructor University Bremen, Igor Engel JetBrains Research; Constructor University Bremen, Daniil Berezun JetBrains Research; Constructor University Bremen
DOI
11:50
25m
Talk
Partial Evaluation of Reversible Flowchart Programs
PEPM
Louis Marott Normann University of Copenhagen, Robert Glück University of Copenhagen
DOI
12:15
15m
Talk
Towards a Language-parametric DSL for Refactoring (Short Paper)
PEPM
Casper Bach Poulsen Delft University of Technology, Xulei Liu Delft University of Technology, Luka Miljak Delft University of Technology
File Attached
14:00 - 15:30
Types & Staging PEPM at Haslett Room
Chair(s): Gabriele Keller Utrecht University
14:00
25m
Talk
An Intrinsically Typed Compiler for Algebraic Effect Handlers
PEPM
Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
DOI
14:25
25m
Talk
Ownership Types for Verification of Programs with Pointer Arithmetic
PEPM
Izumi Tanaka University of Tokyo, Ken Sakayori University of Tokyo, Naoki Kobayashi University of Tokyo
DOI
14:50
25m
Talk
Scoped and Typed Staging by EvaluationRemote
PEPM
Guillaume Allais University of Strathclyde
DOI Pre-print
15:15
15m
Talk
One-Pass CPS Translation of Dependent Types (Talk Proposal)
PEPM
Youyou Cong Tokyo Institute of Technology
Pre-print
16:00 - 18:30
History of PEPMPEPM at Haslett Room
Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
16:00
30m
Talk
In memoriam Neil Deaton Jones
PEPM
Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
DOI
16:30
30m
Talk
The Genesis of Mix: Early Days of Self-Applicable Partial Evaluation (Invited Contribution)
PEPM
Peter Sestoft IT University of Copenhagen, Harald Sondergaard The University of Melbourne
DOI
17:00
30m
Talk
A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
PEPM
Alberto Pettorossi University of Rome Tor Vergata; IASI-CNR, Maurizio Proietti IASI-CNR, Fabio Fioravanti University of Chieti-Pescara, Emanuele De Angelis IASI-CNR
DOI
17:30
30m
Talk
Incremental Computation: What Is the Essence? (Invited Contribution)Remote
PEPM
Y. Annie Liu Stony Brook University
DOI
18:00
30m
Meeting
Informal discussion on history and future of PEPM
PEPM

Sat 20 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1WITS at Haslett Room
Chair(s): Richard A. Eisenberg Jane Street
09:00
60m
Keynote
Inside the Scala Capture Checker
WITS
10:00
30m
Talk
Binding Syntax for Dependently-Typed Programs
WITS
Andre Videla University Of Strathclyde
11:00 - 12:30
Session 2WITS at Haslett Room
Chair(s): William J. Bowman University of British Columbia
11:00
30m
Talk
Retrofitting Null-Safety into Java
WITS
Artem Pianykh Facebook London
12:00
30m
Talk
Type inference for application spines
WITS
Simon Peyton Jones Epic Games
14:00 - 15:30
Session 3WITS at Haslett Room
14:00
30m
Talk
On Modelling Heap Invariants for Type Systems in Dafny
WITS
James Noble Creative Research & Programming, Tobias Wrigstad Uppsala University
14:30
30m
Talk
Solving constraints during type inference
WITS
Simon Peyton Jones Epic Games
15:00
30m
Talk
Yaffle: A New Core for Idris 2
WITS
Edwin Brady University of St Andrews, UK
16:00 - 17:30
Session 4WITS at Haslett Room
Chair(s): Edwin Brady University of St Andrews, UK
16:00
30m
Talk
asai: a Library for Compiler Diagnostics
WITS
Kuen-Bang Hou (Favonia) University of Minnesota, Reed Mullanix McMaster University
16:30
30m
Talk
Efficient Evaluation with Controlled Definition Unfolding
WITS
András Kovács University of Gothenburg
17:00
30m
Talk
Implementing separation logic using an SMT-backed Frame RuleRemote
WITS
Kirill Golubev University of Lisbon, Alcides Fonseca University of Lisbon

Sun 14 Jan

Displayed time zone: London change

Mon 15 Jan

Displayed time zone: London change

Tue 16 Jan

Displayed time zone: London change

Sat 20 Jan

Displayed time zone: London change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Haslett Room