{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:37:29Z","timestamp":1737005849052,"version":"3.33.0"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,4,19]],"date-time":"2007-04-19T00:00:00Z","timestamp":1176940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2007,4,19]],"date-time":"2007-04-19T00:00:00Z","timestamp":1176940800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,7]]},"DOI":"10.1007\/s10817-006-9061-y","type":"journal-article","created":{"date-parts":[[2007,4,18]],"date-time":"2007-04-18T13:50:44Z","timestamp":1176904244000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts"],"prefix":"10.1007","volume":"39","author":[{"given":"Alberto","family":"Ciaffaglione","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,19]]},"reference":[{"key":"9061_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Berlin Heidelberg New York (1996)"},{"key":"9061_CR2","unstructured":"Barendregt, H., Nipkow, T. (eds.): In: Proceedings of TYPES. Lecture Notes in Computer Science, vol. 806 (1994)"},{"key":"9061_CR3","unstructured":"Bertot, Y.: A certified compiler for an imperative language. Technical Report RR-3488, INRIA (1998)"},{"issue":"3","key":"9061_CR4","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1017\/S0956796806005892","volume":"16","author":"A. Bucalo","year":"2006","unstructured":"Bucalo, A., Hofmann, M., Honsell, F., Miculan, M., Scagnetto, I.: Consistency of the theory of contexts. J. Funct. Program. 16(3), 327\u2013395 (2006)","journal-title":"J. Funct. Program."},{"key":"9061_CR5","doi-asserted-by":"crossref","unstructured":"Burstall, R., Honsell, F.: Operational semantics in a natural deduction setting. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 185\u2013214. Cambridge University Press (1990)","DOI":"10.1017\/CBO9780511569807.009"},{"issue":"1","key":"9061_CR6","first-page":"27","volume":"8","author":"L. Cardelli","year":"1995","unstructured":"Cardelli, L.: Obliq: a language with distributed scope. Comput. Syst. 8(1), 27\u201359 (1995)","journal-title":"Comput. Syst."},{"issue":"1","key":"9061_CR7","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1006\/inco.2001.2951","volume":"179","author":"I. Cervesato","year":"2002","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19\u201375 (2002)","journal-title":"Inf. Comput."},{"key":"9061_CR8","unstructured":"Chirimar, J.L.: Proof theoretic approach to specification languages. Ph.D. thesis, University of Pennsylvania (1995)"},{"key":"9061_CR9","unstructured":"Ciaffaglione, A.: Certified reasoning on real numbers and objects in co-inductive type theory. Ph.D. thesis, Dipartimento di Matematica e Informatica, Universit\u00e0 di Udine, Italy and INPL-ENSMN, Nancy, France (2003)"},{"key":"9061_CR10","volume-title":"Proceedings of LPAR. Lecture Notes in Computer Science, vol. 2850","author":"A. Ciaffaglione","year":"2003","unstructured":"Ciaffaglione, A., Liquori, L., Miculan, M.: Imperative object-calculi in (Co)inductive type theories. In: Proceedings of LPAR. Lecture Notes in Computer Science, vol. 2850. Springer, Berlin Heidelberg New York (2003)"},{"key":"9061_CR11","doi-asserted-by":"crossref","unstructured":"Ciaffaglione, A., Liquori, L., Miculan, M.: Reasoning on an imperative object-calculus in higher-order abstract syntax. In: [30], ACM (2003)","DOI":"10.1145\/976571.976574"},{"key":"9061_CR12","unstructured":"Ciaffaglione, A., Liquori, L., Miculan, M.: The web appendix of this paper. University of Udine, Italy. http:\/\/www.dimi.uniud.it\/ciaffagl (2003)"},{"key":"9061_CR13","doi-asserted-by":"crossref","unstructured":"Ciaffaglione, A., Scagnetto, I.: Plug and play the theory of contexts in higher-order abstract syntax. In: Proceedings of CoMeta (2003)","DOI":"10.1016\/j.entcs.2004.09.022"},{"key":"9061_CR14","unstructured":"Coq: The Coq Proof Assistant 7.3. INRIA. http:\/\/coq.inria.fr (2003)"},{"key":"9061_CR15","unstructured":"Crole, R.L.: Lectures on [Co]induction and [Co]algebras. Technical Report 1998\/12, Department of Mathematics and Computer Science, University of Leicester (1998)"},{"key":"9061_CR16","unstructured":"Despeyroux, J.: Proof of translation in natural semantics. In: Proceedings of LICS, pp. 193\u2013205, ACM (1986)"},{"key":"9061_CR17","volume-title":"Proceedings of TLCA. Lecture Notes in Computer Science, vol. 905","author":"J. Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order syntax in Coq. In: Proceedings of TLCA. Lecture Notes in Computer Science, vol. 905. Springer, Berlin Heidelberg New York (1995)"},{"issue":"4","key":"9061_CR18","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1017\/S0960129501003346","volume":"11","author":"J. Despeyroux","year":"2001","unstructured":"Despeyroux, J., Leleu, P.: Recursion over objects of functional type. Math. Struct. Comput. Sci. 11(4), 555\u2013572 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9061_CR19","first-page":"198","volume-title":"Proceedings of TPHOLs. Lecture Notes in Computer Science, vol. 2410","author":"A.P. Felty","year":"2002","unstructured":"Felty, A.P.: Two-level meta-reasoning in Coq. In: Carre\u00f1o, V., Mu\u00f1oz, C., Tashar, S. (eds.) Proceedings of TPHOLs. Lecture Notes in Computer Science, vol. 2410, pp. 198\u2013213. Springer, Berlin Heidelberg New York (2002)"},{"key":"9061_CR20","doi-asserted-by":"crossref","unstructured":"Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: [37], pp. 193\u2013202. IEEE Computer Society Press (1999)","DOI":"10.1109\/LICS.1999.782615"},{"key":"9061_CR21","first-page":"3","volume":"1","author":"K. Fisher","year":"1994","unstructured":"Fisher, K., Honsell, F., Mitchell, J.: A lambda calculus of objects and method specialization. Nord. J. Comput. 1, 3\u201337 (1994)","journal-title":"Nord. J. Comput."},{"key":"9061_CR22","unstructured":"Frost, J.: A case study of co-induction in Isabelle. Technical Report 359, University of Cambridge, Computer Laboratory. Revised version of CUCL 308, August 1993 (1995)"},{"key":"9061_CR23","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M.J. Gabbay","year":"2002","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13, 341\u2013363 (2002)","journal-title":"Form. Asp. Comput."},{"key":"9061_CR24","first-page":"417","volume-title":"Proceedings of CADE 17","author":"G. Gillard","year":"2000","unstructured":"Gillard, G.: A formalization of a concurrent object calculus up to alpha-conversion. In: Proceedings of CADE 17, pp. 417\u2013432. Springer, Berlin Heidelberg New York (2000)"},{"key":"9061_CR25","first-page":"39","volume-title":"Proceedings of TYPES. Lecture Notes in Computer Science, vol. 996","author":"E. Gim\u00e9nez","year":"1995","unstructured":"Gim\u00e9nez, E.: Codifying guarded recursion definitions with recursive schemes. In: Smith, J. (ed.) Proceedings of TYPES. Lecture Notes in Computer Science, vol. 996, pp. 39\u201359. Springer, Berlin Heidelberg New York (1995)"},{"issue":"1","key":"9061_CR26","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of ACM 40(1), 143\u2013184 (1993)","journal-title":"Journal of ACM"},{"key":"9061_CR27","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: [37], pp. 204\u2013213. IEEE Computer Society Press (1999)","DOI":"10.1109\/LICS.1999.782616"},{"key":"9061_CR28","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Tang, F.: Implementing a program logic of objects in a higher-order logic theorem prover. In: Proceedings of TPHOLs, pp. 268\u2013282 (2000)","DOI":"10.1007\/3-540-44659-1_17"},{"key":"9061_CR29","unstructured":"Hofmann, M., Tang, F.: A higher-order embedding of a logic of objects. Technical Report EDI-INF-RR-0033, LFCS, University of Edinburgh (2001)"},{"key":"9061_CR30","unstructured":"Honsell, F., Miculan, M., Momigliano, A. (eds.): Eighth ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN 2003. ACM (2003)"},{"key":"9061_CR31","doi-asserted-by":"crossref","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In: Proceedings of ICALP. Lecture Notes in Computer Science, vol. 2076, pp. 963\u2013978 (2001)","DOI":"10.1007\/3-540-48224-5_78"},{"issue":"2","key":"9061_CR32","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: \u03c0-calculus in (Co)inductive type theory. Theor. Comp. Sci. 253(2), 239\u2013285 (2001)","journal-title":"Theor. Comp. Sci."},{"key":"9061_CR33","unstructured":"Huisman, M.: Reasoning about Java programs in higher order logic with PVS and Isabelle. Ph.D. thesis, Katholieke Universiteit Nijmegen (2001)"},{"key":"9061_CR34","first-page":"22","volume-title":"Proceedings of STACS. Lecture Notes in Computer Science, vol. 247","author":"G. Kahn","year":"1987","unstructured":"Kahn, G.: Natural semantics. In: Proceedings of STACS. Lecture Notes in Computer Science, vol. 247, pp. 22\u201339. Springer, Berlin Heidelberg New York (1987)"},{"issue":"3","key":"9061_CR35","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified bytecode verifiers. Theor. Comp. Sci. 298(3), 583\u2013626 (2003)","journal-title":"Theor. Comp. Sci."},{"key":"9061_CR36","unstructured":"Laurent, O.: S\u00e9mantique naturelle et Coq: vers la sp\u00e9cification et les preuves sur les langages \u00e0 objets. Technical Report RR-3307, INRIA (1997)"},{"key":"9061_CR37","unstructured":"Longo, G. (ed.): Proceedings of LICS. IEEE Computer Society Press (1999)"},{"issue":"1-2","key":"9061_CR38","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA: a tool for certification of JAVA\/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming 58(1-2), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"9061_CR39","doi-asserted-by":"crossref","unstructured":"McDowell, R., Miller, D.: A logic for reasoning with higher-order abstract syntax. In: Proceedings of 12 th LICS, pp. 434\u2013445 (1997)","DOI":"10.1109\/LICS.1997.614968"},{"key":"9061_CR40","doi-asserted-by":"crossref","unstructured":"Miculan, M.: The expressive power of structural operational semantics with explicit assumptions. In: [2], pp. 292\u2013320 (1994)","DOI":"10.1007\/3-540-58085-9_80"},{"key":"9061_CR41","unstructured":"Miculan, M.: Encoding logical theories of programs. Ph.D. thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Italy (1997)"},{"key":"9061_CR42","doi-asserted-by":"crossref","unstructured":"Miculan, M.: Developing (meta)theory of lambda-calculus in the theory of contexts. In: Ambler, S., Crole, R., Momigliano, A. (eds.) Proceedings of MERLIN ENTCS, vol. 58.1, pp. 1\u201322. Elsevier (2001)","DOI":"10.1016\/S1571-0661(04)00278-6"},{"issue":"1","key":"9061_CR43","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1006\/inco.2000.2902","volume":"164","author":"M. Miculan","year":"2001","unstructured":"Miculan, M.: On the formalization of the modal \u03bc-calculus in the calculus of inductive constructions. Inf. Comput. 164(1), 199\u2013231 (2001)","journal-title":"Inf. Comput."},{"key":"9061_CR44","doi-asserted-by":"crossref","unstructured":"Miller, D.: A multiple-conclusion meta-logic. In: Abramsky, S. (ed.) Proceedings of LICS. Paris, pp. 272\u2013281 (1994)","DOI":"10.1109\/LICS.1994.316062"},{"key":"9061_CR45","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0304-3975(91)90033-X","volume":"87","author":"R. Milner","year":"1991","unstructured":"Milner, R., Tofte, M.: Co-induction in relational semantics. Theor. Comp. Sci. 87, 209\u2013220 (1991)","journal-title":"Theor. Comp. Sci."},{"key":"9061_CR46","volume-title":"Proceedings of FOSSACS","author":"A. Momigliano","year":"2003","unstructured":"Momigliano, A., Ambler, S.: Multi-level meta-reasoning with higher order abstract syntax. In: Proceedings of FOSSACS. Springer, Berlin Heidelberg New York (2003)"},{"key":"9061_CR47","doi-asserted-by":"crossref","unstructured":"Norrish, M.: Mechanising Hankin and Barendregt using the Gordon\u2013Melham axioms. In: [30], ACM (2003)","DOI":"10.1145\/976571.976577"},{"key":"9061_CR48","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of ACM SIGPLAN \u201988 Symposium on Language Design and Implementation, pp. 199\u2013208 (1988)","DOI":"10.1145\/960116.54010"},{"key":"9061_CR49","unstructured":"Scagnetto, I.: Reasoning about names in higher-order abstract syntax. Ph.D. thesis, Dipartimento di Matematica e Informatica, Universit\u00e0 di Udine, Italy (2002)"},{"key":"9061_CR50","doi-asserted-by":"crossref","unstructured":"Scagnetto, I., Miculan, M.: Ambient calculus and its logic in the calculus of inductive constructions. In: Pfenning, F. (ed.) Proceedings of LFM. Electronic Notes in Theoretical Computer Science, vol. 70.2. Elsevier (2002)","DOI":"10.1016\/S1571-0661(04)80507-3"},{"key":"9061_CR51","unstructured":"Self: The Self programming language. Sun Microsystems. http:\/\/research.sun.com\/self\/language.html (2003)"},{"key":"9061_CR52","first-page":"63","volume-title":"Proceedings of CADE. Lecture Notes in Computer Science, vol. 2392","author":"M. Strecker","year":"2002","unstructured":"Strecker, M.: Formal verification of a Java compiler in Isabelle. In: Proceedings of CADE. Lecture Notes in Computer Science, vol. 2392, pp. 63\u201377. Springer, Berlin Heidelberg New York (2002)"},{"key":"9061_CR53","unstructured":"Tews, H.: A case study in coalgebraic specification: memory management in the FIASCO microkernel. Technical report, TU Dresden (2000)"},{"key":"9061_CR54","doi-asserted-by":"crossref","unstructured":"Van\u00a0den Berg, J., Jacobs, B., Poll, E.: Formal specification and verification of JavaCard\u2019s Application Identifier Class. In: Proceedings of the JavaCard 2000 Workshop (2001)","DOI":"10.1007\/3-540-45165-X_11"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9061-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-006-9061-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9061-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9061-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,15]],"date-time":"2025-01-15T20:48:41Z","timestamp":1736974121000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-006-9061-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,4,19]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["9061"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9061-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2007,4,19]]},"assertion":[{"value":"1 February 2004","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 June 2006","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 June 2006","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 April 2007","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}