Towards a Formalization of Nominal Sets in Coq
summary
Formalization of nominal sets in Coq 8.14 implements list-of-swaps permutations and a type-class hierarchy for groups and actions, proving support, freshness and basic nominal properties but leaving nominal functions and name-abstractions as work in progress. Permutations compute inverses by list reverse; representation is non‑unique so a manual unique support must be supplied and verified. Setoid/offsetoid machinery and functional extensionality issues force some workarounds; merging classes fixes many rewrite failures but rewriting tactics remain brittle. Automation and plugin (Mtac2, Elpi) options are being explored.
AI-written summary · about
chapters (18)
- 0:00Intro
- 2:18Name Permutation
- 3:45Support
- 5:05Nominal Set
- 5:36Nominal Tools
- 6:03Implementation Issues
- 7:47Implement Implementation
- 8:11Defining Representation
- 8:42Blended Approach
- 9:11Equivalence Representation
- 9:55Group Action
- 10:07Permutation
- 11:02Nominal Type
- 11:38Freshness
- 13:49Proofs
- 14:42Conclusion
- 16:31Future
- 17:38Questions
related talks
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
19mExtensible Metatheory Mechanization via Family Polymorphism
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
25mLocally Nameless Sets
30mNominal Matching Logic With Fixpoints
21mSyntax with Shifted Names