PADL 2024
Dates to be announced
London, United Kingdom
co-located with
POPL 2024
Toggle navigation
Attending
Venue: Institution of Engineering and Technology
Program
PADL Program
Your Program
Tue 31 Dec
Track/Call
Organization
PADL 2024 Committees
Track Committees
Programme Chairs
Program Committee
Contributors
People Index
Search
Series
Series
PADL 2025
PADL 2024
PADL 2023
PADL 2022
PADL 2021
PADL 2020
PADL 2019
PADL 2018
PADL 2017
PADL
Sign in
Sign up
POPL 2024
(
series
) /
PADL 2024 (
series
) /
Institution of Engineering and Technology
/
Room information: Haslett Room
Venue
Institution of Engineering and Technology
Room name
Haslett Room
Floor
0
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT) London
.
Use conference time zone: (GMT) London
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 14 Jan
Displayed time zone:
London
change
09:00 - 10:30
Morning Track 1
POPL TutorialFest
at
Haslett Room
09:00
90m
Tutorial
Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-Completeness
Remote
POPL TutorialFest
P. Madhusudan
University of Illinois at Urbana-Champaign
,
Adithya Murali
University of Illinois at Urbana-Champaign
11:00 - 12:30
Morning Track 1
POPL TutorialFest
at
Haslett Room
11:00
90m
Tutorial
Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-Completeness
Remote
POPL TutorialFest
P. Madhusudan
University of Illinois at Urbana-Champaign
,
Adithya Murali
University of Illinois at Urbana-Champaign
14:00 - 15:30
Afternoon Track 1
POPL TutorialFest
at
Haslett Room
14:00
90m
Tutorial
Scaling Verification of Concurrent Programs with the Civl Verifier
POPL TutorialFest
Constantin Enea
Ecole Polytechnique / LIX / CNRS
,
Shaz Qadeer
Facebook
16:00 - 17:30
Afternoon Track 1
POPL TutorialFest
at
Haslett Room
16:00
90m
Tutorial
Scaling Verification of Concurrent Programs with the Civl Verifier
POPL TutorialFest
Constantin Enea
Ecole Polytechnique / LIX / CNRS
,
Shaz Qadeer
Facebook
Mon 15 Jan
Displayed time zone:
London
change
09:00 - 10:30
Morning Track 1
POPL TutorialFest
at
Haslett Room
09:00
90m
Tutorial
Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
POPL 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 1
POPL TutorialFest
at
Haslett Room
11:00
90m
Tutorial
Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
POPL 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 1
POPL TutorialFest
at
Haslett Room
14:00
90m
Tutorial
Machine Learning Meets Program Synthesis
POPL TutorialFest
Nathanaël Fijalkow
CNRS, LaBRI, and Alan Turing Institute
16:00 - 17:30
Afternoon Track 1
POPL TutorialFest
at
Haslett Room
16:00
90m
Tutorial
Machine Learning Meets Program Synthesis
POPL 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 & DSLs
PEPM
at
Haslett Room
Chair(s):
Youyou Cong
Tokyo Institute of Technology
11:00
25m
Talk
Complete Stream Fusion for Software-Defined Radio
Distinguished 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 Evaluation
Remote
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 PEPM
PEPM
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 1
WITS
at
Haslett Room
Chair(s):
Richard A. Eisenberg
Jane Street
09:00
60m
Keynote
Inside the Scala Capture Checker
WITS
Martin Odersky
EPFL
10:00
30m
Talk
Binding Syntax for Dependently-Typed Programs
WITS
Andre Videla
University Of Strathclyde
11:00 - 12:30
Session 2
WITS
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 3
WITS
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 4
WITS
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 Rule
Remote
WITS
Kirill Golubev
University of Lisbon
,
Alcides Fonseca
University of Lisbon
Sun 14 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Haslett Room
POPL TutorialFest
Morning Track 1
POPL TutorialFest
Morning Track 1
POPL TutorialFest
Afternoon Track 1
POPL TutorialFest
Afternoon Track 1
Mon 15 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Haslett Room
POPL TutorialFest
Morning Track 1
POPL TutorialFest
Morning Track 1
POPL TutorialFest
Afternoon Track 1
POPL TutorialFest
Afternoon Track 1
Tue 16 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Haslett Room
PEPM
Keynote & Termination analysis
PEPM
Program Inversion & DSLs
PEPM
Types & Staging
PEPM
History of PEPM
Sat 20 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Haslett Room
WITS
Session 1
WITS
Session 2
WITS
Session 3
WITS
Session 4
Sun 14 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Haslett Room
POPL TutorialFest
Remote
Automated Datastructure Verification using Unfoldings and SMT Solving: ...
09:00 - 10:30
POPL TutorialFest
Remote
Automated Datastructure Verification using Unfoldings and SMT Solving: ...
11:00 - 12:30
POPL TutorialFest
Scaling Verification of Concurrent Programs with the Civl Verifier
14:00 - 15:30
POPL TutorialFest
Scaling Verification of Concurrent Programs with the Civl Verifier
16:00 - 17:30
Mon 15 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Haslett Room
POPL TutorialFest
Arm Architecture and Formal Artifacts: Memory Model and Instruction Sem ...
09:00 - 10:30
POPL TutorialFest
Arm Architecture and Formal Artifacts: Memory Model and Instruction Sem ...
11:00 - 12:30
POPL TutorialFest
Machine Learning Meets Program Synthesis
14:00 - 15:30
POPL TutorialFest
Machine Learning Meets Program Synthesis
16:00 - 17:30
Tue 16 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
Haslett Room
PEPM
Opening
09:00 - 09:05
PEPM
From Theory to Practice: Crafting Differential Privacy Systems with Haskell
09:05 - 10:05
PEPM
Productivity Verification for Functional Programs by Reduction to Termi ...
10:05 - 10:30
PEPM
Distinguished Paper
Complete Stream Fusion for Software-Defined Radio
11:00 - 11:25
PEPM
A Case Study in Functional Conversion and Mode Inference in miniKanren
11:25 - 11:50
PEPM
Partial Evaluation of Reversible Flowchart Programs
11:50 - 12:15
PEPM
Towards a Language-parametric DSL for Refactoring (Short Paper)
12:15 - 12:30
PEPM
An Intrinsically Typed Compiler for Algebraic Effect Handlers
14:00 - 14:25
PEPM
Ownership Types for Verification of Programs with Pointer Arithmetic
14:25 - 14:50
PEPM
Remote
Scoped and Typed Staging by Evaluation
14:50 - 15:15
PEPM
One-Pass CPS Translation of Dependent Types (Talk Proposal)
15:15 - 15:30
PEPM
In memoriam Neil Deaton Jones
16:00 - 16:30
PEPM
The Genesis of Mix: Early Days of Self-Applicable Partial Evaluation (I ...
16:30 - 17:00
PEPM
A Historical Perspective on Program Transformation and Recent Developme ...
17:00 - 17:30
PEPM
Remote
Incremental Computation: What Is the Essence? (Invited Contribution)
17:30 - 18:00
PEPM
Informal discussion on history and future of PEPM
18:00 - 18:30
Sat 20 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Haslett Room
WITS
Inside the Scala Capture Checker
09:00 - 10:00
WITS
Binding Syntax for Dependently-Typed Programs
10:00 - 10:30
WITS
Retrofitting Null-Safety into Java
11:00 - 11:30
WITS
Type inference for application spines
12:00 - 12:30
WITS
On Modelling Heap Invariants for Type Systems in Dafny
14:00 - 14:30
WITS
Solving constraints during type inference
14:30 - 15:00
WITS
Yaffle: A New Core for Idris 2
15:00 - 15:30
WITS
asai: a Library for Compiler Diagnostics
16:00 - 16:30
WITS
Efficient Evaluation with Controlled Definition Unfolding
16:30 - 17:00
WITS
Remote
Implementing separation logic using an SMT-backed Frame Rule
17:00 - 17:30
x
Sun 22 Dec 03:08