Representing inductively defined sets by wellorderings in Martin-Löf's type theory
type: Item
instance of: scholarly article
title: Representing inductively defined sets by wellorderings in Martin-Löf's type theory
zbMATH Open document ID: 0898.68047
DOI: 10.1016/S0304-3975(96)00145-4
author: Peter Dybjer
published in: Theoretical Computer Science
publication date: 1998-07-27T00:00:00Z
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 1179140
zbMATH Keywords: Martin-Löf's extensional type theory
MaRDI profile type: Publication
cites work: Q5753923
cites work: Q4012883
cites work: Inductive families
cites work: Q4296744
cites work: Q5638283
cites work: Constructive mathematics and computer programming
cites work: Q3688389
cites work: Proving termination of normalization functions for conditional expressions
cites work: A set constructor for inductive sets in Martin-Löf's type theory
description: scientific article; zbMATH DE number 1179140