Skip to Main content Skip to Navigation
Journal articles

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

Alberto Ciaffaglione 1 Luigi Liquori 2 Marino Miculan 1
2 MASCOTTE - Algorithms, simulation, combinatorics and optimization for telecommunications
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
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 combination with 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.
Complete list of metadata

Cited literature [56 references]  Display  Hide  Download
Contributor : Luigi Liquori Connect in order to contact the contributor
Submitted on : Wednesday, May 13, 2015 - 1:16:32 PM
Last modification on : Thursday, January 20, 2022 - 5:32:14 PM
Long-term archiving on: : Wednesday, April 19, 2017 - 2:42:26 PM


Files produced by the author(s)




Alberto Ciaffaglione, Luigi Liquori, Marino Miculan. Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. Journal of Automated Reasoning, Springer Verlag, 2007, Journal of Automated Reasoning, 39 (1), pp.1-47. ⟨10.1007/s10817-006-9061-y⟩. ⟨hal-01148347⟩



Les métriques sont temporairement indisponibles