Infinitary Refinement Types for Temporal Properties in Scott Domains
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_ | 1866910960880451584 |
|---|---|
| author | Riba, Colin Kejikian, Alexandre |
| author_facet | Riba, Colin Kejikian, Alexandre |
| contents | We discuss an infinitary refinement type system for input-output temporal specifications of functions that handle infinite objects like streams or infinite trees. Our system is based on a reformulation of Bonsangue and Kok's infinitary extension of Abramsky's Domain Theory in Logical Form to saturated properties. We show that in an interesting range of cases, our system is complete without the need of an infinitary rule introduced by Bonsangue and Kok to reflect the well-filteredness of Scott domains. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_11917 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Infinitary Refinement Types for Temporal Properties in Scott Domains Riba, Colin Kejikian, Alexandre Logic in Computer Science F.3.1; F.3.2; F.4.1 We discuss an infinitary refinement type system for input-output temporal specifications of functions that handle infinite objects like streams or infinite trees. Our system is based on a reformulation of Bonsangue and Kok's infinitary extension of Abramsky's Domain Theory in Logical Form to saturated properties. We show that in an interesting range of cases, our system is complete without the need of an infinitary rule introduced by Bonsangue and Kok to reflect the well-filteredness of Scott domains. |
| title | Infinitary Refinement Types for Temporal Properties in Scott Domains |
| topic | Logic in Computer Science F.3.1; F.3.2; F.4.1 |
| url | https://arxiv.org/abs/2502.11917 |