A set constructor for inductive sets in Martin-Löf's type theory
From MaRDI portal
Publication:5096257
DOI10.1007/BFb0018349zbMath1493.68119MaRDI QIDQ5096257
Publication date: 16 August 2022
Published in: Category Theory and Computer Science (Search for Journal in Brave)
68N15: Theory of programming languages
68N18: Functional programming and lambda calculus
68Q65: Abstract data types; algebraic specification
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03F50: Metamathematics of constructive systems
Related Items
Constructive characterizations of bar subsets, Program development in constructive type theory, Representing inductively defined sets by wellorderings in Martin-Löf's type theory, Programming interfaces and basic topology
