A Coq Library of Sets for Teaching Denotational Semantics
Qinxiang Cao, Xiwei Wu, Yalun Liang
TL;DR
This work tackles the readability gap in Coq-based denotational semantics by introducing a teaching-oriented library that treats any $T = A -> B -> ... -> Prop$ as a set and unifies set operators, membership, and relation composition via Coq type classes. It provides core definitions (Sets.equiv, Sets.included, Sets.union, Sets.general_union, etc.), an intuitive membership interface (In), and a unified composition framework (Rels.concat) along with a zero-cost unfolding tactic (Sets_unfold). The library includes extensive lemmas (61 key results) and practical tactic support to enable readable, automated proofs suitable for teaching and for professional use, with validation in multiple undergraduate programming language theory courses. Overall, it lowers the barrier to using Coq for denotational semantics in classrooms while preserving compatibility with standard libraries and enabling scalable, readable formalizations.
Abstract
Sets and relations are very useful concepts for defining denotational semantics. In the Coq proof assistant, curried functions to Prop are used to represent sets and relations, e.g. A -> Prop, A -> B -> Prop, A -> B -> C -> Prop, etc. Further, the membership relation can be encoded by function applications, e.g. X a represents a in X if X: A -> Prop. This is very convenient for developing formal definitions and proofs for professional users, but it makes propositions more difficult to read for non-professional users, e.g. students of a program semantics course. We develop a small Coq library of sets and relations so that standard math notations can be used when teaching denotational semantics of simple imperative languages. This library is developed using Coq's type class system. It brings about zero proof-term overhead comparing with the existing formalization of sets.