Skip to main navigation Skip to search Skip to main content

A Coq implementation of a Theory of Tagged Objects

Research output: Contribution to journalArticle

Abstract

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.
Original languageEnglish
Article numberabs/2502.11344
Number of pages30
JournalCoRR
DOIs
Publication statusPublished - Feb 2025

Cite this