{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T06:55:39Z","timestamp":1794380139242,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540221647","type":"print"},{"value":"9783540248491","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_21","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T16:34:24Z","timestamp":1281285264000},"page":"324-337","source":"Crossref","is-referenced-by-count":1,"title":["Mobility Types in Coq"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BFb0053547","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Cardelli","year":"1998","unstructured":"Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol.\u00a01378, pp. 140\u2013155. Springer, Heidelberg (1998)"},{"key":"21_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"21_CR3","series-title":"ENTCS","volume-title":"Proceedings of CATS\u20192003","author":"M. Coppo","year":"2003","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Giovannetti, E., Salvo, I.: M3: Mobility types for mobile processes in mobile ambients. In: Proceedings of CATS\u20192003. ENTCS, vol.\u00a078, Springer, Heidelberg (2003)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Vision, Virtual Reality and Robotics in Medicine","author":"J. Despeyroux","year":"1995","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order syntax in Coq. In: Ayache, N. (ed.) CVRMed 1995. LNCS, vol.\u00a0905, Springer, Heidelberg (1995); Also appears as INRIA research report RR-2556 (April 1995)"},{"issue":"1","key":"21_CR5","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. J. ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"21_CR6","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, pp. 963\u2013978. Springer, Heidelberg (2001), http:\/\/www.dimi.uniud.it\/~miculan\/Papers\/"},{"key":"#cr-split#-21_CR7.1","doi-asserted-by":"crossref","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: \u03c0-calculus in (co)inductive type theory. Theoretical computer science\u00a0(2), 239\u2013285 (2001);","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"#cr-split#-21_CR7.2","unstructured":"First appeared as a talk at TYPES 1998 annual workshop"},{"key":"21_CR8","unstructured":"INRIA. The Coq Proof Assistant Reference Manual - Version 7.4. INRIA, Rocquencourt, France (February 2003), Available at ftp:\/\/ftp.inria.fr\/INRIA\/coq\/V7.4\/doc"},{"key":"21_CR9","unstructured":"Martin-L\u00f6f, P.: On the meaning of the logical constants and the justifications of the logic laws. Technical Report 2, Dipartimento di Matematica, Universit\u2018a di Siena (1985)"},{"key":"21_CR10","series-title":"ENTCS","volume-title":"Proceedings of LFM 2002","author":"M. Miculan","year":"2002","unstructured":"Miculan, M., Scagnetto, I.: Ambient calculus and its logic in the calculus of inductive constructions. In: Proceedings of LFM 2002. ENTCS, vol.\u00a070.2, Elsevier, Amsterdam (2002)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:57:39Z","timestamp":1605743859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_21","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/b98246","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}