{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:52:59Z","timestamp":1776891179292,"version":"3.51.2"},"reference-count":43,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"2","license":[{"start":{"date-parts":[[2016,8,10]],"date-time":"2016-08-10T00:00:00Z","timestamp":1470787200000},"content-version":"unspecified","delay-in-days":9263,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1991,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Programming languages often come with type systems. Some of these are simple, others are sophisticated. As a stylistic representation of types in programming languages several versions of typed lambda calculus are studied. During the last 20 years many of these systems have appeared, so there is some need of classification. Working towards a taxonomy, Barendregt (1991) gives a fine-structure of the theory of constructions (Coquand and Huet 1988) in the form of a canonical cube of eight type systems ordered by inclusion. Berardi (1988) and Terlouw (1988) have independently generalized the method of constructing systems in the \u03bb-cube. Moreover, Berardi (1988, 1990) showed that the generalized type systems are flexible enough to describe many logical systems. In that way the well-known\n                    <jats:italic>propositions-as-types<\/jats:italic>\n                    interpretation obtains a nice canonical form.\n                  <\/jats:p>","DOI":"10.1017\/s0956796800020025","type":"journal-article","created":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T06:00:14Z","timestamp":1531116014000},"page":"125-154","source":"Crossref","is-referenced-by-count":132,"title":["Introduction to generalized type systems"],"prefix":"10.46298","volume":"1","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2016,8,10]]},"reference":[{"key":"S0956796800020025_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0956796800020025_ref012","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S0956796800020025_ref035","volume-title":"Natural Deduction","author":"Prawitz","year":"1965"},{"key":"S0956796800020025_ref005","unstructured":"Barendregt H. P. and Dekkers W. 1990. Typed lambda calculi."},{"key":"S0956796800020025_ref006","unstructured":"Barendsen E. 1989. Representation of Logic, Data Types and Recursive Functions in Typed Lambda Calculi. Masters thesis, University of Nijmegen, Netherlands."},{"key":"S0956796800020025_ref029","volume-title":"Constructive Natural Deduction and its Modest Interpretation","author":"Longo","year":"1988"},{"key":"S0956796800020025_ref031","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796800020025_ref024","unstructured":"Girard J.-Y. 1972. Interpr\u00e9tation Fonctionelle et \u00c9limination des Coupures dans l' Arithm\u00e9tique d'Ordre Sup\u00e9rieur. Th\u00e8se de Doctorat d'\u00c9tat, Universit\u00e9 Paris VII, France."},{"key":"S0956796800020025_ref008","unstructured":"Berardi S. 1988. Personal communication."},{"key":"S0956796800020025_ref027","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S0956796800020025_ref039","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-2913-1"},{"key":"S0956796800020025_ref017","unstructured":"van Daalen D. 1980. The Language Theory of AUTOMATH. PhD. thesis, Technical University Eindhoven, Netherlands."},{"key":"S0956796800020025_ref001","volume-title":"The Lambda Calculus; Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S0956796800020025_ref011","first-page":"580","volume-title":"To H. B. Curry: Essays on Combinatory logic, Lambda Calculus and Formalism","author":"de Bruijn","year":"1980"},{"key":"S0956796800020025_ref043","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0029530"},{"key":"S0956796800020025_ref014","volume-title":"Proc. Ecole de Printemps du LITP","author":"Coquand","year":"1989"},{"key":"S0956796800020025_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02382-2"},{"key":"S0956796800020025_ref037","first-page":"408","volume-title":"Proc. Colloque sur la Programmation","volume":"19","author":"Reynolds","year":"1974"},{"key":"S0956796800020025_ref034","volume-title":"Een opmerking over intuitionistische logica","author":"Peremans","year":"1949"},{"key":"S0956796800020025_ref020","unstructured":"Geuvers H. 1988. The Interpretation of Logics in Type Systems. Master thesis, University of Nijmegen, Netherlands."},{"key":"S0956796800020025_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"S0956796800020025_ref041","unstructured":"Terlouw J. 1988. Personal communication."},{"key":"S0956796800020025_ref004","first-page":"1","volume-title":"Proc. European Symposium on Programming","author":"Barendregt","year":"1990"},{"key":"S0956796800020025_ref038","first-page":"145","volume-title":"Lecture Notes in Computer Science","volume":"185","author":"Reynolds","year":"1985"},{"key":"S0956796800020025_ref032","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802035"},{"key":"S0956796800020025_ref023","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","article-title":"A modular proof of strong normalization for the theory of constructions","volume":"1","author":"Geuvers","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"S0956796800020025_ref010","first-page":"29","volume-title":"Lecture Notes in Mathematics","volume":"125","author":"de Bruijn","year":"1970"},{"key":"S0956796800020025_ref042","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-15975-4_26","volume-title":"Functional Programming Languages and Computer Architecture. Lecture Notes in Computer Science","volume":"201","author":"Turner","year":"1985"},{"key":"S0956796800020025_ref033","doi-asserted-by":"publisher","DOI":"10.2307\/2266682"},{"key":"S0956796800020025_ref040","unstructured":"Swaen M. D. G. 1989. Weak and Strong Sum-elimination in Institutionistic Type Theory. PhD. thesis, University of Amsterdam, Netherlands."},{"key":"S0956796800020025_ref022","volume-title":"Type systems for higher order logic","author":"Geuvers","year":"1990"},{"key":"S0956796800020025_ref019","volume-title":"Relationship between logic and type system","author":"Fujita","year":"1989"},{"key":"S0956796800020025_ref009","unstructured":"Berardi S. 1990. Type Dependence and Constructive Mathematics. PhD thesis, Mathematical Institute, Torino, Italy."},{"key":"S0956796800020025_ref007","volume-title":"Conservativity of \u03bbP over PRED","author":"Barendsen","year":"1989"},{"key":"S0956796800020025_ref021","volume-title":"Theory of constructions is not conservative over higher order logic","author":"Geuvers","year":"1989"},{"key":"S0956796800020025_ref016","volume-title":"Combinatory logic","author":"Curry","year":"1958"},{"key":"S0956796800020025_ref036","volume-title":"Strictness analysis for a language with polymorphic and recursive types (preprint)","author":"Renardel de Lavalette","year":"1987"},{"key":"S0956796800020025_ref030","volume-title":"A construction of the provable wellorderings of the theory of species","author":"Martin-L\u00f6f","year":"1970"},{"key":"S0956796800020025_ref013","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0956796800020025_ref026","first-page":"194","volume-title":"Proc. 2nd Symp. Logic in Computer Science","author":"Harper","year":"1987"},{"key":"S0956796800020025_ref028","first-page":"279","volume-title":"Logic and Computer Science","author":"Leivant","year":"1989"},{"key":"S0956796800020025_ref002","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1991"},{"key":"S0956796800020025_ref003","first-page":"122","volume-title":"Lecture Notes in Computer Science","volume":"224","author":"Barendregt","year":"1985"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800020025","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:17:47Z","timestamp":1776889067000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800020025\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,4]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1991,4]]}},"alternative-id":["S0956796800020025"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800020025","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,4]]}}}