{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:26:09Z","timestamp":1742919969492,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642253782"},{"type":"electronic","value":"9783642253799"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25379-9_9","type":"book-chapter","created":{"date-parts":[[2011,11,14]],"date-time":"2011-11-14T01:33:47Z","timestamp":1321234427000},"page":"87-102","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem"],"prefix":"10.1007","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[]},{"given":"Henk","family":"Barendregt","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. Elsevier (2001)"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods in Computer Science\u00a07(1) (2011)","DOI":"10.2168\/LMCS-7(1:11)2011"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science\u00a05(2) (2008)","DOI":"10.2168\/LMCS-5(2:16)2009"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with smt solvers. Automated Deduction (2011) (accepted)","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-57880-3_9","volume-title":"Programming Languages and Systems - ESOP \u201994","author":"C. B\u00f6hm","year":"1994","unstructured":"B\u00f6hm, C., Piperno, A., Guerrini, S.: Lambda-definition of function(al)s by normal forms. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol.\u00a0788, pp. 135\u2013149. Springer, Heidelberg (1994)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Hankin, C.: Lambda Calculi: A Guide for Computer Scientists. Graduate Texts in Computer Science, vol.\u00a03. Clarendon Press (1993)","DOI":"10.1093\/oso\/9780198538417.001.0001"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-14052-5_5","volume-title":"Interactive Theorem Proving","author":"B. Huffman","year":"2010","unstructured":"Huffman, B., Urban, C.: A New Foundation for Nominal Isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 35\u201350. Springer, Heidelberg (2010)"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, C.: Quotients revisited for Isabelle\/HOL. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.-C. (eds.) Proc. of the 26th ACM Symposium on Applied Computing (SAC 2011), pp. 1639\u20131644. ACM (2011)","DOI":"10.1145\/1982185.1982529"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Minamide, Y., Okuma, K.: Verifying CPS transformations in Isabelle\/HOL. In: Proc. of the Workshop on Mechanized reasoning about languages with variable binding (MERLIN 2003). ACM (2003)","DOI":"10.1145\/976571.976576"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/s10990-006-8745-7","volume":"19","author":"M. Norrish","year":"2006","unstructured":"Norrish, M.: Mechanising \u03bb-calculus using a classical first order theory of terms with permutations. Higher-Order and Symbolic Computation\u00a019, 169\u2013195 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-22863-6_22","volume-title":"Interactive Theorem Proving","author":"M. Norrish","year":"2011","unstructured":"Norrish, M.: Mechanised Computability Theory. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 297\u2013311. Springer, Heidelberg (2011)"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"183","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal Logic, A First Order Theory of Names and Binding. Information and Computation\u00a0183, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"9_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/11532231_4","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Urban","year":"2005","unstructured":"Urban, C., Tasson, C.: Nominal Techniques in Isabelle\/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 38\u201353. Springer, Heidelberg (2005)"},{"key":"9_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/11814771_41","volume-title":"Automated Reasoning","author":"C. Urban","year":"2006","unstructured":"Urban, C., Berghofer, S.: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 498\u2013512. Springer, Heidelberg (2006)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Urban, C., Cheney, J., Berghofer, S.: Mechanizing the Metatheory of LF. In: Proc.\u00a0of the 23rd LICS Symposium, pp. 45\u201356 (2008)","DOI":"10.1109\/LICS.2008.29"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-19718-5_25","volume-title":"Programming Languages and Systems","author":"C. Urban","year":"2011","unstructured":"Urban, C., Kaliszyk, C.: General Bindings and Alpha-Equivalence in Nominal Isabelle. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 480\u2013500. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25379-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,14]],"date-time":"2024-04-14T17:44:53Z","timestamp":1713116693000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25379-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253782","9783642253799"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25379-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}