A set constructor for inductive sets in Martin-Löf's type theory

DOI10.1007/BFb0018349zbMath1493.68119OpenAlexW1539120745MaRDI QIDQ5096257

Kent Petersson, Dan Synek

Publication date: 16 August 2022

Published in: Category Theory and Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0018349

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Metamathematics of constructive systems (03F50)

Related Items

Data Types with Symmetries and Polynomial Functors over Groupoids, Constructive characterizations of bar subsets, Representing inductively defined sets by wellorderings in Martin-Löf's type theory, Indexed containers, Interactive programming in Agda – Objects and graphical user interfaces, The essence of ornaments, How to Reason Coinductively Informally, Program development in constructive type theory, W-types in setoids, Unnamed Item, Programming interfaces and basic topology

Cites Work

• Derivation of a parsing algorithm in Martin-Löf's theory of types
• Revised report on the algorithmic language ALGOL 68
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Recursive data structures
• Unnamed Item
• Unnamed Item
• Unnamed Item