Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
VenueOnline (How to POPL in 2021)
Room nameCoqPL
Additional informationThere is no additional information of this room available.
Program

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:30 - 15:30: Invited TalkCoqPL at CoqPL
14:30 - 15:30
Keynote
Verifying a compiler through equational means
CoqPL
16:00 - 17:30: Contributed TalksCoqPL at CoqPL
16:00 - 16:15
Talk
A Limited Case for Reification by Type Inference
CoqPL
Jason GrossMIT CSAIL
Media Attached File Attached
16:15 - 16:30
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui QiNagoya University, Jacques GarrigueNagoya University
File Attached
16:30 - 16:45
Talk
Record Updates in Coq
CoqPL
Tej ChajedMassachusetts Institute of Technology, USA
Media Attached File Attached
16:45 - 17:00
Break
Break
CoqPL
17:00 - 17:15
Talk
The B+-tree Index as a Verified Software Unit
CoqPL
Anastasiya Kravchuk-KirilyukHarvard University, Andrew AppelPrinceton, Lennart BeringerPrinceton University
File Attached
17:15 - 17:30
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul ChiplunkarMassachusetts Institute of Technology, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology
File Attached
18:00 - 18:45: Contributed TalksCoqPL at CoqPL
18:00 - 18:15
Talk
Verification of Algorithm and Code Generation for Signal Transforms
CoqPL
Patrick BrinichDrexel University, Jeremy JohnsonDrexel University, USA
File Attached
18:15 - 18:30
Talk
An experience report on writing usable DSLs in Coq
CoqPL
Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Thomas BourgeatMIT CSAIL
File Attached
18:30 - 18:45
Break
Break
CoqPL
18:45 - 19:30: Session with the Coq Development TeamCoqPL at CoqPL
18:45 - 19:30
Demonstration
Session with the Coq Development Team
CoqPL
P: Matthieu SozeauInria, P: Enrico TassiINRIA

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change