Martin-Löf's type theory as an open-ended framework

DOI10.1142/S0129054101000400zbMATH Open1320.03065MaRDI QIDQ5249247FDOQ5249247

Authors: Yasuyuki Tsukada 

Publication date: 30 April 2015

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Recommendations

• On the syntax of Martin-Löf's type theories
• Remarks on Martin-Löf's partial type theory
• scientific article; zbMATH DE number 1302055
• scientific article; zbMATH DE number 65535
• scientific article; zbMATH DE number 4212037

zbMATH Keywords

inductively defined typespartial equivalence relationsopen-endednessMartin-Löf's type theorybisimulation-like equivalencesstructured lazy evaluation systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Second- and higher-order arithmetic and fragments (03F35)

Cites Work

• Inductive families
• Proving congruence of bisimulation in functional programming languages
• Do-it-yourself type theory
• HYBRID PARTIAL-TOTAL TYPE THEORY
• Recursive models for constructive set theories
• Equational theories for inductive types
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Realizability interpretation of generalized inductive definitions
• A NEW FORMALIZATION OF FEFERMAN’S SYSTEM OF FUNCTIONS AND CLASSES AND ITS RELATION TO FREGE STRUCTURE
• Constructing type systems over an operational semantics
• An intuitionistic theory of types with assumptions of high-arity variables
• Reading between the lines in constructive type theory
• A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS

Cited In (7)

• Extending Martin-Löf type theory by one Mahlo-universe
• Title not available (Why is that?)
• ERRATA: "The paper: MARTIN-LOF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK"
• The Friedman‐Translation for Martin‐Löf's Type Theory
• Title not available (Why is that?)
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• Kripke Semantics for Martin-Löf’s Extensional Type Theory

This page was built for publication: Martin-Löf's type theory as an open-ended framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5249247)