By Alberto Ciaffaglione, Luigi Liquori and Marino Miculan, from MERLIN 2003, available from Luigi Liquori’s website:

We illustrate the benefits of using

Natural Deductionin combination withweak Higher-Order Abstract Syntaxfor formalizing an object-based calculus with objects, cloning, method-update, types with subtyping, and side-effects, in inductive type theories such as theCalculus of Inductive Constructions. This setting suggests a clean and compact formalization of the syntax and semantics of the calculus, with an efficient management of method closures. Using our formalization and theTheory of Contexts, we can prove formally the Subject Reduction Theorem in the proof assistant Coq, with a relatively small overhead.