Computer Science – Logic in Computer Science
Scientific paper
2010-12-22
EPTCS 43, 2010, pp. 29-48
Computer Science
Logic in Computer Science
In Proceedings PAR 2010, arXiv:1012.4555
Scientific paper
10.4204/EPTCS.43.3
Some total languages, like Agda and Coq, allow the use of guarded corecursion to construct infinite values and proofs. Guarded corecursion is a form of recursion in which arbitrary recursive calls are allowed, as long as they are guarded by a coinductive constructor. Guardedness ensures that programs are productive, i.e. that every finite prefix of an infinite value can be computed in finite time. However, many productive programs are not guarded, and it can be nontrivial to put them in guarded form. This paper gives a method for turning a productive program into a guarded program. The method amounts to defining a problem-specific language as a data type, writing the program in the problem-specific language, and writing a guarded interpreter for this language.
No associations
LandOfFree
Beating the Productivity Checker Using Embedded Languages 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 Beating the Productivity Checker Using Embedded Languages, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Beating the Productivity Checker Using Embedded Languages will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-581945