{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:56Z","timestamp":1761611216195},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418641"},{"type":"electronic","value":"9783540453154"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45315-6_24","type":"book-chapter","created":{"date-parts":[[2007,12,3]],"date-time":"2007-12-03T01:28:39Z","timestamp":1196645319000},"page":"364-378","source":"Crossref","is-referenced-by-count":12,"title":["Higher-Order Abstract Syntax with Induction in Isabelle\/HOL: Formalizing the \u03c0-Calculus and Mechanizing the Theory of Contexts"],"prefix":"10.1007","author":[{"given":"Christine","family":"R\u00f6ckl","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Hirschkoff","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Berghofer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"24_CR1","unstructured":"O. A\u00eft-Mohamed. Pi-Calculus Theory in HOL. PhD thesis, Henry Poincarr\u00e9 University, Nancy, 1996."},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Proc. TPHOL\u201999","author":"S. Berghofer","year":"1999","unstructured":"S. Berghofer and M. Wenzel. Inductive datatypes in HOL \u2014 lessons learned in Formal-Logic Engineering. In Proc. TPHOL\u201999, volume 1690 of LNCS, pages 19\u201336, 1999."},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TCS\u201900","author":"J. Despeyroux","year":"2000","unstructured":"J. Despeyroux. A higher-order specification of the \u03c0-calculus. In Proc. TCS\u201900, LNCS. Springer, 2000. To appear."},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0014049","volume-title":"Proc. TLCA\u201995","author":"J. Despeyroux","year":"1995","unstructured":"J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. In Proc. TLCA\u201995, volume 902 of LNCS, pages 124\u2013138. Springer, 1995."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/3-540-58216-9_36","volume-title":"Proc. LPAR\u201994","author":"J. Despeyroux","year":"1994","unstructured":"J. Despeyroux and A. Hirschowitz. Higher-order abstract syntax with induction in Coq. In Proc. LPAR\u201994, volume 822 of LNCS, pages 159\u2013173. Springer, 1994."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"S. Gay. A framework for the formalisation of pi-calculus type-systems in Isabelle\/HOL. Technical report, University of Glasgow, 2000.","DOI":"10.1007\/3-540-44755-5_16"},{"key":"24_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Proc. TPHOL\u201996","author":"A. Gordon","year":"1996","unstructured":"A. Gordon and T. Melham. Five axioms of alpha-conversion. In Proc. TPHOL\u201996, volume 1125 of LNCS, pages 173\u2013190. Springer, 1996."},{"key":"24_CR8","unstructured":"L. Henry-Gr\u00e9ard. Proof of the subject reduction property for a pi-calculus in Coq. Technical Report RR-3698, INRIA, 1999."},{"key":"24_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BFb0028392","volume-title":"Proc. TPHOL\u201997","author":"D. Hirschkoff","year":"1997","unstructured":"D. Hirschkoff. A full formalisation of --calculus theory in the calculus of constructions. In Proc. TPHOL\u201997, volume 1275 of LNCS, pages 153\u2013169. Springer, 1997."},{"key":"24_CR10","first-page":"204","volume":"158","author":"M. Hofmann","year":"1999","unstructured":"M. Hofmann. Semantical analysis of higher-order abstract syntax. In Proc. LICS\u201999, volume 158, pages 204\u2013213. IEEE, 1999.","journal-title":"Proc. LICS\u201999"},{"issue":"2","key":"24_CR11","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"F. Honsell, M. Miculan, and I. Scagnetto. \u03c0-calculus in (co)inductive type theory. Theoretical Computer Science, 253(2):239\u2013285, 2001.","journal-title":"Theoretical Computer Science"},{"key":"24_CR12","volume-title":"M\u00e9thodes et Outils pour les Preuve Compositionnelles de Syst\u00e8mes Paralle\u00e8les (in french)","author":"B. Mammass","year":"1999","unstructured":"B. Mammass. M\u00e9thodes et Outils pour les Preuve Compositionnelles de Syst\u00e8mes Paralle\u00e8les (in french). PhD thesis, Pierre et Marie Curie University, Paris, 1999."},{"key":"24_CR13","unstructured":"R. McDowell and D. Miller. Reasoning with higher-order abstract syntax in a logical framework. Transactions on Computational Logic, 2000. to appear."},{"issue":"1","key":"24_CR14","first-page":"50","volume":"1","author":"T. Melham","year":"1995","unstructured":"T. Melham. A mechanized theory of the --calculus in HOL. Nordic Journal of Computing, 1(1):50\u201376, 1995.","journal-title":"Nordic Journal of Computing"},{"key":"24_CR15","unstructured":"D. Miller. Specification of the pi-calculus. available at http:\/\/www.cse.psu.edu\/~dale\/lProlog\/examples\/pi-calculus\/toc.html ."},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"17","author":"R. Milner","year":"1992","unstructured":"R. Milner. Functions as processes. Journal of Math. Struct. in Computer Science, 17:119\u2013141, 1992.","journal-title":"Journal of Math. Struct. in Computer Science"},{"key":"24_CR17","unstructured":"R. Milner. Communicating and Mobile Processes. Cambridge University Press, 1999."},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Information and Computation, 100:1\u201377, 1992.","journal-title":"Information and Computation"},{"key":"24_CR19","unstructured":"G. Nadathur and D. Miller. An overview of \u03bbprolog. In M. Press, editor, Proc. LPC\u201998, pages 810\u2013827, 1998."},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle\u2019s object-logics. Technical Report 286, University of Cambridge, Computer Laboratory, 1993.","DOI":"10.1007\/BFb0030541"},{"key":"24_CR21","first-page":"148","volume":"814","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Procs CADE\u201994, volume 814 of LNAI, pages 148\u2013161. Springer, 1994.","journal-title":"Procs CADE\u201994"},{"key":"24_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Isabelle: a generic theorem prover","year":"1994","unstructured":"L. C. Paulson, editor. Isabelle: a generic theorem prover, volume 828 of LNCS. Springer, 1994."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Elf: A language for logic definition and verified metaprogramming. In Proc. LICS\u201989, pages 313\u2013321. IEEE, 1989.","DOI":"10.1109\/LICS.1989.39186"},{"key":"24_CR24","first-page":"202","volume":"1632","author":"F. Pfenning","year":"1999","unstructured":"F. Pfenning and C. Schurmann. System description: Twelf-a meta-logical framework for deductive systems. In Proc. CAD\u201999, volume 1632 of LNAI, pages 202\u2013206. Springer, 1999.","journal-title":"Proc. CAD\u201999"},{"key":"24_CR25","unstructured":"C. Rockl. On the Mechanized Validation of Infinite-State and Parameterized Reactive and Mobile Systems. PhD thesis, Technische Universitat Munchen, 2001. Submitted."},{"key":"24_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/3-540-49019-1_21","volume-title":"Proc. FOSSACS\u201999","author":"C. Rockl","year":"1999","unstructured":"C. Rockl and D. Sangiorgi. A \u03c0-calculus process semantics of concurrent idealized ALGOL. In Proc. FOSSACS\u201999, volume 1578 of LNCS, pages 306\u2013321. Springer, 1999."},{"key":"24_CR27","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1006\/inco.1995.1018","volume":"116","author":"D. Walker","year":"1995","unstructured":"D. Walker. Objects in the \u03c0-calculus. Information and Computation, 116:253\u2013271, 1995.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45315-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T09:10:04Z","timestamp":1557047404000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45315-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418641","9783540453154"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45315-6_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}