scientific article; zbMATH DE number 1302058
From MaRDI portal
Publication:4247302
Recommendations
- scientific article; zbMATH DE number 1497733
- scientific article; zbMATH DE number 3853066
- An interpretation of Martin-Löf's type theory in a type-free theory of propositions
- A realizability interpretation of Church's simple theory of types
- A Realizability Model for Impredicative Hoare Type Theory
- Remarks on Martin-Löf's partial type theory
- Domain interpretations of Martin-Löf's partial type theory
- AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
- Internalising modified realisability in constructive type theory
- A coherence theorem for Martin-Löf's type theory
Cited in
(19)- On the syntax of Martin-Löf's type theories
- Game semantics for dependent types
- An adequacy theorem for dependent type theory
- Characterizing the interpretation of set theory in Martin-Löf type theory
- Indexed induction-recursion
- From realizability to induction via dependent intersection
- scientific article; zbMATH DE number 3853066 (Why is no real title available?)
- The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
- A characterization of ML in many-sorted arithmetic with conditional application
- scientific article; zbMATH DE number 1497733 (Why is no real title available?)
- scientific article; zbMATH DE number 1497737 (Why is no real title available?)
- scientific article; zbMATH DE number 1531359 (Why is no real title available?)
- The Friedman‐Translation for Martin‐Löf's Type Theory
- Some normalization properties of Martin-Löf's type theory, and applications
- Type-theory in color
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- The metatheory of UTT
- Realizability and intuitionistic logic
- Domain interpretations of Martin-Löf's partial type theory
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 Q4247302)
