{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T10:49:08Z","timestamp":1649155748723},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":8777,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1990,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper discusses six formalization techniques, of varying strengths, for extending a formal system based on traditional mathematical logic. The purpose of these formalization techniques is to simulate the introduction of new syntactic constructs, along with associated semantics for them. We show that certain techniques (among the six) subsume others. To illustrate sharpness, we also consider a selection of constructs and show which techniques can and cannot be used to introduce them. The six studied techniques were selected on the basis of actual practice in logic and computing. They do not form an exhaustive list.<\/jats:p>","DOI":"10.2307\/2274964","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:33:48Z","timestamp":1146940428000},"page":"220-243","source":"Crossref","is-referenced-by-count":0,"title":["On the formalization of semantic conventions"],"prefix":"10.1017","volume":"55","author":[{"given":"James G.","family":"Williams","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200026530_ref021","volume-title":"Formally grounded software reasoning systems: theory and requirements","author":"Williams","year":"1987"},{"key":"S0022481200026530_ref020","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380090105"},{"key":"S0022481200026530_ref018","volume-title":"The mathematics of m-Verdi","author":"Saaltink","year":"1986"},{"key":"S0022481200026530_ref008","volume-title":"Combinatory logic","volume":"I","author":"Curry","year":"1958"},{"key":"S0022481200026530_ref015","volume-title":"The logical basis for computer programming","author":"Manna","year":"1985"},{"key":"S0022481200026530_ref013","volume-title":"Set theory: an introduction to independence proofs","author":"Kunen","year":"1983"},{"key":"S0022481200026530_ref019","volume-title":"Denotational semantics: the Scott-Strachey approach to programming language theory","author":"Stoy","year":"1977"},{"key":"S0022481200026530_ref003","first-page":"2","volume-title":"Proceedings of the 1986 symposium on logic programming (Salt Lake City, Utah)","author":"Bledsoe","year":"1986"},{"key":"S0022481200026530_ref017","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093891710"},{"key":"S0022481200026530_ref010","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"S0022481200026530_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15187-7"},{"key":"S0022481200026530_ref012","volume-title":"Set theory","author":"Jech","year":"1978"},{"key":"S0022481200026530_ref004","volume-title":"A computational logic","author":"Boyer","year":"1979"},{"key":"S0022481200026530_ref006","doi-asserted-by":"publisher","DOI":"10.1145\/1012497.1012499"},{"key":"S0022481200026530_ref014","first-page":"88","volume-title":"Polish logic 1920\u20131939","author":"\u0141ukasiewicz","year":"1967"},{"key":"S0022481200026530_ref001","volume-title":"Structure and interpretation of computer programs","author":"Abelson","year":"1985"},{"key":"S0022481200026530_ref009","volume-title":"A mathematical introduction to logic","author":"Enderton","year":"1972"},{"key":"S0022481200026530_ref016","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1959-0104609-5"},{"key":"S0022481200026530_ref005","first-page":"95","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Control"},{"key":"S0022481200026530_ref011","volume-title":"The denotational description of programming languages, an introduction","author":"Gordon","year":"1970"},{"key":"S0022481200026530_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-1138-9_13"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200026530","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T17:51:58Z","timestamp":1558201918000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200026530\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,3]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1990,3]]}},"alternative-id":["S0022481200026530"],"URL":"https:\/\/doi.org\/10.2307\/2274964","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,3]]}}}