PLDI 2024
Mon 24 - Fri 28 June 2024
Copenhagen, Denmark
Toggle navigation
Attending
Venue: Radisson Blu Scandinavia, Copenhagen
Sponsorship
Registration
Visa
Live Streams
Presenter Instructions
Program
PLDI Program
Your Program
Mon 24 Jun
Tue 25 Jun
Wed 26 Jun
Thu 27 Jun
Fri 28 Jun
Tracks
PLDI 2024
PLDI Events
Research Artifacts
PLDI Research Papers
Workshops and Tutorials
SRC
Tutorials
- Algorithms and Applications for Provable Repair of Deep Neural Networks
- Concurrent Algorithms in Kotlin Coroutines
- Democratizing DSL development with the BuildIt Framework
- Quick and dirty development of static analyses with LiSA
- Static Code Analysis with SootUp
Volunteering
Diversity, Equity and Inclusion
Co-hosted Conferences
ISMM
LCTES
Workshops
ARRAY
CP
Choreographic Programming
EGRAPHS
Infer
PLMW@PLDI
PODELSKI
PLDI Workshop Honoring Andreas Podelski
RTFM
: Red-Hot Topics in Faculty Mentoring
SOAP
Sparse
WQS
Organization
PLDI 2024 Committees
AV Committee
Organizing Committee
Track Committees
Research Artifacts
PLDI Research Papers
SRC
Contributors
People Index
Co-hosted Conferences
ISMM
Organizing Committee
Program Committee
Steering Committee
LCTES
Organizing Committee
Program Committee
Steering Committee
Workshops
ARRAY
Organizing Committee
Program Committee
CP
Organizing Committee
Program Committee
EGRAPHS
Organizing Committee
Program Committee
Infer
Organizing Committee
PLMW@PLDI
Organizing Committee
PODELSKI
Program Committee
RTFM
Organizing Committee
Speakers and Panelists
SOAP
Organizing Committee
Program Committee
Sparse
Organizing Committee
Program Committee
WQS
Organizing Committee
Program Committee
Search
Series
Series
PLDI 2025
PLDI 2024
PLDI 2023
PLDI 2022
PLDI 2021
PLDI 2020
PLDI 2019
PLDI 2018
PLDI 2017
PLDI 2016
PLDI 2015
Sign in
Sign up
PLDI 2024
(
series
) /
PLDI Research Papers
/
Verified Extraction from Coq to OCaml
Who
Yannick Forster
,
Matthieu Sozeau
,
Nicolas Tabareau
Track
PLDI 2024 PLDI Research Papers
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+02:00) Windhoek
.
Use conference time zone: (GMT+02:00) Windhoek
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06: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-06:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02: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) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03: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+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12: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
When
Wed 26 Jun 2024 14:00 - 14:20 at
Iceland / Denmark
-
Formal Verification 1
Chair(s):
Jeehoon Kang
DOI
https://doi.org/10.1145/3656379
Yannick Forster
Inria
France
Matthieu Sozeau
Inria
France
Nicolas Tabareau
Inria
France
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+02:00) Windhoek
.
Use conference time zone: (GMT+02:00) Windhoek
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06: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-06:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02: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) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03: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+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12: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
Session Program
Wed 26 Jun
Displayed time zone:
Windhoek
change
13:40 - 15:20
Formal Verification 1
PLDI Research Papers
at
Iceland / Denmark
Chair(s):
Jeehoon Kang
KAIST
13:40
20m
Talk
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
PLDI Research Papers
Gaurav Parthasarathy
ETH Zurich
,
Thibault Dardinier
ETH Zurich
,
Benjamin Bonneau
Verimag
,
Peter Müller
ETH Zurich
,
Alexander J. Summers
University of British Columbia
DOI
14:00
20m
Talk
Verified Extraction from Coq to OCaml
PLDI Research Papers
Yannick Forster
Inria
,
Matthieu Sozeau
Inria
,
Nicolas Tabareau
Inria
DOI
14:20
20m
Talk
Verification under Intel-x86 with Persistency
PLDI Research Papers
Parosh Aziz Abdulla
Uppsala University, Sweden
,
Mohamed Faouzi Atig
Uppsala University, Sweden
,
Ahmed Bouajjani
IRIF, Université Paris Diderot
,
K Narayan Kumar
Chennai Mathematical Institute
,
Prakash Saivasan
The Institute of Mathematical Sciences, India
DOI
14:40
20m
Talk
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
PLDI Research Papers
Lennard Gäher
MPI-SWS
,
Michael Sammler
MPI-SWS
,
Ralf Jung
ETH Zurich
,
Robbert Krebbers
Radboud University Nijmegen
,
Derek Dreyer
MPI-SWS
DOI
15:00
20m
Talk
Hyperblock Scheduling for Verified High-Level Synthesis
PLDI Research Papers
Yann Herklotz
Imperial College London
,
John Wickerson
Imperial College London
DOI
Pre-print
File Attached
x
Sun 22 Dec 02:31
