{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:12Z","timestamp":1760202552071},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540734437"},{"type":"electronic","value":"9783540734451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73445-1_12","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T06:32:08Z","timestamp":1183444328000},"page":"162-176","source":"Crossref","is-referenced-by-count":10,"title":["A Formal Calculus for Informal Equality with Binding"],"prefix":"10.1007","author":[{"given":"Murdoch J.","family":"Gabbay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aad","family":"Mathijssen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Barendregt, H.P.: The Lambda Calculus: its Syntax and Semantics. North-Holland (revised edn.)"},{"key":"12_CR2","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic. vol.\u00a01, North Holland (1958)"},{"key":"12_CR3","unstructured":"Henkin, L., Monk, J.D., Tarski, A.: Cylindric Algebras, Parts I and II, North Holland (1971, 1985)"},{"issue":"2","key":"12_CR4","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1016\/0304-3975(92)90310-C","volume":"100","author":"K. Meinke","year":"1992","unstructured":"Meinke, K.: Universal algebra in higher types. Theoretical Computer Science\u00a0100(2), 385\u2013417 (1992)","journal-title":"Theoretical Computer Science"},{"key":"12_CR5","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1093\/oso\/9780198537465.003.0004","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"D. Leivant","year":"1994","unstructured":"Leivant, D.: Higher order logic. In: Gabbay, D., Hogger, C., Robinson, J. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02, pp. 229\u2013322. Oxford University Press, Oxford, UK (1994)"},{"key":"12_CR6","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Nominal rewriting. Information and Computation (in press)"},{"key":"12_CR7","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Curry-style types for nominal rewriting. In: TYPES\u201906 (2006)"},{"issue":"3\u20135","key":"12_CR8","first-page":"341","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(3\u20135), 341\u2013363 (2001)","journal-title":"Formal Aspects of Computing"},{"issue":"1\u20133","key":"12_CR9","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\u20133), 473\u2013497 (2004)","journal-title":"Theoretical Computer Science"},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1145\/1140335.1140359","volume-title":"PPDP \u201906","author":"M.J. Gabbay","year":"2006","unstructured":"Gabbay, M.J., Mathijssen, A.: One-and-a-halfth-order logic. In: PPDP \u201906. Proc. of the 8th ACM SIGPLAN symposium on Principles and Practice of Declarative Programming, pp. 189\u2013200. ACM Press, New York (2006)"},{"key":"12_CR11","volume-title":"Proofs and types","author":"J.Y. Girard","year":"1989","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and types. Cambridge University Press, Cambridge (1989)"},{"key":"12_CR12","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1016\/B978-044482830-9\/50026-6","volume-title":"Handbook of Process Algebra","author":"J. Parrow","year":"2001","unstructured":"Parrow, J.: An introduction to the pi-calculus. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 479\u2013543. Elsevier, Amsterdam (2001)"},{"key":"12_CR13","first-page":"1","volume-title":"Handbook of Philosophical Logic","author":"W. Hodges","year":"2001","unstructured":"Hodges, W.: Elementary predicate logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol.\u00a01, pp. 1\u2013131. Kluwer Academic Publishers, Dordrecht (2001)","edition":"2"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/11921240_14","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"M.J. Gabbay","year":"2006","unstructured":"Gabbay, M.J., Mathijssen, A.: Capture-avoiding substitution as a nominal algebra. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 198\u2013212. Springer, Heidelberg (2006)"},{"key":"12_CR15","unstructured":"Gabbay, M.J.: Fresh logic. Journal of Logic and Computation, 2006 (in press)"},{"issue":"3","key":"12_CR16","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning\u00a05(3), 363\u2013397 (1989)","journal-title":"Journal of Automated Reasoning"},{"issue":"34","key":"12_CR17","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"5","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae\u00a05(34), 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1145\/53990.54010","volume-title":"PLDI \u201988","author":"F. Pfenning","year":"1988","unstructured":"Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI \u201988. Proc. of the ACM SIGPLAN 1988 conf. on Programming Language design and Implementation, pp. 199\u2013208. ACM Press, New York (1988)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Miculan, M.: Developing (meta)theory of lambda-calculus in the theory of contexts. ENTCS 1(58) (2001)","DOI":"10.1016\/S1571-0661(04)00278-6"},{"key":"12_CR20","series-title":"Lecture Notes in Artificial Intelligence","first-page":"202","volume-title":"CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE-16. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"issue":"2","key":"12_CR21","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(2), 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/944705.944729","volume-title":"ICFP 2003","author":"M.R. Shinwell","year":"2003","unstructured":"Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programming with binders made simple. In: ICFP 2003. Eighth ACM SIGPLAN Int\u2019l Conf. on Functional Programming, Uppsala, Sweden, pp. 263\u2013274. ACM Press, New York (2003)"},{"key":"12_CR23","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the working programmer","author":"L.C. Paulson","year":"1996","unstructured":"Paulson, L.C.: ML for the working programmer, 2nd edn. Cambridge University Press, Cambridge (1996)","edition":"2"},{"issue":"3","key":"12_CR24","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1016\/j.tcs.2003.10.041","volume":"322","author":"L.C. Lu\u00eds Caires","year":"2004","unstructured":"Lu\u00eds Caires, L.C.: A spatial logic for concurrency (part II). Theoretical Computer Science\u00a0322(3), 517\u2013565 (2004)","journal-title":"Theoretical Computer Science"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/11417170_8","volume-title":"Typed Lambda Calculi and Applications","author":"N. Benton","year":"2005","unstructured":"Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 86\u2013101. Springer, Heidelberg (2005)"},{"key":"12_CR26","unstructured":"Cheney, J., Urban, C.: System description: Alpha-Prolog, a fresh approach to logic programming modulo alpha-equivalence. In: de Valencia, U.P. (ed.) Proc. 17th Int. Workshop on Unification, UNIF\u201903, 15\u201319 (2003)"},{"key":"12_CR27","first-page":"361","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361\u2013386. Academic Press, London (1990)"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-45685-6_2","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Huet","year":"2002","unstructured":"Huet, G.: Higher order unification 30 years later. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 3\u201312. Springer, Heidelberg (2002)"},{"key":"12_CR29","first-page":"223","volume":"172","author":"R.A. Clouston","year":"2007","unstructured":"Clouston, R.A., Pitts, A.M.: Nominal equational logic. ENTCS\u00a0172, 223\u2013257 (2007)","journal-title":"ENTCS"},{"key":"12_CR30","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0304-3975(97)00170-9","volume":"211","author":"Y. Sun","year":"1999","unstructured":"Sun, Y.: An algebraic generalization of frege structures - binding algebras. Theoretical Computer Science\u00a0211, 189\u2013232 (1999)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"12_CR31","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0304-3975(00)00059-1","volume":"249","author":"A. Salibra","year":"2000","unstructured":"Salibra, A.: On the algebraic models of lambda calculus. Theoretical Computer Science\u00a0249(1), 197\u2013240 (2000)","journal-title":"Theoretical Computer Science"},{"key":"12_CR32","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-8130-3","volume-title":"A Course in Universal Algebra","author":"S. Burris","year":"1981","unstructured":"Burris, S., Sankappanavar, H.: A Course in Universal Algebra. Springer, Heidelberg (1981)"},{"key":"12_CR33","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-94-017-0452-6_3","volume-title":"Handbook of Philosophical Logic","author":"H. Andr\u00e9ka","year":"2001","unstructured":"Andr\u00e9ka, H., N\u00e9meti, I., Sain, I.: Algebraic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., pp. 133\u2013249. Kluwer Academic Publishers, Dordrecht (2001)","edition":"2"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Blok, W.J., Pigozzi, D.: Algebraizable logics. Memoirs of the AMS 77(396) (1989)","DOI":"10.1090\/memo\/0396"},{"key":"12_CR35","first-page":"327","volume":"37","author":"H. Barendregt","year":"1998","unstructured":"Barendregt, H., Dekkers, W., Bunder, M.: Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus. Archive f\u00fcr Mathematische Logik\u00a037, 327\u2013341 (1998)","journal-title":"Archive f\u00fcr Mathematische Logik"},{"key":"12_CR36","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/266420.266432","volume-title":"CCS \u201997","author":"M. Abadi","year":"1997","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. In: CCS \u201997. Proc. of the 4th ACM conf, pp. 36\u201347. ACM Press, New York (1997)"},{"key":"12_CR37","unstructured":"Luttik, B.: Choice Quantification in Process Algebra. PhD thesis, University of Amsterdam (2002)"},{"key":"12_CR38","first-page":"375","volume-title":"Lectures on formal methods and performance analysis: first EEF\/Euro summer school on trends in computer science","author":"J.P. Katoen","year":"2002","unstructured":"Katoen, J.P., D\u2019Argenio, P.R.: General distributions in process algebra. In: Lectures on formal methods and performance analysis: first EEF\/Euro summer school on trends in computer science, pp. 375\u2013429. Springer, Heidelberg (2002)"},{"issue":"9","key":"12_CR39","doi-asserted-by":"publisher","first-page":"838","DOI":"10.2307\/2975289","volume":"104","author":"T. Forster","year":"1997","unstructured":"Forster, T.: Quine\u2019s NF, 60 years on. American Mathematical Monthly\u00a0104(9), 838\u2013845 (1997)","journal-title":"American Mathematical Monthly"},{"key":"12_CR40","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1145\/1069774.1069783","volume-title":"PPDP \u201905","author":"M.J. Gabbay","year":"2005","unstructured":"Gabbay, M.J.: A new calculus of contexts. In: PPDP \u201905. Proc. of the 7th ACM SIGPLAN int\u2019l conf. on Principles and Practice of Declarative Programming, pp. 94\u2013105. ACM Press, New York (2005)"},{"key":"12_CR41","unstructured":"Gabbay, M.J.: Hierarchical nominal rewriting. In: LFMTP\u201906: Logical Frameworks and Meta-Languages: Theory and Practice, pp. 32\u201347 (2006)"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73445-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,15]],"date-time":"2024-02-15T18:02:21Z","timestamp":1708020141000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73445-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540734437","9783540734451"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73445-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}