Dependently Sorted Nominal Signatures
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_ | 1866908591898755072 |
|---|---|
| author | Fernández, Maribel Pagano, Miguel Szasz, Nora Tasistro, Álvaro |
| author_facet | Fernández, Maribel Pagano, Miguel Szasz, Nora Tasistro, Álvaro |
| contents | We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to lambda-calculi). Expressions are then classified using a system of sorts and sort families that respects alpha-conversion (similarly to dependently-typed lambda-calculi) but not allowing names to carry abstraction sorts, thus constituting a first-order dependent sort system. The system can represent forms of judgement and rules of inference of several interesting calculi. We present rules and properties of the system as well as experiments of representation, and discuss how it constitutes a basis on which to build a type theory where raw expressions with alpha-equivalence are given a completely formal treatment. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_12305 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Dependently Sorted Nominal Signatures Fernández, Maribel Pagano, Miguel Szasz, Nora Tasistro, Álvaro Logic in Computer Science F.4.1 We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to lambda-calculi). Expressions are then classified using a system of sorts and sort families that respects alpha-conversion (similarly to dependently-typed lambda-calculi) but not allowing names to carry abstraction sorts, thus constituting a first-order dependent sort system. The system can represent forms of judgement and rules of inference of several interesting calculi. We present rules and properties of the system as well as experiments of representation, and discuss how it constitutes a basis on which to build a type theory where raw expressions with alpha-equivalence are given a completely formal treatment. |
| title | Dependently Sorted Nominal Signatures |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2510.12305 |