POPL 2023
Sun 15 - Sat 21 January 2023
Boston, Massachusetts, United States
Toggle navigation
Attending
Venue: Boston Park Plaza
Supporting POPL
Registration
Information for Students
Information for Presenters
Information for Virtual Attendees
Nearby Events
Program
POPL Program
Your Program
Filter by Day
Sun 15 Jan
Mon 16 Jan
Tue 17 Jan
Wed 18 Jan
Thu 19 Jan
Fri 20 Jan
Sat 21 Jan
Tracks
POPL 2023
POPL
Session Previews
Artifact Evaluation
Diversity, Equity and Inclusion
Student Research Competition
Student Volunteers
TutorialFest
Workshops and Co-located Events
Co-hosted Conferences
CPP
VMCAI
Workshops
CoqPL
LAFI
LAFI
- Introduction to the tensor-programs framework, a PL approach that helps analyse theoretical properties of deep learning.
PEPM
PLMW @ POPL
PriSC
ProLaLa
Co-hosted Symposia
PADL
Organization
POPL 2023 Committees
Organizing Committee
Track Committees
POPL
Artifact Evaluation
Student Research Competition
TutorialFest
Contributors
People Index
Co-hosted Conferences
CPP
Organizing Committee
Program Committee
Steering Committee
VMCAI
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PLMW @ POPL
Organizing Committee
Speakers
Panelists
PriSC
Program Committee
Steering Committee
ProLaLa
Program Committee
Co-hosted Symposia
PADL
Programme Chairs
Program Committee
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2023
(
series
) /
Boston Park Plaza
/
Room information: Park
Venue
Boston Park Plaza
Room name
Park
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-05:00) Eastern Time (US & Canada)
.
Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)
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
Mon 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:30
Tutorials 2A
TutorialFest
at
Park
09:00
90m
Tutorial
Isabelle/HOL: Foundations, Induction, and Coinduction
TutorialFest
Andrei Popescu
University of Sheffield
,
Dmitriy Traytel
University of Copenhagen
11:00 - 12:30
Tutorials 2B
TutorialFest
at
Park
11:00
90m
Tutorial
Isabelle/HOL: Foundations, Induction, and Coinduction
TutorialFest
Andrei Popescu
University of Sheffield
,
Dmitriy Traytel
University of Copenhagen
14:00 - 15:30
Tutorials 6A
TutorialFest
at
Park
14:00
90m
Tutorial
Using a Proof Assistant to Teach PL Theory, Without the Overhead
TutorialFest
Jonathan Aldrich
Carnegie Mellon University
,
John Boyland
Univeristy of Wisconsin, Milwaukee
16:00 - 17:30
Tutorials 6B
TutorialFest
at
Park
16:00
90m
Tutorial
Using a Proof Assistant to Teach PL Theory, Without the Overhead
TutorialFest
Jonathan Aldrich
Carnegie Mellon University
,
John Boyland
Univeristy of Wisconsin, Milwaukee
Sat 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:30
Session 1
PriSC
at
Park
Chair(s):
Marco Guarnieri
IMDEA Software Institute
09:00
5m
Day opening
Introduction
PriSC
09:05
60m
Keynote
Semantic Intermediate Representations for Sound Language Interoperability
PriSC
Amal Ahmed
Northeastern University, USA
Pre-print
10:05
25m
Talk
Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers
PriSC
Farzaneh Derakhshan
Carnegie Mellon University
,
Zichao Zhang
Carnegie Mellon University
,
Amit Vasudevan
Carnegie Mellon University
,
Limin Jia
Carnegie Mellon University
File Attached
11:00 - 12:30
Session 2
PriSC
at
Park
Chair(s):
Cătălin Hriţcu
MPI-SP
11:00
25m
Talk
Automated Learning and Verification of Embedded Security Architectures
PriSC
Matteo Busi
University Ca' Foscari, Venice
,
Riccardo Focardi
University Ca' Foscari, Venice
,
Flaminia L. Luccio
University Ca' Foscari, Venice
File Attached
11:25
25m
Talk
pi_RA: A pi-calculus for verifying protocols that use remote attestation
PriSC
Emiel Lanckriet
KU Leuven
,
Matteo Busi
University Ca' Foscari, Venice
,
Dominique Devriese
KU Leuven
File Attached
11:50
25m
Talk
Robust Constant-Time Cryptography
PriSC
Matthew Kolosick
University of California at San Diego
,
Basavesh Ammanaghatta Shivakumar
Max Planck Institute for Security and Privacy (MPI-SP)
,
Sunjay Cauligi
University of California at San Diego, USA
,
Marco Patrignani
University of Trento
,
Marco Vassena
Utrecht University
,
Ranjit Jhala
University of California at San Diego
,
Deian Stefan
University of California at San Diego
Pre-print
12:15
15m
Talk
Short Talk: Generalising secure compilation criteria
PriSC
Emiel Lanckriet
KU Leuven
14:00 - 15:30
Session 3
PriSC
at
Park
Chair(s):
Sébastien Bardin
CEA LIST, University Paris-Saclay
14:00
25m
Talk
Blame-Preserving Secure Compilation
PriSC
Marco Patrignani
University of Trento
,
Matthis Kruse
CISPA Helmholtz Center for Information Security
Pre-print
14:25
25m
Talk
Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces
Recorded
PriSC
Cezar-Constantin Andrici
MPI-SP
,
Cătălin Hriţcu
MPI-SP
,
Théo Winterhalter
INRIA Saclay
Pre-print
File Attached
14:50
25m
Talk
SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
PriSC
Jérémy Thibault
MPI-SP
,
Arthur Azevedo de Amorim
Boston University
,
Roberto Blanco
MPI-SP
,
Aina Linn Georges
Aarhus University
,
Cătălin Hriţcu
MPI-SP
,
Andrew Tolmach
Portland State University
Pre-print
Media Attached
File Attached
16:00 - 17:30
Session 4
PriSC
at
Park
Chair(s):
Matteo Busi
University Ca' Foscari, Venice
16:00
25m
Talk
Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
PriSC
Michael Smith
UC San Diego
,
Abhishek Sharma
UC San Diego
,
John Renner
University of California at San Diego, USA
,
David Thien
UC San Diego
,
Sorin Lerner
University of California at San Diego
,
Fraser Brown
CMU
,
Hovav Shacham
University of Texas at Austin
,
Deian Stefan
University of California at San Diego
File Attached
16:25
25m
Talk
FaJITa: Verifying Optimizations on Just-In-Time Programs
PriSC
David Thien
UC San Diego
,
Michael Smith
UC San Diego
,
Evan Johnson
University of California at San Diego; Arm
,
Sorin Lerner
University of California at San Diego
,
Hovav Shacham
University of Texas at Austin
,
Deian Stefan
University of California at San Diego
,
Fraser Brown
CMU
Pre-print
File Attached
16:50
25m
Talk
Universally Composable Security for Program Partitioning
PriSC
Coşku Acay
Cornell University
,
Joshua Gancher
Carnegie Mellon University
,
Rolph Recto
Cornell University
,
Andrew Myers
Cornell University
File Attached
Mon 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
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
Park
TutorialFest
Tutorials 2A
TutorialFest
TutorialFest
Tutorials 2B
TutorialFest
TutorialFest
Tutorials 6A
TutorialFest
TutorialFest
Tutorials 6B
Sat 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
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
Park
PriSC
Session 1
PriSC
Session 2
PriSC
Session 3
PriSC
Session 4
Mon 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
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
Park
POPL TutorialFest
Isabelle/HOL: Foundations, Induction, and Coinduction
09:00 - 10:30
POPL TutorialFest
Isabelle/HOL: Foundations, Induction, and Coinduction
11:00 - 12:30
POPL TutorialFest
Using a Proof Assistant to Teach PL Theory, Without the Overhead
14:00 - 15:30
POPL TutorialFest
Using a Proof Assistant to Teach PL Theory, Without the Overhead
16:00 - 17:30
Sat 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
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
Park
PriSC
Introduction
09:00 - 09:05
PriSC
Semantic Intermediate Representations for Sound Language Interoperability
09:05 - 10:05
PriSC
Towards End-to-End Verified TEEs via Verified Interface Conformance and ...
10:05 - 10:30
PriSC
Automated Learning and Verification of Embedded Security Architectures
11:00 - 11:25
PriSC
pi_RA: A pi-calculus for verifying protocols that use remote attestation
11:25 - 11:50
PriSC
Robust Constant-Time Cryptography
11:50 - 12:15
PriSC
Short Talk: Generalising secure compilation criteria
12:15 - 12:30
PriSC
Blame-Preserving Secure Compilation
14:00 - 14:25
PriSC
Recorded
Securely Compiling F* Programs With IO and Then Linking Them Against We ...
14:25 - 14:50
PriSC
SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capa ...
14:50 - 15:15
PriSC
Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
16:00 - 16:25
PriSC
FaJITa: Verifying Optimizations on Just-In-Time Programs
16:25 - 16:50
PriSC
Universally Composable Security for Program Partitioning
16:50 - 17:15
x
Sat 21 Dec 15:44