{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:40Z","timestamp":1779836740150,"version":"3.53.1"},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":6247,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1991,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Quest is a programming language based on impredicative type quantifiers and subtyping within a three-level structure of kinds, types and type operators, and values.<\/jats:p>\n                  <jats:p>The semantics of Quest is rather challenging. In particular, difficulties arise when we try to model simultaneously features such as contravariant function spaces, record types, subtyping, recursive types and fixpoints.<\/jats:p>\n                  <jats:p>In this paper we describe in detail the type inference rules for Quest, and give them meaning using a partial equivalence relation model of types. Subtyping is interpreted as in previous work by Bruce and Longo (1989), but the interpretation of some aspects \u2013 namely subsumption, power kinds, and record subtyping \u2013 is novel. The latter is based on a new encoding of record types.<\/jats:p>\n                  <jats:p>We concentrate on modelling quantifiers and subtyping; recursion is the subject of current work.<\/jats:p>","DOI":"10.1017\/s0956796800000198","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:14:25Z","timestamp":1226056465000},"page":"417-458","source":"Crossref","is-referenced-by-count":51,"title":["A semantic basis for Quest"],"prefix":"10.1017","volume":"1","author":[{"given":"Luca","family":"Cardelli","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giuseppe","family":"Longo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800000198_ref027","doi-asserted-by":"crossref","unstructured":"Hyland M. 1982. The effective topos. In Troelstra A. and Van Dalen (editors), The Brower Symposium, North-Holland.","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"S0956796800000198_ref005","unstructured":"Asperti A. and Martini S. 1989. Categorical models of polymorphism. Information and Computation (to appear)."},{"key":"S0956796800000198_ref024","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19800261902"},{"key":"S0956796800000198_ref019","unstructured":"Fairbairn J. 1989. Some types with inclusion properties in \u2200, \u2192, \u03bc. Technical Report No. 171, University of Cambridge Computer Laboratory, UK."},{"key":"S0956796800000198_ref020","unstructured":"Feferman S. 1987. Weyl Vindicated: Das Kontinuum, 70 Years Later. Preprint, Stanford University. Proc. Cesena Conf. on Logic and Philosophy of Science (to appear)."},{"key":"S0956796800000198_ref018","unstructured":"Ehrhard T. 1988. A categorical semantics of constructions. Proc. 3rd Annual Symposium on Logic in Computer Science, Edinburgh, UK."},{"key":"S0956796800000198_ref008","unstructured":"Breazu-Tannen V. , Coquand T. , Gunter C. and Scedrov A. 1989. Inheritance and explicit coercion. Proc. Fourth Annual Symposium on Logic in Computer Science."},{"key":"S0956796800000198_ref014","unstructured":"Cardelli L. and Mitchell J. C. 1989. Operations on records. Proc. Fifth Conference on Mathematical Foundations of Programming Language Semantics, New Orleans, USA (to appear in Mathematical Structures in Computer Science, 1.)"},{"key":"S0956796800000198_ref013","unstructured":"Cardelli L. , Donahue J. , Glassman L. , Jordan M. , Kalsow B. and Nelson G. 1988. Modula-3 report. Research Report n.31, DEC Systems Research Center (September 1988)."},{"key":"S0956796800000198_ref009","article-title":"Modest models of records, inheritance and bounded quantification","volume":"87","author":"Bruce","year":"1989","journal-title":"Information and Computation"},{"key":"S0956796800000198_ref023","unstructured":"Girard J.-Y. 1972. Interpretation Fonctionelle et \u00c9limination des Coupures dans l'Arithm\u00e9tique d'Ordre Sup\u00e9rieur. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 Paris VII, France."},{"key":"S0956796800000198_ref034","unstructured":"Mitchell J. C. 1986. A type-inference approach to reduction properties and semantics of polymorphic expressions. ACM Conf. LISP and Functional Programming, Boston, USA, 308\u2013319."},{"key":"S0956796800000198_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90007-7"},{"key":"S0956796800000198_ref003","volume-title":"Formal theories of inheritance for typed functional languages","author":"Amadio","year":"1989"},{"key":"S0956796800000198_ref035","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"S0956796800000198_ref037","volume-title":"Proc. Workshop on Database Programming Languages","author":"Ohori","year":"1987"},{"key":"S0956796800000198_ref039","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. 1984. Polymorphism is not set-theoretic. Symposium on Semantics of Data Types, Volume 173 of Lecture Notes in Computer Science,Springer-Verlag.","DOI":"10.1007\/3-540-13346-1_7"},{"key":"S0956796800000198_ref007","volume-title":"The lambda calculus; its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"S0956796800000198_ref028","volume-title":"Some aspects of impredicativity: notes on Weyl's philosophy of mathematics and today's Type Theory","author":"Longo","year":"1988"},{"key":"S0956796800000198_ref041","unstructured":"Scedrov A. A Guide to Polymorphic Types. CIME Lectures Montecatini Terme, June, (revised version)."},{"key":"S0956796800000198_ref010","doi-asserted-by":"crossref","unstructured":"Carboni A. , Freyd P. J. and Scedrov A. 1987. A categorical approach to realizability and polymorphic types. Proc. Third Symposium on Mathematical Foundations of Programming Language Semantics, New Orleans, USA (to appear).","DOI":"10.1007\/3-540-19020-1_2"},{"key":"S0956796800000198_ref031","doi-asserted-by":"crossref","unstructured":"Martini S. 1988. Bounded quantifiers have interval models. ACM Conf. Lisp and Functional Programming Languages, Snowbird, USA.","DOI":"10.1145\/62678.62699"},{"key":"S0956796800000198_ref012","volume-title":"Typeful programming","author":"Cardelli","year":"1989"},{"key":"S0956796800000198_ref025","article-title":"A small complete category","volume":"40","author":"Hyland","year":"1987","journal-title":"Annals of Pure and Applied Logic"},{"key":"S0956796800000198_ref001","unstructured":"Abadi M. and Plotkin G. D. 1990. A Per model of polymorphism and recursive types. Proc. Fifth Annual Symposium on Logic in Computer Science."},{"key":"S0956796800000198_ref016","volume-title":"Proc. POPL'90","author":"Cook","year":"1990"},{"key":"S0956796800000198_ref015","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S0956796800000198_ref040","unstructured":"Rosolini G. 1986. Continuity and effectiveness in Topoi. DPhil. Thesis, Oxford University, UK."},{"key":"S0956796800000198_ref006","volume-title":"Proc. Programming Institute on Logical Foundations of Functional Programming","author":"Bainbridge","year":"1987"},{"key":"S0956796800000198_ref004","volume-title":"Categories, Types and Structures: an introduction to category theory for the working computer scientist","author":"Asperti","year":"1991"},{"key":"S0956796800000198_ref029","unstructured":"Longo G. and Moggi E. 1988. Constructive Natural Deduction and its \u201c\u03c9-Set\u201d interpretation. CMU report CS-88-131, Mathematical Structures in C.S., 1 no. 2, 1991."},{"key":"S0956796800000198_ref026","volume-title":"Categories in Computer Science and Logic (Proc. Boulder '87)","author":"Hyland","year":"1987"},{"key":"S0956796800000198_ref042","volume-title":"Lecture Notes in Mathematics","author":"Troelstra","year":"1973"},{"key":"S0956796800000198_ref043","unstructured":"Wand M. Type inference for record concatenation and multiple inheritance. Proc. Fourth Annual Symposium on Logic in Computer Science."},{"key":"S0956796800000198_ref032","unstructured":"Meseguer J. 1988. Relating Models of Polymorphism. SRI-CSL-88-13, October, SRI Projects 2316, 4415 and 6729, SRI International."},{"key":"S0956796800000198_ref022","unstructured":"Freyd P. J. , Mulry P. , Rosolini G. and Scott D. 1990. Domains in Per. Proc. 5th Annual Symposium on Logic in Computer Science."},{"key":"S0956796800000198_ref033","doi-asserted-by":"crossref","unstructured":"Mitchell J. C. 1984. Coercion and type inference. Proc. POPL '84.","DOI":"10.1145\/800017.800529"},{"key":"S0956796800000198_ref036","doi-asserted-by":"crossref","unstructured":"Mitchell J. C. and Plotkin G. D. 1985. Abstract types have existential type. Proc. POPL '85.","DOI":"10.1145\/318593.318606"},{"key":"S0956796800000198_ref038","doi-asserted-by":"crossref","unstructured":"Pitts A. 1987. Polymorphism is Set theoretic, constructively. Symposium on Category Theory and Computer Science, SLNCS 283, Edinburgh, UK.","DOI":"10.1007\/3-540-18508-9_18"},{"key":"S0956796800000198_ref030","volume-title":"ECC, an Extended Calculus of Constructions","author":"Luo","year":"1988"},{"key":"S0956796800000198_ref017","unstructured":"Curien P. L. and Ghelli G. 1990. Coherence of subsumption, Mathematical Structures in Computer Science, 1 no. 3."},{"key":"S0956796800000198_ref021","first-page":"151","article-title":"Polymorphic typed lambda-calculi in a type-free axiomatic framework","author":"Feferman","year":"1988","journal-title":"J. ACM"},{"key":"S0956796800000198_ref002","unstructured":"Amadio R. 1989 a. Recursion over realizability structures. Information and Computation, 1991."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800000198","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:16Z","timestamp":1779834976000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800000198\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,10]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1991,10]]}},"alternative-id":["S0956796800000198"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800000198","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,10]]}}}