Related papers: Pure Type Systems without Explicit Contexts
We define a class of formal systems inspired by Prawitz's theory of grounds. The latter is a semantics that aims at accounting for epistemic grounding, namely, at explaining why and how deductively valid inferences have the power to…
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the…
We study increasingly expressive type systems, from $F^\mu$ -- an extension of the polymorphic lambda calculus with equirecursive types -- to $F^{\mu;}_\omega$ -- the higher-order polymorphic lambda calculus with equirecursive types and…
We give a type system in which the universe of types is closed by reflection into it of the logical relation defined externally by induction on the structure of types. This contribution is placed in the context of the search for a natural,…
B-systems are algebras (models) of an essentially algebraic theory that is expected to be constructively equivalent to the essentially algebraic theory of C-systems which is, in turn, constructively equivalent to the theory of contextual…
Simple type theory is formulated for use with the generic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the eta-operator) introduce the…
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present…
The logical technique of focusing can be applied to the $\lambda$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $\beta\eta$-normal forms.…
This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We…
This paper proposes an alternative to standard first-order logic that seeks greater naturalness, generality, and semantic self-containment. The system removes the first-order restriction, avoids type hierarchies, and dispenses with external…
We provide a treatment of isomorphism within a set-theoretic formulation of dependent type theory. Type expressions are assigned their natural set-theoretic compositional meaning. Types are divided into small and large types --- sets and…
Shape types are a general concept of process types which work for many process calculi. We extend the previously published Poly* system of shape types to support name restriction. We evaluate the expressiveness of the extended system by…
This paper provides a systematic account of the hidden variable models (HVMs) formulated to describe systems of random variables with mutually exclusive contexts. Any such system can be described either by a model with free choice but…
Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been…
In this paper we consider a type system with a universal type $\omega$ where any term (whether open or closed, $\beta$-normalising or not) has type $\omega$. We provide this type system with a realisability semantics where an atomic type is…
We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is…
We reformulate recent advances in directed type theory--a type theory where the types have the structure of synthetic (higher) categories--as a logical calculus with multiple context 'zones', following the example of Pfenning and Davies.…
Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing…
Humans can generate reasonable answers to novel queries (Schulz, 2012): if I asked you what kind of food you want to eat for lunch, you would respond with a food, not a time. The thought that one would respond "After 4pm" to "What would you…
The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer,…