{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T20:38:21Z","timestamp":1770496701884,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540280057","type":"print"},{"value":"9783540318644","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_4","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"38-53","source":"Crossref","is-referenced-by-count":61,"title":["Nominal Techniques in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Christian","family":"Urban","sequence":"first","affiliation":[]},{"given":"Christine","family":"Tasson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/BFb0037095","volume-title":"Typed Lambda Calculi and Applications","author":"T. Altenkirch","year":"1993","unstructured":"Altenkirch, T.: A Formalization of the Strong Normalisation Proof for System F in LEGO. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 13\u201328. Springer, Heidelberg (1993)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized Metatheory for the Masses: The PoplMark Challenge. (accepted at tphol) (2005)","DOI":"10.1007\/11541868_4"},{"key":"4_CR3","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"H. Barendregt","year":"1981","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. In: Studies in Logic and the Foundations of Mathematics, vol.\u00a0103, North-Holland, Amsterdam (1981)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","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 Abstract Syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 124\u2013138. Springer, Heidelberg (1995)"},{"key":"4_CR5","unstructured":"Gabbay, M.J.: A Theory of Inductive Definitions With \u03b1-equivalence. PhD thesis, University of Cambridge (2000)"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M.J. Gabbay","year":"2001","unstructured":"Gabbay, M.J., Pitts, A.M.: A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing\u00a013, 341\u2013363 (2001)","journal-title":"Formal Aspects of Computing"},{"key":"4_CR7","volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. In: Cambridge Tracts in Theoretical Computer Science, vol.\u00a07, Cambridge University Press, Cambridge (1989)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","first-page":"414","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"A.D. Gordon","year":"1994","unstructured":"Gordon, A.D.: 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. 414\u2013426. Springer, Heidelberg (1994)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Theorem Proving in Higher Order Logics","author":"A.D. Gordon","year":"1996","unstructured":"Gordon, A.D., Melham, T.: Five Axioms of Alpha-Conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 173\u2013190. Springer, Heidelberg (1996)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0028392","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"Hirschkoff, D.: A Full Formalisation of \u03c0-Calculus Theory in the Calculus of Constructions. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 153\u2013169. Springer, Heidelberg (1997)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"4_CR12","unstructured":"Norrish, M.: Mechanising \u03bb-calculus using a Classical First Order Theory of Terms with Permutations, forthcoming"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-540-30142-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Norrish","year":"2004","unstructured":"Norrish, M.: Recursive function definition for types with binders. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 241\u2013256. Springer, Heidelberg (2004)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Paulson, L.: Defining Functions on Equivalence Classes. ACM Transactions on Computational Logic (to appear)","DOI":"10.1145\/1183278.1183280"},{"key":"4_CR15","first-page":"199","volume-title":"Proc.\u00a0of the ACM SIGPLAN Conference PLDI","author":"F. Pfenning","year":"1989","unstructured":"Pfenning, F., Elliott, C.: Higher-Order Abstract Syntax. In: Proc.\u00a0of the ACM SIGPLAN Conference PLDI, pp. 199\u2013208. ACM Press, New York (1989)"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal Logic, A First Order Theory of Names and Binding. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"4_CR17","volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"A.S. Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. In: Cambridge Tracts in Theoretical Computer Science, vol.\u00a043, Cambridge University Press, Cambridge (2000)"},{"issue":"1-2","key":"4_CR18","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","volume":"323","author":"C. Urban","year":"2004","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal Unification. Theoretical Computer Science\u00a0323(1-2), 473\u2013497 (2004)","journal-title":"Theoretical Computer Science"},{"key":"4_CR19","unstructured":"VanInwegen, M.: The Machine-Assisted Proof of Programming Language Properties. PhD thesis, University of Pennsylvania, Available as MS-CIS-96-31 (1996)"},{"key":"4_CR20","unstructured":"Wenzel, M.: Using Axiomatic Type Classes in Isabelle. Manual in the Isabelle distribution"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:09:15Z","timestamp":1605643755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11532231_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}