{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T07:51:55Z","timestamp":1757577115314},"reference-count":32,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":5699,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1993,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We extend the definition of natural semantics to include simply typed \u03bb-terms, instead of first-order terms, for representing programs, and to include inference rules for the introduction and discharge of hypotheses and eigenvariables. This extension, which we call <jats:italic>extended natural semantics<\/jats:italic>, affords a higher-level notion of abstract syntax for representing programs and suitable mechanisms for manipulating this syntax. We present several examples of semantic specifications for a simple functional programming language and demonstrate how we achieve simple and elegant manipulations of bound variables in functional programs. All the examples have been implemented and tested in \u03bbProlog, a higher-order logic programming language that supports all of the features of extended natural semantics.<\/jats:p>","DOI":"10.1017\/s0956796800000666","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:13:50Z","timestamp":1226056430000},"page":"123-152","source":"Crossref","is-referenced-by-count":18,"title":["Extended natural semantics"],"prefix":"10.1017","volume":"3","author":[{"given":"John","family":"Hannan","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800000666_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51305-1_13"},{"key":"S0956796800000666_ref031","volume-title":"Natural Deduction","author":"Prawitz","year":"1965"},{"key":"S0956796800000666_ref029","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0956796800000666_ref032","first-page":"403","volume-title":"To H. B. Curry: Essays on Combinatory Logic","author":"Scott","year":"1980"},{"key":"S0956796800000666_ref026","first-page":"199","volume-title":"Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation","volume":"23","author":"Pfenning","year":"1988"},{"key":"S0956796800000666_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"S0956796800000666_ref023","first-page":"28","volume-title":"Proceedings of the ACM Conference on Principles of Programming Languages","author":"Mitchell","year":"1988"},{"key":"S0956796800000666_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)80087-9"},{"key":"S0956796800000666_ref024","first-page":"810","volume-title":"Fifth International Conference and Symposium on Logic Programming","author":"Nadathur","year":"1988"},{"key":"S0956796800000666_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"S0956796800000666_ref016","first-page":"22","volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science","volume":"247","author":"Kahn","year":"1987"},{"key":"S0956796800000666_ref030","volume-title":"A structural approach to operational semantics","author":"Plotkin","year":"1981"},{"key":"S0956796800000666_ref006","unstructured":"Elliott C. and Pfenning F. 1989. eLP, a Common Lisp Implementation of \u03bbProlog."},{"key":"S0956796800000666_ref019","first-page":"379","volume-title":"Proceedings of the IEEE Fourth Symposium on Logic Programming","author":"Miller","year":"1987"},{"key":"S0956796800000666_ref008","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S0956796800000666_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_90"},{"key":"S0956796800000666_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"S0956796800000666_ref011","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185552"},{"key":"S0956796800000666_ref005","first-page":"207","volume-title":"Proceedings of the ACM Conference on Principles of Programming Languages","author":"Damas","year":"1982"},{"key":"S0956796800000666_ref001","doi-asserted-by":"crossref","unstructured":"Borras P. , Cl\u00e9ment D. , Despeyroux T. , Incerpi J. , Kahn G. , Lang B. and Pascual V. 1987. CENTAUR: the system. Technical Report 777, INRIA, (12).","DOI":"10.1145\/64135.65005"},{"key":"S0956796800000666_ref022","volume-title":"The Definition of Standard ML","author":"Milner","year":"1991"},{"key":"S0956796800000666_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013612"},{"key":"S0956796800000666_ref002","first-page":"589","volume-title":"H. B. Curry: Essays on Combinatory Logic","author":"Bruijn","year":"1980"},{"key":"S0956796800000666_ref012","unstructured":"Hannan J. 1991. Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania, (Available as MS-CIS-91-09.)"},{"key":"S0956796800000666_ref013","first-page":"194","article-title":"A framework for defining logics","author":"Harper","year":"1987","journal-title":"Journal of the ACM"},{"key":"S0956796800000666_ref028","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.008"},{"key":"S0956796800000666_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264598"},{"key":"S0956796800000666_ref009","unstructured":"Hannan J. and Miller D. 1988. Enriching a meta-language with higher-order features. Technical Report MS-CIS-88-45, University of Pennsylvania (06)."},{"key":"S0956796800000666_ref021","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"S0956796800000666_ref027","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39186"},{"key":"S0956796800000666_ref003","first-page":"89","volume-title":"Logical Frameworks","author":"Burstall","year":"1991"},{"key":"S0956796800000666_ref004","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319847"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800000666","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T19:28:03Z","timestamp":1557948483000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800000666\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,4]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,4]]}},"alternative-id":["S0956796800000666"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800000666","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,4]]}}}