Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- 20 April 1997
- journal article
- research article
- Published by Elsevier in Theoretical Computer Science
- Vol. 176 (1-2) , 329-335
- https://doi.org/10.1016/s0304-3975(96)00145-4
Abstract
No abstract availableKeywords
This publication has 5 references indexed in Scilit:
- Constructive Mathematics and Computer ProgrammingPublished by Elsevier ,2014
- Computation and reasoning: a type theory for computer scienceChoice Reviews Online, 1995
- Inductive familiesFormal Aspects of Computing, 1994
- Proving termination of normalization functions for conditional expressionsJournal of Automated Reasoning, 1986
- Hauptsatz for the Intuitionistic Theory of Iterated Inductive DefinitionsPublished by Elsevier ,1971