A Coq implementation of a Theory of Tagged Objects
Matthew Gates, Alex Potanin · arXiv (Cornell University) · 2025
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.