source: etc/campbell/dev-notes/2013-05-13-non-terminating.txt

Last change on this file was 3672, checked in by campbell, 3 years ago

I'd been keeping some notes in the repo; didn't commit these before

File size: 375 bytes
Line 
1Something that came up while discussing the presentation of the front-end for
2the review meeting:
3
4It would have been nice to show that any non-terminating function execution
5yields an infinite trace of cost labels.  However, this needs the soundness of
6the cost labelling, which might be a little awkward because you'd want the
7result at Clight, but it's checked at RTLabs.
Note: See TracBrowser for help on using the repository browser.