A Coq implementation of a Theory of Tagged Objects

TL;DR

This work introduces a Coq encoding of the Theory of Tagged Objects ($ToTO$), focusing on encoding its tag-based type system and dynamic semantics. It presents the syntax, subtyping, substitution, typing, and dynamics in Coq, and outlines Preservation and Progress as type-soundness goals (to be mechanized). The contribution provides a mechanized foundation for reasoning about tagged objects and dynamic class hierarchies, and discusses limitations and future directions such as proofs, translations to the core language, and extending tagging to multiple inheritance.

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.

Figures (7)

• Figure 1: Theory of Tagged objects type encoding
• Figure 2: Subtyping Rules
• Figure 3: Type Judgements
• Figure 4: Store Definitions
• Figure 5: Reduction rules