{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215630},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422877"},{"type":"electronic","value":"9783540482246"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-48224-5_78","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:04Z","timestamp":1193538544000},"page":"963-978","source":"Crossref","is-referenced-by-count":32,"title":["An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marino","family":"Miculan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"78_CR1","unstructured":"A. Bucalo, M. Hofmann, F. Honsell, M. Miculan, and I. Scagnetto. Using functor categories to explain and justify an axiomatization of variables and schemata in HOAS. In preparation, 2001."},{"key":"78_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of TLCA\u201995","author":"J. Despeyroux","year":"1995","unstructured":"J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order syntax in Coq. In Proc. of TLCA\u201995, LNCS 905. Springer-Verlag, 1995."},{"key":"78_CR3","doi-asserted-by":"crossref","unstructured":"J. Despeyroux, F. Pfenning, and C. Sch\u00fcrmann. Primitive recursion for higher order abstract syntax. Technical Report CMU-CS-96-172, Carnegie Mellon University, September 1996.","DOI":"10.1007\/3-540-62688-3_34"},{"key":"78_CR4","doi-asserted-by":"crossref","unstructured":"M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In G. Longo, ed., Proc. 14th LICS, pages 193\u2013202. IEEE, 1999.","DOI":"10.1109\/LICS.1999.782615"},{"key":"78_CR5","unstructured":"M. J. Gabbay. A Theory of Inductive Definitions With \u03b1-equivalence. PhD thesis, Trinity College, Cambridge University, 2000."},{"key":"78_CR6","doi-asserted-by":"crossref","unstructured":"M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In G. Longo, ed., Proc. 14th LICS, pages 214\u2013224. IEEE, 1999.","DOI":"10.1109\/LICS.1999.782617"},{"issue":"1","key":"78_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. J. ACM, 40(1):143\u2013184, Jan. 1993.","journal-title":"J. ACM"},{"key":"78_CR8","doi-asserted-by":"crossref","unstructured":"M. Hofmann. Semantical analysis of higher-order abstract syntax. In G. Longo, ed., Proc. 14th LICS, pages 204\u2013213. IEEE, 1999.","DOI":"10.1109\/LICS.1999.782616"},{"key":"78_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/3-540-61780-9_69","volume-title":"Proc. of TYPES\u201995","author":"F. Honsell","year":"1996","unstructured":"F. Honsell and M. Miculan. A natural deduction approach to dynamic logics. In Proc. of TYPES\u201995, LNCS 1158, pages 165\u2013182. Springer-Verlag, 1996."},{"issue":"2","key":"78_CR10","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. TCS 253(2):239\u2013285, 2001. First appeared as a talk at TYPES\u201998 annual workshop.","journal-title":"TCS"},{"key":"78_CR11","unstructured":"INRIA. The Coq Proof Assistant, 2000. http:\/\/www.coq.inria.fr\/doc\/main.html ."},{"key":"78_CR12","doi-asserted-by":"crossref","unstructured":"R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax. In Proc. 12 th LICS. IEEE, 1997.","DOI":"10.1109\/LICS.1997.614968"},{"key":"78_CR13","series-title":"PhD thesis","volume-title":"Encoding Logical Theories of Programs","author":"M. Miculan","year":"1997","unstructured":"M. Miculan. Encoding Logical Theories of Programs. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Italy, Mar. 1997."},{"key":"78_CR14","unstructured":"M. Miculan. Encoding and metareasoning of call-by-name \u03bb-calculus. Available at http:\/\/www.dimi.uniud.it\/~miculan\/CoqCode\/HOAS , 2000."},{"issue":"1","key":"78_CR15","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. Inform. and Comput., 100(1):1\u201377, 1992.","journal-title":"Inform. and Comput."},{"key":"78_CR16","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proc. of ACM SIGPLAN\u2019 88, pages 199\u2013208, 1988.","DOI":"10.1145\/53990.54010"},{"key":"78_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/10722010_15","volume-title":"Proc. MPC2000","author":"A. M. Pitts","year":"2000","unstructured":"A. M. Pitts and M. J. Gabbay. A metalanguage for programming with bound names modulo renaming. In Proc. MPC2000, LNCS 1837, pages 230\u2013255. Springer, 2000."},{"key":"78_CR18","series-title":"Lect Notes Comput Sci","first-page":"359","volume-title":"Proc. FOSSACS 2001","author":"C. R\u00f6ckl","year":"2001","unstructured":"C. R\u00f6ckl, D. Hirschkoff, and S. Berghofer. Higher-order abstract syntax with induction in Isabelle\/HOL: Formalising the \u03c0-calculus and mechanizing the theory of contexts. In Proc. FOSSACS 2001, LNCS 2030, pages 359\u2013373. Springer, 2001."},{"key":"78_CR19","series-title":"PhD thesis","volume-title":"Reasoning on Names In Higher-Order Abstract Syntax","author":"I. Scagnetto","year":"2002","unstructured":"I. Scagnetto. Reasoning on Names In Higher-Order Abstract Syntax. PhD thesis, Dip. di Matematica e Informatica, Universit\u00e0 di Udine, 2002. In preparation."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48224-5_78","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T11:08:41Z","timestamp":1684062521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48224-5_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422877","9783540482246"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-48224-5_78","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}