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

DOI10.1142/S0129054101000400MaRDI QIDQ5249247zbMATH OpenFDO

Authors Yasuyuki Tsukada

Publication date 30 April 2015

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

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)

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

Cites work

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

Cited in

(7)

• Extending Martin-Löf type theory by one Mahlo-universe
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• ERRATA: "The paper: MARTIN-LOF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK"
• The Friedman‐Translation for Martin‐Löf's Type Theory
• scientific article; zbMATH DE number 5033853 (Why is no real title available?)
• 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)