scientific article; zbMATH DE number 1302058

zbMATH Open0937.03068MaRDI QIDQ4247302FDOQ4247302

Authors: Catarina Coquand 

Publication date: 13 June 2000

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

normalizationdependent functionsfragment of Martin-Löf's polymorphic type theoryrealizability model for theories with dependent types

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35)

Cited In (17)

• An adequacy theorem for dependent type theory
• A characterization of ML in many-sorted arithmetic with conditional application
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Domain interpretations of Martin-Löf's partial type theory
• The Friedman‐Translation for Martin‐Löf's Type Theory
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• From realizability to induction via dependent intersection
• Game semantics for dependent types
• Indexed induction-recursion
• The metatheory of UTT
• Some normalization properties of Martin-Löf's type theory, and applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Type-theory in color
• Realizability and intuitionistic logic
• On the syntax of Martin-Löf's type theories

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)