Revisiting the categorical interpretation of dependent type theory

, &
Theoretical Computer Science 546:99--119 (2014)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Add categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,571

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

An interpretation of Martin-löf's type theory in a type-free theory of propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.
Propositions as [Types].Steve Awodey & Andrej Bauer - unknown
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
On the strength of dependent products in the type theory of Martin-Löf.Richard Garner - 2009 - Annals of Pure and Applied Logic 160 (1):1-12.
Categories with families and first-order logic with dependent sorts.Erik Palmgren - 2019 - Annals of Pure and Applied Logic 170 (12):102715.
Categorical and algebraic aspects of Martin-löf type theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.
Syntactic calculus with dependent types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
Alpha-conversion, conditions on variables and categorical logic.Pierre-Louis Curien - 1989 - Studia Logica 48 (3):319 - 360.
Applications of Kolmogorov Complexity to Computable Model Theory.B. Khoussainov, P. Semukhin & F. Stephan - 2007 - Journal of Symbolic Logic 72 (3):1041 - 1054.
Supersimple ω-categorical groups and theories.David M. Evans & Frank O. Wagner - 2000 - Journal of Symbolic Logic 65 (2):767-776.
A note on Russell's paradox in locally cartesian closed categories.Andrew M. Pitts & Paul Taylor - 1989 - Studia Logica 48 (3):377 - 387.
Supersimple $\omega$-Categorical Groups and Theories.David Evans & Frank Wagner - 2000 - Journal of Symbolic Logic 65 (2):767-776.
An interpretation of martin‐löf's constructive theory of types in elementary topos theory.Anne Preller - 1992 - Mathematical Logic Quarterly 38 (1):213-240.
Type Theory and Homotopy.Steve Awodey - unknown
Revisiting the 1927 Solvay conference and the early interpretation of quantum mechanics: Guido Bacciagaluppi and Antony Valentini: Quantum theory at the crossroads: Reconsidering the 1927 Solvay conference. Cambridge: Cambridge University Press, 2009, xxv+530pp, £75.00, $130.00 HB.Martin Jähnert - 2011 - Metascience 21 (1):125-129.

Analytics

Added to PP
2020-09-03

Downloads
0

6 months
0

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

No references found.

Add more references