A Coq implementation of a Theory of Tagged Objects

Date

Authors

Gates, Matthew
Potanin, Alex

Journal Title

Journal ISSN

Volume Title

Publisher

Access Statement

Research Projects

Organizational Units

Journal Issue

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.

Description

Keywords

Citation

Source

CoRR

Book Title

Entity type

Publication

Access Statement

License Rights

Restricted until