MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK

DOI10.1142/S0129054101000400zbMath1320.03065MaRDI QIDQ5249247

Yasuyuki Tsukada

Publication date: 30 April 2015

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

zbMATH Keywords

partial equivalence relationsMartin-Löf's type theoryinductively defined typesopen-endednessbisimulation-like equivalencesstructured lazy evaluation systems

Mathematics Subject Classification ID

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

Cites Work

• Equational theories for inductive types
• Do-it-yourself type theory
• An intuitionistic theory of types with assumptions of high-arity variables
• Constructing type systems over an operational semantics
• Realizability interpretation of generalized inductive definitions
• Inductive families
• Proving congruence of bisimulation in functional programming languages
• Recursive models for constructive set theories
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Reading between the lines in constructive type theory
• 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
• HYBRID PARTIAL-TOTAL TYPE THEORY

This page was built for publication: MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK