{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:01Z","timestamp":1725475801140},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_33","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T16:12:31Z","timestamp":1167408751000},"page":"417-432","source":"Crossref","is-referenced-by-count":3,"title":["A Formalization of a Concurrent Object Calculus up to \u03b1-Conversion"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Gillard","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Monographs in Computer Science","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. Monographs in Computer Science. Springer, Heidelberg (1996)"},{"key":"33_CR2","unstructured":"Barras, B.: Coq en Coq. M\u00e9moire du DEA informatique, math\u00e9matiques et applications, \u00c9cole Polytechnique, 1995. INRIA research report RR-3026 (October 1996)"},{"key":"33_CR3","unstructured":"Bertot, J., Bertot, Y., Coscoy, Y., Goguen, H., Montagnac, F.: User uide to the CtCoq proof environment, Inria technical report, RT-0210 (October 1997)"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In: Geuvers, J.H., Nederpelt, R.P., de Vrijer, R.C. (eds.) Selected Papers on Automath, Studies in Logic vol.\u00a0133, pp. 375\u2013388. Springer, Heidelberg (1994) (reprinted)","DOI":"10.1016\/S0049-237X(08)70216-7"},{"key":"33_CR5","unstructured":"Despeyroux, J.: A higher-order specification of the pi-calculus. Presented at the Modelisation and Verification seminar, Marseille (December 1998); submitted for publication, March"},{"key":"33_CR6","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/3-540-58216-9_36","volume-title":"Logic Programming and Automated Reasoning","author":"J. Despeyroux","year":"1994","unstructured":"Despeyroux, J., Hirschowitz, A.: Higher-order syntax and induction in Coq. In: Pfenning, F. (ed.) LPAR 1994. LNCS (LNAI), vol.\u00a0822, pp. 159\u2013173. Springer, Heidelberg (1994) Also appears as INRIA Research Report RR-2292 (June 1994)"},{"key":"33_CR7","unstructured":"Miculan, M., Honsell, F., Scagnetto, I.: Pi calculus in (co)inductive type theories. Technical report, Universita\u2019 di Udine (September 1998)"},{"key":"33_CR8","volume-title":"Proceedings of the HLCL 1998 Conference","author":"A. Gordon","year":"1998","unstructured":"Gordon, A., Hankin, P.: A concurrent object calculus: reduction and typing. In: Proceedings of the HLCL 1998 Conference. Elsevier ENTCS, Amsterdam (1998)"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Gillard, G.: A full formalization of a concurrent object cal-culus up to alpha-conversion (January 2000); draft, Available at ftp:\/\/ftp-sop.inria.fr\/certilab\/ps\/conc_calculus.ps","DOI":"10.1007\/10721959_33"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/3-540-57826-9_152","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"A. Gordon","year":"1994","unstructured":"Gordon, A.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780, pp. 413\u2013425. Springer, Heidelberg (1994)"},{"key":"#cr-split#-33_CR11.1","unstructured":"Henry_Greard, L.: A proof of type preservation for the pi-calculus in Coq. Research Report RR-3698, Inria (December 1998);"},{"key":"#cr-split#-33_CR11.2","unstructured":"Also available in the Coq Contrib library"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Hirschkoff, D.: A full formalization of pi-calculus theory in the Calculus of Constructions. In: Felty, A., Gunter, E. (eds.) Proceedings of the International Conference on Theorem Proving in Higher Order Logics, Murray Hill, New Jersey (August 1997)","DOI":"10.1007\/BFb0028392"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BFb0037113","volume-title":"Typed Lambda Calculi and Applications","author":"J. McKinna","year":"1993","unstructured":"McKinna, J., Pollack, R.: Pure Type Sytems formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 289\u2013305. Springer, Heidelberg (1993)"},{"key":"33_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, R., Walker, J.: A calculus of mobile processes (part I and II). Information and Computation\u00a0100, 1\u201377 (1992)","journal-title":"Information and Computation"},{"key":"33_CR15","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. PhD thesis, University Paris VII (Mai 1994)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:42:43Z","timestamp":1556005363000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/10721959_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}