Mechanizing the Construction and Rewriting of Proper Functions in Coq
The notion of monotonic, or order-preserving, functions is a key notion in programming languages semantics, being used in both logical relations and denotational semantics. In Coq, monotonic functions are also known as Proper functions, because they are usually defined with the Proper typeclass, and they are used for setoid rewriting. Although it is straightforward to define a Coq type for Proper functions, it is onerous and time-consuming to build any non-trivial Proper functions in this type, as the user has to manually write the proofs of monotonicity at every Proper abstraction. Further, rewriting these Proper functions requires rewriting their proofs as well, which can increase the size of expressions dramatically with each rewrite step.
In this talk, ongoing work will be presented that addresses both of these problems. To build Proper functions, a collection of Coq typeclass instances and notations are used to automatically build monotonicity proofs, effectively creating an embedded domain-specific language (EDSL) of Proper functions inside Coq. To rewrite Proper functions, they are first reflected into a Coq inductive datatype that represents Proper functions without requiring monotonicity proofs. This reflection is performed using a second collection of Coq typeclass instances. Because this inductive datatype does not require monotonicity proofs, rewriting becomes orders of magnitude more efficient.
(westbrook-coqpl-2018.pdf) | 327KiB |
(Westbrook-CoqPL18-Slides.pdf) | 3.95MiB |
Sat 13 Jan Times are displayed in time zone: Tijuana, Baja California change
16:00 - 18:05: Semantics and SynthesisCoqPL at Watercourt A Chair(s): Ilya SergeyUniversity College London | |||
16:00 - 16:25 Talk | Phantom Types for Quantum Programs CoqPL Robert RandUniversity of Pennsylvania, Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania File Attached | ||
16:25 - 16:50 Talk | Revisiting Parametricity: Inductives and Uniformity of Propositions CoqPL File Attached | ||
16:50 - 17:15 Talk | Towards Context-Aware Data Refinement CoqPL File Attached | ||
17:15 - 17:40 Talk | Mechanizing the Construction and Rewriting of Proper Functions in Coq CoqPL Edwin WestbrookGalois, Inc. File Attached | ||
17:40 - 18:05 Talk | A calculus for logical refinements in separation logic CoqPL File Attached |