Nominal Sets in Rocq
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914067514392576 |
|---|---|
| author | Paranhos, Fabrício Sanches Ventura, Daniel |
| author_facet | Paranhos, Fabrício Sanches Ventura, Daniel |
| contents | Nominal techniques have been praised for their ability to formalize grammars with binding structures closer to their informal developments. At its core, there lies the definition of nominal sets, which capture the notion of name (in)dependence through a simple, and uniform, metatheory based on name permutations. We present a formal constructive development of nominal sets in Rocq (formerly known as Coq), with its main design and project decisions. Furthermore, we formalize the concepts of freshness, nominal alpha-equivalence, name abstraction, and finitely supported functions. Our implementation relies on a type class hierarchy which, combined with Rocq generalized rewriting mechanism, achieves concise definitions and proofs, whilst easing the well-known "setoid hell" scenario. We conclude with a discussion on how to obtain the constructive alpha-structural recursion and induction combinators, towards a nominal framework. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_25883 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Nominal Sets in Rocq Paranhos, Fabrício Sanches Ventura, Daniel Logic in Computer Science F.3; F.4 Nominal techniques have been praised for their ability to formalize grammars with binding structures closer to their informal developments. At its core, there lies the definition of nominal sets, which capture the notion of name (in)dependence through a simple, and uniform, metatheory based on name permutations. We present a formal constructive development of nominal sets in Rocq (formerly known as Coq), with its main design and project decisions. Furthermore, we formalize the concepts of freshness, nominal alpha-equivalence, name abstraction, and finitely supported functions. Our implementation relies on a type class hierarchy which, combined with Rocq generalized rewriting mechanism, achieves concise definitions and proofs, whilst easing the well-known "setoid hell" scenario. We conclude with a discussion on how to obtain the constructive alpha-structural recursion and induction combinators, towards a nominal framework. |
| title | Nominal Sets in Rocq |
| topic | Logic in Computer Science F.3; F.4 |
| url | https://arxiv.org/abs/2509.25883 |