LAFI 2021
Sun 17 - Fri 22 January 2021
Online
co-located with
POPL 2021
Toggle navigation
Attending
Venue: Online (How to POPL in 2021)
Program
Complete Program
Your Program
Sun 17 Jan
Mon 18 Jan
Tue 19 Jan
Wed 20 Jan
Thu 21 Jan
Fri 22 Jan
Track/Call
Organization
LAFI 2021 Committees
Track Committees
Organizing Committee
Program Committee
Steering Committee
Contributors
People Index
Search
Series
Series
LAFI 2024
LAFI 2023
LAFI 2022
LAFI 2021
LAFI 2020
LAFI 2019
PPS 2018
PPS 2017
PPS 2016
Sign in
Sign up
POPL 2021
(
series
) /
LAFI 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
Wed 24 Apr 13:58