-
1
Normalisation by Evaluation for Type Theory, in Type Theory
Published 2017-10-01“…Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. …”
Get full text
Article -
2
-
3
-
4
Logic Programming & Type Theory /
Published 2012“…This book is a complete package for knowledge sharing on Logic Programming & Type Theory.…”
text -
5
Multimodal Dependent Type Theory
Published 2021-07-01“…We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. …”
Get full text
Article -
6
Dualized Simple Type Theory
Published 2017-04-01“…We propose a new bi-intuitionistic type theory called Dualized Type Theory (DTT). It is a simple type theory with perfect intuitionistic duality, and corresponds to a single-sided polarized sequent calculus. …”
Get full text
Article -
7
Idempotents in intensional type theory
Published 2017-04-01“…We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. …”
Get full text
Article -
8
Modalities in homotopy type theory
Published 2020-01-01“…Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. …”
Get full text
Article -
9
-
10
Dialectica models of type theory
Published 2018“…We present two Dialectica-like constructions for models of intensional Martin-Löf type theory based on Gödel's original Dialectica interpretation and the Diller-Nahm variant, bringing dependent types to categorical proof theory. …”
Conference item -
11
-
12
-
13
Multi-level Contextual Type Theory
Published 2011-10-01“…Contextual type theory distinguishes between bound variables and meta-variables to write potentially incomplete terms in the presence of binders. …”
Get full text
Article -
14
Cellular Cohomology in Homotopy Type Theory
Published 2020-06-01“…We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. …”
Get full text
Article -
15
Internal Parametricity for Cubical Type Theory
Published 2021-11-01“…We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. …”
Get full text
Article -
16
Call-by-name Gradual Type Theory
Published 2020-01-01“…We present gradual type theory, a logic and type theory for call-by-name gradual typing. …”
Get full text
Article -
17
On the strength of proof-irrelevant type theories
Published 2008-09-01“…We present a type theory with some proof-irrelevance built into the conversion rule. …”
Get full text
Article -
18
Explicit Substitutions for Contextual Type Theory
Published 2010-09-01“…Its typing discipline is derived from contextual modal type theory. We first present a dependently typed lambda calculus with explicit substitutions for ordinary variables and explicit meta-substitutions for meta-variables. …”
Get full text
Article -
19
The Independence of Markov's Principle in Type Theory
Published 2017-08-01“…Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. …”
Get full text
Article -
20
A dependent nominal type theory
Published 2012-02-01“…So far nominal techniques have mostly been studied using classical logic or model theory, not type theory. Nominal extensions to simple, dependent and ML-like polymorphic languages have been studied, but decidability and normalization results have only been established for simple nominal type theories. …”
Get full text
Article