scientific article; zbMATH DE number 1302055
Our starting point, to which we refer hereafter as type theory, is the formulation of Martin-Löf's set theory using the theory of types as a logical framework. The question that we address is that of the representation of systems of structures such as algebraic systems or abstract data types. In order to provide a general means to this end, we extend type theory with a new mechanism of type formation, namely that of dependent record types. This allows us to form types of tuples in such a manner as to allow any arbitrary set (i.e. not restricted to be among those generated by a fixed repertoire of set forming operations) to be used as a component of tuples of those types. Such types of tuples cannot be formed in the original theory. Moreover, as is well known from the theory of programming languages, a natural notion of inclusion arises between record types. Given two record types \(\rho\) and \(\rho'\), if \(\rho\) contains every label declared in \(\rho'\) (and possibly more) and the types of the common labels are in the inclusion relation then \(\rho\) is included in \(\rho'\); in symbols, \(\rho\sqsubseteq\rho'\). This is justified because then every object of type \(\rho\) is also an object of type \(\rho'\), since it contains components of appropriate types for all the fields specified in \(\rho'\). Our extension contains the form of judgement \(\alpha\sqsubseteq \beta\) expressing that the type \(\alpha\) is included in the type \(\beta\) and corresponding proof rules, which generalize record type inclusion to dependent record types and propagate it to the rest of the types of the language. In the present formulation, no proper inclusion between ground types is allowed. For the entire collection see [Zbl 0899.00026].
- scientific article; zbMATH DE number 814798
- scientific article; zbMATH DE number 3853066
- Dependently typed records in type theory
- scientific article; zbMATH DE number 1187955
- A calculus with recursive types, record concatenation and subtyping
- Pure type systems with subtyping. (Extended abstract)
- Remarks on Martin-Löf's partial type theory
- Martin-Löf's type theory as an open-ended framework
- Subtyping and intersection types revisited
- Extensional constructs in intensional type theory
- Theories as types
- Packaging Mathematical Structures
- Working with Mathematical Structures in Type Theory
- Manifest Fields and Module Mechanisms in Intensional Type Theory
- scientific article; zbMATH DE number 1187955 (Why is no real title available?)
- Abstract insertion sort in an extension of type theory with record types and subtyping
- System F with width-subtyping and record updating
- Type checking dependent (record) types and subtyping
- Implicit coercions in type systems
- scientific article; zbMATH DE number 2182489 (Why is no real title available?)
- A record calculus with principal types
- Martin-Löf's type theory as an open-ended framework
- Subtyping dependent types
- On subtyping in type theories with canonical objects
- Mathematical structures in natural language semantics: Zawadowski's contribution to linguistics
- Innovations in computational type theory using Nuprl
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247299)
