{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:56Z","timestamp":1759639076208},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642229527"},{"type":"electronic","value":"9783642229534"}],"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-22953-4_14","type":"book-chapter","created":{"date-parts":[[2011,8,17]],"date-time":"2011-08-17T12:28:08Z","timestamp":1313584088000},"page":"160-172","source":"Crossref","is-referenced-by-count":0,"title":["Principal Types for Nominal Theories"],"prefix":"10.1007","author":[{"given":"Elliot","family":"Fairweather","sequence":"first","affiliation":[]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[]},{"given":"Murdoch J.","family":"Gabbay","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1006\/inco.1996.2617","volume":"133","author":"S. Bakel van","year":"1997","unstructured":"van Bakel, S., Fern\u00e1ndez, M.: Normalization results for typeable rewrite systems. Information and Computation\u00a0133(2), 73\u2013116 (1997)","journal-title":"Information and Computation"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/S0304-3975(96)80706-7","volume":"170","author":"F. Barbanera","year":"1996","unstructured":"Barbanera, F., Fern\u00e1ndez, M.: Intersection type assignment systems with higher-order algebraic rewriting. Theoretical Computer Science\u00a0170, 173\u2013207 (1996)","journal-title":"Theoretical Computer Science"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1002\/malq.19740201902","volume":"20","author":"H.P. Barendregt","year":"1974","unstructured":"Barendregt, H.P.: Pairing without conventional constraints. Zeitschrift f\u00fcr mathematischen Logik und Grundlagen der Mathematik\u00a020, 289\u2013306 (1974)","journal-title":"Zeitschrift f\u00fcr mathematischen Logik und Grundlagen der Mathematik"},{"issue":"4","key":"14_CR4","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1983","unstructured":"Barendregt, H.P., Coppo, M., DezaniCiancaglini, M.: A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic\u00a048(4), 931\u2013940 (1983)","journal-title":"Journal of Symbolic Logic"},{"key":"14_CR5","unstructured":"Calv\u00e9s, C.: Complexity and implementation of nominal algorithms, Ph.D. thesis, King\u2019s College London (2010)"},{"key":"14_CR6","unstructured":"Clouston, R.: Closed terms (unpublished notes) (2007), http:\/\/users.cecs.anu.edu.au\/~rclouston\/closedterms.pdf"},{"key":"14_CR7","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/582153.582176","volume-title":"Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1982)","author":"L. Damas","year":"1982","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1982), pp. 207\u2013212. ACM, New York (1982)"},{"key":"14_CR8","unstructured":"Fairweather, E.: Principal types for nominal terms: tool description, http:\/\/www.inf.kcl.ac.uk\/pg\/elliotf\/research"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-74464-1_9","volume-title":"Types for Proofs and Programs","author":"M. Fern\u00e1ndez","year":"2007","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Curry-style types for nominal terms. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 125\u2013139. Springer, Heidelberg (2007), http:\/\/www.gabbay.org.uk\/papers.html#curstn"},{"issue":"6","key":"14_CR10","doi-asserted-by":"publisher","first-page":"917","DOI":"10.1016\/j.ic.2006.12.002","volume":"205","author":"M. Fern\u00e1ndez","year":"2007","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Nominal rewriting (journal version). Information and Computation\u00a0205(6), 917\u2013965 (2007), http:\/\/www.gabbay.org.uk\/papers.html#nomr-jv","journal-title":"Information and Computation"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Closed nominal rewriting and efficiently computable nominal algebra equality. In: Proceedings of the 5th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2010) (2010), http:\/\/www.gabbay.org.uk\/papers.html#clonre","DOI":"10.4204\/EPTCS.34.5"},{"key":"14_CR12","first-page":"108","volume-title":"Proceedings of the 6th ACM SIGPLAN symposium on Principles and Practice of Declarative Programming (PPDP 2004)","author":"M. Fern\u00e1ndez","year":"2004","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J., Mackie, I.: Nominal Rewriting Systems. In: Proceedings of the 6th ACM SIGPLAN symposium on Principles and Practice of Declarative Programming (PPDP 2004), pp. 108\u2013119. ACM Press, New York (2004), http:\/\/www.gabbay.org.uk\/papers.html#nomr"},{"key":"14_CR13","volume-title":"Handbook of Philosphical Logic","author":"M.J. Gabbay","year":"2011","unstructured":"Gabbay, M.J.: Nominal terms and nominal logics: from foundations to meta-mathematics. In: Handbook of Philosphical Logic, vol.\u00a017, Kluwer, Dordrecht (2011), http:\/\/www.gabbay.org.uk\/papers.html#nomtnl"},{"issue":"6","key":"14_CR14","doi-asserted-by":"publisher","first-page":"1455","DOI":"10.1093\/logcom\/exp033","volume":"19","author":"M.J. Gabbay","year":"2009","unstructured":"Gabbay, M.J., Mathijssen, A.: Nominal universal algebra: equational logic with names and binding. Journal of Logic and Computation\u00a019(6), 1455\u20131508 (2009), http:\/\/www.gabbay.org.uk\/papers.html#nomuae","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"14_CR15","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1093\/logcom\/exp049","volume":"20","author":"M.J. Gabbay","year":"2010","unstructured":"Gabbay, M.J., Mathijssen, A.: A nominal axiomatisation of the lambda-calculus. Journal of Logic and Computation\u00a020(2), 501\u2013531 (2010), http:\/\/www.gabbay.org.uk\/papers.html#nomalc","journal-title":"Journal of Logic and Computation"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: The system F of variable types, fifteen years later. Theoretical Computer Science\u00a045 (1986)","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"14_CR17","volume-title":"The Java language specification","author":"J. Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java language specification. Addison-Wesley, Reading (1996)"},{"key":"14_CR18","first-page":"159","volume-title":"Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010)","author":"A.M. Pitts","year":"2010","unstructured":"Pitts, A.M.: Nominal system T. In: Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), pp. 159\u2013170. ACM Press, New York (2010)"},{"key":"14_CR19","first-page":"263","volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (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: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), vol.\u00a038, pp. 263\u2013274. ACM Press, New York (2003), http:\/\/www.gabbay.org.uk\/papers.html#frepbm"},{"issue":"1-3","key":"14_CR20","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-3), 473\u2013497 (2004), http:\/\/www.gabbay.org.uk\/papers.html#nomu-jv","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Computation Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22953-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,22]],"date-time":"2020-06-22T10:08:19Z","timestamp":1592820499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22953-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642229527","9783642229534"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22953-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}