A generalization of the Takeuti–Gandy interpretation

2015 ◽  
Vol 25 (5) ◽  
pp. 1071-1099 ◽  
Author(s):  
BRUNO BARRAS ◽  
THIERRY COQUAND ◽  
SIMON HUBER
Keyword(s):  
Algebraic Structure ◽  
Type Theory ◽  
Dependent Type Theory ◽  
The One ◽  
Weak Notion ◽  
Dependent Type

We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Löf type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.

scholarly journals Denotational semantics for guarded dependent type theory

2020 ◽  
Vol 30 (4) ◽  
pp. 342-378
Author(s):  
Aleš Bizjak ◽  
Rasmus Ejlers Møgelberg
Keyword(s):  
Type Theory ◽  
Denotational Semantics ◽  
Dependent Types ◽  
Proof Assistants ◽  
New Model ◽  
Dependent Type Theory ◽  
Additional Requirement ◽  
The One ◽  
Dependent Type

AbstractWe present a new model of guarded dependent type theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves internally right orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one found in homotopy theoretic models of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.

scholarly journals A relationally parametric model of dependent type theory

2014 ◽  
Vol 49 (1) ◽  
pp. 503-515 ◽  
Author(s):  
Robert Atkey ◽  
Neil Ghani ◽  
Patricia Johann
Keyword(s):  
Type Theory ◽  
Parametric Model ◽  
Dependent Type Theory ◽  
Dependent Type

scholarly journals Implementing a modal dependent type theory

2019 ◽  
Vol 3 (ICFP) ◽  
pp. 1-29 ◽  
Author(s):  
Daniel Gratzer ◽  
Jonathan Sterling ◽  
Lars Birkedal
Keyword(s):  
Type Theory ◽  
Dependent Type Theory ◽  
Dependent Type

scholarly journals Guarded Dependent Type Theory with Coinductive Types

2016 ◽  
pp. 20-35 ◽  
Author(s):  
Aleš Bizjak ◽  
Hans Bugge Grathwohl ◽  
Ranald Clouston ◽  
Rasmus E. Møgelberg ◽  
Lars Birkedal
Keyword(s):  
Type Theory ◽  
Dependent Type Theory ◽  
Dependent Type

scholarly journals Parametric quantifiers for dependent type theory

2017 ◽  
Vol 1 (ICFP) ◽  
pp. 1-29 ◽  
Author(s):  
Andreas Nuyts ◽  
Andrea Vezzosi ◽  
Dominique Devriese
Keyword(s):  
Type Theory ◽  
Dependent Type Theory ◽  
Dependent Type

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming

2004 ◽  
Vol 14 (1) ◽  
pp. 1-2
Author(s):  
GILLES BARTHE ◽  
PETER DYBJEN ◽  
PETER THIEMANN
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Type System ◽  
Type Systems ◽  
Special Issue ◽  
Dependent Type Theory ◽  
Dependent Type

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.

scholarly journals Univalent categories and the Rezk completion

2015 ◽  
Vol 25 (5) ◽  
pp. 1010-1039 ◽  
Author(s):  
BENEDIKT AHRENS ◽  
KRZYSZTOF KAPULKIN ◽  
MICHAEL SHULMAN
Keyword(s):  
Category Theory ◽  
Type Theory ◽  
Dependent Type Theory ◽  
Equivalence Of Categories ◽  
Segal Spaces ◽  
Definition Of ◽  
Categorical Semantics ◽  
Univalent Foundations ◽  
Dependent Type

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

Sign in / Sign up

Export Citation Format

Share Document