Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 17:15 - 17:30 at CoqPL - Contributed Talks

We demonstrate correct-by-construction firewalls—stateful packet filters for TCP/IP packets—using the Fiat synthesis library [3]. We present a general DSL for specifying their behavior independent of algorithmic implementation. We outline the design of a verified compiler in Coq, detail a few verified efficiency optimizations, and show how the compiler can easily be extended to support custom optimizations for user-defined policies.

Abstract (coqpl21-final7.pdf)344KiB

Tue 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Contributed TalksCoqPL 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 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