A Coq implementation of a Theory of Tagged Objects
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909496541970432 |
|---|---|
| author | Gates, Matthew Potanin, Alex |
| author_facet | Gates, Matthew Potanin, Alex |
| contents | We present a first step towards the Coq implementation of the Theory of Tagged Objects formalism. The concept of tagged types is encoded, and the soundness proofs are discussed with some future work suggestions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_11344 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Coq implementation of a Theory of Tagged Objects Gates, Matthew Potanin, Alex Programming Languages We present a first step towards the Coq implementation of the Theory of Tagged Objects formalism. The concept of tagged types is encoded, and the soundness proofs are discussed with some future work suggestions. |
| title | A Coq implementation of a Theory of Tagged Objects |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2502.11344 |