Adequate Models for Recursive Program Schemes

Download: PDF.

“Adequate Models for Recursive Program Schemes” by Michael D. Ernst. Bachelors thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), June 1989.


This thesis is a pedagogical exposition of adequacy for recursive program schemes in the monotone frame. Adequacy relates the operational and denotational meanings of a term; it states that for any term of base type, the operational and denotational meanings are identical. Adequacy is typically proved in the continuous frame. This is a pedagogically questionable step; in order to prove adequacy (or some other property) of a pair of semantics, it would be desirable to show the property directly, without introducing superfluous notions. This difficulty is particularly acute because, in general, not all monotone functions are continuous.

This thesis attempts to work out the concept of adequacy for a class of monotone first-order recursive program schemes, using Vuillemin and Manna's method of “safe” computation rules. The attempt is very nearly successful, but at a crucial point the fact that the scheme-definable functions are, in fact, continuous as well as monotone must be used.

Download: PDF.

BibTeX entry:

   author = {Michael D. Ernst},
   title = {Adequate Models for Recursive Program Schemes},
   school = {MIT Department of Electrical Engineering and Computer Science},
   type = {Bachelors thesis},
   address = {Cambridge, MA},
   month = jun,
   year = {1989}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.