Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021
Online
Toggle navigation
Attending
Venue: Online (How to POPL in 2021)
Supporting POPL
Student Volunteers
Code of Conduct
Registration
FAQ
Program
POPL Program
Your Program
Sun 17 Jan
Mon 18 Jan
Tue 19 Jan
Wed 20 Jan
Thu 21 Jan
Fri 22 Jan
Tracks
POPL 2021
POPL
Artifact Evaluation
Workshops and Co-located Events
TutorialFest
Student Research Competition
Student Volunteers
POPL Meetups
Co-hosted Conferences
CPP
CPP
CPP
Lightning Talks
PLMW
VMCAI
Workshops
CoqPL
LAFI
PEPM
PriSC
Co-hosted Symposia
PADL
Organization
POPL 2021 Committees
Organizing Committee
Track Committees
POPL
Artifact Evaluation
TutorialFest
Student Research Competition
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Organization Committee
Program Committee
Steering Committee
PLMW
Invited Speakers
Panelists
Organizing Committee
VMCAI
Invited Speakers
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Invited speaker
Organizing Committee
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PriSC
Program Committee
Steering Committee
Co-hosted Symposia
PADL
Programme Chairs
Programme 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 2021
(
series
) /
Online (How to POPL in 2021)
/
Room information: CoqPL
Venue
Online (How to POPL in 2021)
Room name
CoqPL
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+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
.
Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
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-07: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+02: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
Tue 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
14:30 - 15:30
Invited Talk
CoqPL
at
CoqPL
14:30
60m
Keynote
Verifying a compiler through equational means
CoqPL
Yannick Zakowski
Inria
16:00 - 17:30
Contributed Talks
CoqPL
at
CoqPL
16:00
15m
Talk
A Limited Case for Reification by Type Inference
CoqPL
Jason Gross
MIT CSAIL
Media Attached
File Attached
16:15
15m
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui Qi
Nagoya University
,
Jacques Garrigue
Nagoya University
File Attached
16:30
15m
Talk
Record Updates in Coq
CoqPL
Tej Chajed
Massachusetts Institute of Technology, USA
Media Attached
File Attached
16:45
15m
Break
Break
CoqPL
17:00
15m
Talk
The B+-tree Index as a Verified Software Unit
CoqPL
Anastasiya Kravchuk-Kirilyuk
Harvard University
,
Andrew W. Appel
Princeton
,
Lennart Beringer
Princeton University
File Attached
17:15
15m
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul Chiplunkar
Massachusetts Institute of Technology
,
Clément Pit-Claudel
Massachusetts Institute of Technology, USA
,
Adam Chlipala
Massachusetts Institute of Technology
File Attached
18:00 - 18:45
Contributed Talks
CoqPL
at
CoqPL
18:00
15m
Talk
Verification of Algorithm and Code Generation for Signal Transforms
CoqPL
Patrick Brinich
Drexel University
,
Jeremy Johnson
Drexel University, USA
File Attached
18:15
15m
Talk
An experience report on writing usable DSLs in Coq
CoqPL
Clément Pit-Claudel
Massachusetts Institute of Technology, USA
,
Thomas Bourgeat
MIT CSAIL
File Attached
18:30
15m
Break
Break
CoqPL
18:45 - 19:30
Session with the Coq Development Team
CoqPL
at
CoqPL
18:45
45m
Demonstration
Session with the Coq Development Team
CoqPL
P:
Matthieu Sozeau
Inria
,
P:
Enrico Tassi
INRIA
Tue 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
CoqPL
CoqPL
Invited Talk
CoqPL
Contributed Talks
CoqPL
Contributed Talks
CoqPL
Session with the Coq Development Team
Tue 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
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
19:00
15
30
45
CoqPL
CoqPL
Verifying a compiler through equational means
14:30 - 15:30
CoqPL
A Limited Case for Reification by Type Inference
16:00 - 16:15
CoqPL
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
16:15 - 16:30
CoqPL
Record Updates in Coq
16:30 - 16:45
CoqPL
Break
16:45 - 17:00
CoqPL
The B+-tree Index as a Verified Software Unit
17:00 - 17:15
CoqPL
Automated Synthesis of Verified Firewalls
17:15 - 17:30
CoqPL
Verification of Algorithm and Code Generation for Signal Transforms
18:00 - 18:15
CoqPL
An experience report on writing usable DSLs in Coq
18:15 - 18:30
CoqPL
Break
18:30 - 18:45
CoqPL
Session with the Coq Development Team
18:45 - 19:30
x
Thu 21 Nov 09:35