{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:02Z","timestamp":1776316922597,"version":"3.50.1"},"reference-count":12,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":11059,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1983,12]]},"abstract":"<jats:p>In [6, p. 317] Curry described a formal system assigning types to terms of the type-free <jats:italic>\u03bb<\/jats:italic>-calculus. In [11] Scott gave a natural semantics for this type assignment and asked whether a completeness result holds.<\/jats:p><jats:p>Inspired by [4] and [5] we extend the syntax and semantics of the Curry types in such a way that filters in the resulting type structure form a domain in the sense of Scott [12]. We will show that it is possible to turn the domain of types into a <jats:italic>\u03bb<\/jats:italic>-model, among other reasons because all <jats:italic>\u03bb<\/jats:italic>-terms possess a type. This model gives the completeness result for the extended system. By a conservativity result the completeness for Curry's system follows.<\/jats:p><jats:p>Independently Hindley [8], [9] has proved both completeness results using term models. His method of proof is in some sense dual to ours.<\/jats:p><jats:p>For <jats:italic>\u03bb<\/jats:italic>-calculus notation see [1].<\/jats:p>","DOI":"10.2307\/2273659","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:06:05Z","timestamp":1146953165000},"page":"931-940","source":"Crossref","is-referenced-by-count":328,"title":["A filter lambda model and the completeness of type assignment"],"prefix":"10.1017","volume":"48","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]},{"given":"Mario","family":"Coppo","sequence":"additional","affiliation":[]},{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200037324_ref003","volume-title":"Automata, languages and programming","author":"Coppo"},{"key":"S0022481200037324_ref007","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19800261902"},{"key":"S0022481200037324_ref002","unstructured":"BEN-Yelles C. B. , Type-assignment in the lambda-calculus; Syntax and semantics, Doctoral Thesis, University College of Swansea, 1979."},{"key":"S0022481200037324_ref006","volume-title":"Combinatory logic. I","author":"Curry","year":"1958"},{"key":"S0022481200037324_ref001","volume-title":"The lambda calculus, its syntax and semantics","author":"Barendregt","year":"1981"},{"key":"S0022481200037324_ref011","first-page":"369","volume-title":"\u03bb-calculus and computer science theory","volume":"37","author":"Scott","year":"1975"},{"key":"S0022481200037324_ref010","volume-title":"Natural deduction, a proof-theoretical study","author":"Prawitz","year":"1965"},{"key":"S0022481200037324_ref004","first-page":"535","volume-title":"To H.B. Curry, Essays in combinatory logic, lambda-calculus and formalism","author":"Coppo","year":"1980"},{"key":"S0022481200037324_ref012","volume-title":"Lectures on a mathematical theory of computation","author":"Scott","year":"1980"},{"key":"S0022481200037324_ref005","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"S0022481200037324_ref008","volume-title":"Theoretical Computer Science","author":"Hindley"},{"key":"S0022481200037324_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_15"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200037324","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T22:12:26Z","timestamp":1558649546000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200037324\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1983,12]]},"references-count":12,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1983,12]]}},"alternative-id":["S0022481200037324"],"URL":"https:\/\/doi.org\/10.2307\/2273659","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1983,12]]}}}