1 paper
Matthew Gates, Alex Potanin
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 wit…