Type-based termination of recursive definitions
- 1 January 1999
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 14 (1) , 97-141
- https://doi.org/10.1017/s0960129503004122
Abstract
This paper introduces in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to support coinductive types and corecursive function definitions also.Keywords
This publication has 0 references indexed in Scilit: