{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:51:15Z","timestamp":1725558675828},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540201014"},{"type":"electronic","value":"9783540398134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39813-4_4","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T19:27:49Z","timestamp":1277839669000},"page":"59-77","source":"Crossref","is-referenced-by-count":3,"title":["Imperative Object-Based Calculi in Co-inductive Type Theories"],"prefix":"10.1007","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","reference":[{"key":"4_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, Heidelberg (1996)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030634","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"M. Abadi","year":"1997","unstructured":"Abadi, M., Leino, K.: A logic of object-oriented programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214. Springer, Heidelberg (1997)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","year":"1994","unstructured":"Barendregt, H., Nipkow, T. (eds.): TYPES 1993. LNCS, vol.\u00a0806. Springer, Heidelberg (1994)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-45719-4_4","volume-title":"Algebraic Methodology and Software Technology","author":"G. Barthe","year":"2002","unstructured":"Barthe, G., Courtieu, P., Dufay, G., de Sousa, S.M.: Tool-assisted specification and verification of the JavaCard platform. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, p. 41. Springer, Heidelberg (2002)"},{"key":"4_CR5","unstructured":"Bertot, Y.: A certified compiler for an imperative language. Technical Report INRIA (1998)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-44585-4_3","volume-title":"Computer Aided Verification","author":"Y. Bertot","year":"2001","unstructured":"Bertot, Y.: Formalizing a JVML verifier for initialization in a theorem prover. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 14. Springer, Heidelberg (2001)"},{"key":"4_CR7","volume-title":"Logical Frameworks","author":"R. Burstall","year":"1990","unstructured":"Burstall, R., Honsell, F.: Operational semantics in a natural deduction setting. In: Logical Frameworks. Cambridge University Press, Cambridge (1990)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: Obliq: A Language with Distributed Scope. Computing Systems (1995)","DOI":"10.1145\/199448.199516"},{"key":"4_CR9","unstructured":"Ciaffaglione, A.: Certified reasoning on Real Numbers and Objects in Co-inductive Type Theory. PhD thesis, Dipartimento di Matematica e Informatica, Universit\u00e0 di Udine, Italy and LORIA-INPL, Nancy, France (2003)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Ciaffaglione, A., Liquori, L., Miculan, M.: On the formalization of imperative object-based calculi in (co)inductive type theories. Technical Report INRIA (2003)","DOI":"10.1007\/978-3-540-39813-4_4"},{"key":"4_CR11","unstructured":"Ciaffaglione, A., Liquori, L., Miculan, M.: The Web Appendix of this paper (2003), http:\/\/www.dimi.uniud.it\/~ciaffagl\/Objects\/Imp-covarsigma.tar.gz"},{"key":"4_CR12","volume-title":"Proc. of LICS 1986","author":"J. Despeyroux","year":"1986","unstructured":"Despeyroux, J.: Proof of translation in natural semantics. In: Proc. of LICS 1986. ACM, New York (1986)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014049","volume-title":"Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902. Springer, Heidelberg (1995)"},{"key":"4_CR14","unstructured":"Fisher, K., Honsell, F., Mitchell, J.: A lambda calculus of objects and method specialization. Nordic Journal of Computing (1994)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1995","unstructured":"Gim\u00e9nez, E.: Codifying guarded recursion definitions with recursive schemes. In: Smith, J., Dybjer, P., Nordstr\u00f6m, B. (eds.) TYPES 1994. LNCS, vol.\u00a0996. Springer, Heidelberg (1995)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM (1993)","DOI":"10.1145\/138027.138060"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/3-540-48224-5_78","volume-title":"Automata, Languages and Programming","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, p. 963. Springer, Heidelberg (2001)"},{"key":"4_CR18","unstructured":"Huisman, M.: Reasoning about Java programs in higher order logic with PVS and Isabelle. PhD thesis, Katholieke Universiteit Nijmegen (2001)"},{"key":"4_CR19","unstructured":"INRIA. The Coq Proof Assistant (2003), http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039592","volume-title":"STACS 87","author":"G. Kahn","year":"1987","unstructured":"Kahn, G.: Natural Semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol.\u00a0247. Springer, Heidelberg (1987)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Klein, G., Nipkow, T.: Verified bytecode verifiers. TCS 298(3) (2003)","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"4_CR22","unstructured":"Laurent, O.: S\u00e9mantique Naturelle et Coq: vers la sp\u00e9cification et les preuves sur les langages \u00e0 objets. Technical Report INRIA (1997)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Miculan, M.: The expressive power of structural operational semantics with explicit assumptions. In: [3]","DOI":"10.1007\/3-540-58085-9_80"},{"key":"4_CR24","unstructured":"Miculan, M.: Encoding Logical Theories of Programs. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa (1997)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proc. of ACM SIGPLAN (1988)","DOI":"10.1145\/53990.54010"},{"key":"4_CR26","unstructured":"Scagnetto, I.: Reasoning about Names In Higher-Order Abstract Syntax. PhD thesis, Dipartimento di Matematica e Informatica, Universit\u00e0 di Udine (2002)"},{"key":"4_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction - CADE-18","author":"M. Strecker","year":"2002","unstructured":"Strecker, M.: Formal verification of a Java compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 63. Springer, Heidelberg (2002)"},{"key":"4_CR28","unstructured":"Tews, H.: A case study in coalgebraic specification: memory management in the FIASCO microkernel. Technical report, TU Dresden (2000)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45165-X_11","volume-title":"Java on Smart Cards: Programming and Security","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B., Poll, E.: Formal specification and verification of JavaCard\u2019s application identifier class. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol.\u00a02041, p. 137. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39813-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T15:00:01Z","timestamp":1559228401000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39813-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540201014","9783540398134"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39813-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}