Sciweavers

JAR
2007

Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts

13 years 10 months ago
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts
Abstract. We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive Constructions, by taking advantage of Natural Deduction Semantics and coinduction in comwith weak Higher-Order Abstract Syntax and the Theory of Contexts. Our methodology allows to implement smoothly the calculi in the target metalanguage; moreover, it suggests novel presentations of the calculi themselves. In detail, we present a compact formalization of the syntax and semantics for the functional and the imperative variants of the ς-calculus. Our approach simplifies the proof of Subject Reduction theorems, which are proved formally in the proof assistant Coq with a relatively small overhead.
Alberto Ciaffaglione, Luigi Liquori, Marino Micula
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where JAR
Authors Alberto Ciaffaglione, Luigi Liquori, Marino Miculan
Comments (0)