Computer Science – Logic in Computer Science
Scientific paper
2000-10-31
Journal of Symbolic Computation 2 (1986), 325-355
Computer Science
Logic in Computer Science
Scientific paper
Martin-L\"of's Intuitionistic Theory of Types is becoming popular for formal reasoning about computer programs. To handle recursion schemes other than primitive recursion, a theory of well-founded relations is presented. Using primitive recursion over higher types, induction and recursion are formally derived for a large class of well-founded relations. Included are < on natural numbers, and relations formed by inverse images, addition, multiplication, and exponentiation of other relations. The constructions are given in full detail to allow their use in theorem provers for Type Theory, such as Nuprl. The theory is compared with work in the field of ordinal recursion over higher types.
No associations
LandOfFree
Constructing Recursion Operators in Intuitionistic Type Theory does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Constructing Recursion Operators in Intuitionistic Type Theory, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Constructing Recursion Operators in Intuitionistic Type Theory will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-446294