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

Proof by reflection is a common and well-studied automation tool. Reification—generally written using Ltac, OCaml, typeclasses, or canonical structures—is the means by which a structured representation is derived from an unstructured representation. The reflective automation then operates on the structured representation, relying on an interpretation or denotation function to justify a correspondence between the structured and unstructured representations.

A couple of years ago, I presented a trick for blazing fast reification in two lines of Ltac—using the pattern tactic—which I termed reification by parametricity. While I still advocate for parametricity as the preferred method of domain-specific reification, I would like to present here yet another method.

While reification typically requires meta-programming features, I was surprised and delighted to discover that, in some restricted cases, reification can be performed entirely by a combination of the notation system and type inference. In some sense, this is trivial: by redefining the basic syntactic notations, a term can be “reified” merely by writing the same symbols in another scope. In another sense, though, this trick is quite surprising: we use the notation system merely to insert “reify here” functions at every atom, and the reification itself is in fact performed by type inference. My hope is that the audience will walk away with this new trick in their toolbox, and that some day some problem will come along demanding a slight generalization of this trick, and that generalization will be new and interesting in its own right. This, after all, is how reification by parametricity was discovered.

I propose to present the one example I have for this trick: reifying the type structure of a function in a way that allows manipulations of the arguments, such as uncurrying, reassociation of the uncurried structure, and reordering. I will present the simple code for this example in detail. My goal will be that the audience understand completely how it works, why it works, and how it might be used elsewhere.

Abstract (coqpl21-final1.pdf)90KiB
reification_by_type_inference_presentation.v (reification_by_type_inference_presentation.v)5KiB

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