A Coq implementation of a Theory of Tagged Objects
arXiv:2502.11344
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.