Equational theories for inductive types

DOI10.1016/S0168-0072(96)00021-8zbMath0873.03019OpenAlexW2097508095MaRDI QIDQ678762

Ralph Loader

Publication date: 26 October 1997

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(96)00021-8

zbMATH Keywords

full abstractioninductive typesequational theorytyped lambda calculusdomain modelPER model

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Linear realizability and full completeness for typed lambda-calculi ⋮ Least and Greatest Fixpoints in Game Semantics ⋮ MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK

Cites Work

• The system \({\mathcal F}\) of variable types, fifteen years later
• The lambda calculus, its syntax and semantics
• Total sets and objects in domain theory
• Classical recursion theory. Vol. II
• Interpreting higher computations as types with totality
• Total objects in inductively defined types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Equational theories for inductive types