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.
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
16:00 - 18:05
|Phantom Types for Quantum Programs|
Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of PennsylvaniaFile Attached
|Revisiting Parametricity: Inductives and Uniformity of Propositions|
|Towards Context-Aware Data Refinement|
Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue UniversityFile Attached
|Mechanizing the Construction and Rewriting of Proper Functions in Coq|
Edwin Westbrook Galois, Inc.File Attached
|A calculus for logical refinements in separation logic|