caa a22 4500 463182812 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070701xx s 000 0 eng 10.1007/s10817-006-9061-y doi (NATIONALLICENCE)springer-10.1007/s10817-006-9061-y Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts [Elektronische Daten] [Alberto Ciaffaglione, Luigi Liquori, Marino Miculan] 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 us 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 deduction theorems, which are proved formally in the proof assistant Coq with a relatively small overhead. Springer Science+Business Media, Inc., 2007 Functional and imperative object-calculi nationallicence Logical foundations of programming nationallicence Coinductive type theories nationallicence Logical frameworks nationallicence Interactive theorem proving nationallicence Ciaffaglione Alberto Dipartimento di Matematica e Informatica, Università di Udine, via delle Scienze, 206-33100, Udine, Italy aut Liquori Luigi INRIA, Sophia Antipolis, France aut Miculan Marino Dipartimento di Matematica e Informatica, Università di Udine, via delle Scienze, 206-33100, Udine, Italy aut Journal of Automated Reasoning Kluwer Academic Publishers 39/1(2007-07-01), 1-47 0168-7433 39:1<1 2007 39 10817 https://doi.org/10.1007/s10817-006-9061-y text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9061-y text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Ciaffaglione Alberto Dipartimento di Matematica e Informatica, Università di Udine, via delle Scienze, 206-33100, Udine, Italy aut NATIONALLICENCE 700 1- Liquori Luigi INRIA, Sophia Antipolis, France aut NATIONALLICENCE 700 1- Miculan Marino Dipartimento di Matematica e Informatica, Università di Udine, via delle Scienze, 206-33100, Udine, Italy aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 39/1(2007-07-01), 1-47 0168-7433 39:1<1 2007 39 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer