Representing inductively defined sets by wellorderings in Martin-Löf's type theory

DOI10.1016/S0304-3975(96)00145-4zbMath0898.68047MaRDI QIDQ1392287

Peter Dybjer

Publication date: 27 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

Martin-Löf's extensional type theory

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (12)

Finitary higher inductive types in the groupoid model ⋮ A set constructor for inductive sets in Martin-Löf's type theory ⋮ Coalgebras in functional programming and type theory ⋮ Do-it-yourself type theory ⋮ Indexed containers ⋮ The essence of ornaments ⋮ Partiality, State and Dependent Types ⋮ Type-theoretic interpretation of iterated, strictly positive inductive definitions ⋮ Unnamed Item ⋮ W-types in setoids ⋮ Wellfounded trees in categories ⋮ Containers: Constructing strictly positive types

Cites Work

• Proving termination of normalization functions for conditional expressions
• Inductive families
• Constructive mathematics and computer programming
• A set constructor for inductive sets in Martin-Löf's type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Representing inductively defined sets by wellorderings in Martin-Löf's type theory