I. Resaux, Lab * TType)))) | t_step: (S:SType;A,B,C:TType;v:Res;i:Loc;l:Lab) (pl:(list (Lab * TType))) (type_from_lab A l), resaux S A v B)->(list_from_type B)=pl-> ... (resaux S A (cons (l,i) v) (mk (cons (l,C) pl))

I. Type_b, SType;b:Term;A:TType) (type b A)->(type_b S (ground b) A) | t_bind: (S:SType;b:Var->Body;A,B:TType;v:Res) (res S v A), x:Var)(typenv x A)->(type_b S (b x) B))-> (type_b S (bind v b) B)

F. Of, . Coinductive, and . Typing, The judgements cores and cotype b of Subsection 3.4 are rendered by means of two mutually defined coinductive predicates (although cotype b is intrinsically inductive). The encoding of the rules of Figure 14 needs an auxiliary coinductive judgement (coaux), similarly to the treatment of res above

C. Coaux, TType;s:Store;pl:(list(Lab * TType))) (v:Res;i:Loc;c:Cls;l:Lab) (store_nth i s)=(c)-> ((x:Var)(typenv x C)->(cotype_b s (c x) B))-> (coaux C s v A)->(list_from_type A)=pl->...-> (coaux C s (cons (l,i) v) (mk (cons (l,B) pl))) with cotype_b: Store->Body->TType->Prop:= t_coground: (s:Store;b:Term;A:TType) (type b A)->(cotype_b s (ground b) A) | t_cobind: (s:Store;b:Var->Body, :TType;v:Res) ((x:Var)(typenv x A)->(cotype_b s (b x) B))-> (coaux A s v A)->(cotype_b s (bind v b) B)

M. Abadi and L. Cardelli, A theory of objects, 1996.
DOI : 10.1007/978-1-4419-8598-9

Y. Bertot, A certified compiler for an imperative language, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00073199

A. Bucalo, M. Hofmann, F. Honsell, M. Miculan, and I. Scagnetto, Consistency of the theory of contexts, Journal of Functional Programming, vol.16, issue.03, pp.327-395, 2006.
DOI : 10.1017/S0956796806005892

R. Burstall and F. Honsell, Operational semantics in a natural deduction setting Logical Frameworks, pp.185-214, 1990.

L. Cardelli, Obliq: A Language with Distributed Scope, Computing Systems, vol.8, issue.1, pp.27-59, 1995.

I. Cervesato and F. Pfenning, A Linear Logical Framework, Information and Computation, vol.179, issue.1, pp.19-75, 2002.
DOI : 10.1006/inco.2001.2951
URL : http://doi.org/10.1006/inco.2001.2951

J. L. Chirimar, Proof Theoretic Approach to Specification Languages, 1995.

A. Ciaffaglione, Certified reasoning on Real Numbers and Objects in Co-inductive Type Theory, Dipartimento di Matematica e Informatica, 2003.

A. Ciaffaglione, L. Liquori, and M. Miculan, Imperative Object-Based Calculi in Co-inductive Type Theories, Proc. of LPAR of Lecture Notes in Computer Science, 2003.
DOI : 10.1007/978-3-540-39813-4_4
URL : https://hal.archives-ouvertes.fr/hal-01149867

A. Ciaffaglione, L. Liquori, and M. Miculanhonsell, Reasoning on an Imperative objectcalculus in Higher-Order Abstract Syntax, 2003.

A. Ciaffaglione, L. Liquori, and M. Miculan, The Web Appendix of this paper, 2003.

A. Ciaffaglione and I. Scagnetto, Plug and Play the Theory of Contexts in Higher-Order Abstract Syntax, Proceedings of CoMeta, 2003.
DOI : 10.1016/j.entcs.2004.09.022

. Coq, The Coq Proof Assistant 7.3'. INRIA, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00069919

R. L. Crole, Lectures on, 1998.

J. Despeyroux, Proof of Translation in Natural Semantics, Proc. of LICS, pp.193-205, 1986.
URL : https://hal.archives-ouvertes.fr/inria-00076040

J. Despeyroux, A. Felty, and A. Hirschowitz, Higher-order syntax in Coq, Proc. of TLCA, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00074124

J. Despeyroux and P. Leleu, Recursion over objects of functional type, Mathematical Structures in Computer Science, vol.11, issue.04, pp.555-572, 2001.
DOI : 10.1017/S0960129501003346

A. P. Felty, Two-Level Meta-reasoning in Coq, Proc. TPHOLs of Lecture Notes in Computer Science, pp.198-213, 2002.
DOI : 10.1007/3-540-45685-6_14

M. P. Fiore, G. D. Plotkin, and D. Turi, Abstract syntax and variable binding, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.193-202, 1999.
DOI : 10.1109/LICS.1999.782615

K. Fisher, F. Honsell, and J. Mitchell, A lambda calculus of objects and method specialization, Nordic Journal of Computing, 1994.

J. Frost, A Case Study of Co-induction in Isabelle, 1993.

M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing, vol.13, issue.3-5, pp.341-363, 2002.
DOI : 10.1007/s001650200016

G. Gillard, A formalization of a concurrent object calculus up to alpha-conversion, Proc. of CADE, 2000.

E. Giménez, Codifying guarded definitions with recursive schemes, Proc. of TYPES, pp.39-59, 1995.
DOI : 10.1007/3-540-60579-7_3

R. Harper, F. Honsell, and G. , Plotkin: 1993, 'A framework for defining logics, Journal of ACM, vol.40, issue.1

M. Hofmann, Semantical analysis of higher-order abstract syntax, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.204-213, 1999.
DOI : 10.1109/LICS.1999.782616

M. Hofmann and F. Tang, Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover, Proc. of TPHOLs, pp.268-282, 2000.
DOI : 10.1007/3-540-44659-1_17

M. Hofmann and F. Tang, A Higher-Order Embedding of a Logic of Objects, 2001.

F. Honsell, M. Miculan, and I. Scagnetto, An axiomatic approach to metareasoning on systems in higher-order abstract syntax, Proc. ICALP of Lecture Notes in Computer Science, pp.963-978, 2001.

F. Honsell, M. Miculan, and I. , ??-calculus in (Co)inductive-type theory, Theoretical Computer Science, vol.253, issue.2, pp.239-285
DOI : 10.1016/S0304-3975(00)00095-5

M. Huisman, Reasoning about Java programs in higer order logic with PVS and Isabelle, 2001.

G. Kahn, Natural semantics, Proc. of STACS, pp.22-39, 1987.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

O. Laurent, Sémantique Naturelle et Coq : vers la spécification et les preuves sur les langagesàlangages`langagesà objets, 1997.

C. Marché, C. Paulin-mohring, and X. Urbain, The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML, The Journal of Logic and Algebraic Programming, vol.58, issue.1-2, pp.89-106, 2004.
DOI : 10.1016/j.jlap.2003.07.006

R. Mcdowell and D. Miller, A logic for reasoning with higher-order abstract syntax, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.
DOI : 10.1109/LICS.1997.614968

M. Miculan, The expressive power of Structural Operational Semantics with explicit assumptions, Barendregt and Nipkow, pp.292-320, 1994.
DOI : 10.1007/3-540-58085-9_80

M. Miculan, Encoding Logical Theories of Programs, Dipartimento di Informatica, 1997.

M. Miculan, Developing (Meta)Theory of Lambda-calculus in the Theory of Contexts, Proc. of MERLIN, pp.1-22, 2001.

M. Miculan, On the Formalization of the Modal ??-Calculus in the Calculus of Inductive Constructions, Information and Computation, vol.164, issue.1, pp.199-231, 2001.
DOI : 10.1006/inco.2000.2902

D. Miller, A multiple-conclusion meta-logic, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.272-281, 1994.
DOI : 10.1109/LICS.1994.316062

R. Milner and M. Tofte, Co-induction in relational semantics, Theoretical Computer Science, vol.87, issue.1, pp.209-220, 1991.
DOI : 10.1016/0304-3975(91)90033-X

A. Momigliano and S. Ambler, Multi-level Meta-reasoning with Higher-Order Abstract Syntax, Proc. of FOSSACS, 2003.
DOI : 10.1007/3-540-36576-1_24

M. Norrish and . Honsell, Mechanising Hankin and Barendregt using the Gordon-Melham axioms, Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding , MERLIN '03, 2003.
DOI : 10.1145/976571.976577

F. Pfenning and C. Elliott, Higher-order abstract syntax, Proc. of ACM SIGPLAN '88 Symposium on Language Design and Implementation, pp.199-208, 1988.

I. Scagnetto, Reasoning about Names In Higher-Order Abstract Syntax, Dipartimento di Matematica e Informatica, 2002.

I. Scagnetto and M. Miculan, Ambient Calculus and its Logic in the Calculus of Inductive Constructions, Proc. of LFM, 2002.
DOI : 10.1016/S1571-0661(04)80507-3

M. Strecker, Formal Verification of a Java Compiler in Isabelle, Proc. of CADE, pp.63-77, 2002.
DOI : 10.1007/3-540-45620-1_5

H. Tews, A case study in coalgebraic specification: memory management in the FIASCO microkernel, 2000.

J. Van-den-berg, B. Jacobs, and E. Poll, Formal Specification and Verification of JavaCard's Application Identifier Class, Proc. of the JavaCard, 2000.

. Proof, i) By structural induction on the derivation of eval(s, a, s , v

. Proof, By induction on the object [l i =?(x i )b i ] i?I , and Lemmas 30

. Proof, By induction on the result [l i =? i ] i?I , and Lemma 30.(ii)