A semantic basis for Quest

Publisher Website
Google Scholar
Abstract
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.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.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 – namely subsumption, power kinds, and record subtyping – is novel. The latter is based on a new encoding of record types.We concentrate on modelling quantifiers and subtyping; recursion is the subject of current work.

This publication has 13 references indexed in Scilit: