Abstract | ||
---|---|---|
We illustrate the benefits of using Natural Deduction in combination with weak Higher-Order Abstract Syntax for formalizing an object-based calculus with objects, cloning, method-update, types with subtyping, and side-effects, in inductive type theories such as the Calculus 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 the Theory of Contexts, we can prove formally the Subject Reduction Theorem in the proof assistant Coq, with a relatively small overhead. |
Year | DOI | Venue |
---|---|---|
2003 | 10.1145/976571.976574 | MERLIN |
Keywords | Field | DocType |
imperative object-based calculus,inductive type theory,object-based calculus,higher order abstract syntax,method closure,inductive constructions,proof assistant coq,efficient management,compact formalization,small overhead,subject reduction theorem,natural deduction,interactive theorem proving,logical framework,side effect,proof assistant,theory,languages,type theory | Inductive type,Programming language,Subject reduction,Computer science,Natural deduction,Abstract syntax,Higher-order abstract syntax,Syntax,Semantics,Calculus,Proof assistant | Conference |
ISBN | Citations | PageRank |
1-58113-800-8 | 4 | 0.42 |
References | Authors | |
14 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Alberto Ciaffaglione | 1 | 58 | 9.97 |
Luigi Liquori | 2 | 398 | 38.85 |
Marino Miculan | 3 | 502 | 43.24 |