CORRECTNESS OF A COMPILER SPECIFICATION FOR THE SECD MACHINE

Simple item page
dc.contributor.authorSimpson, Toddeng
dc.date.accessioned2008-05-20T23:29:04Z
dc.date.available2008-05-20T23:29:04Z
dc.date.computerscience1999-05-27eng
dc.date.issued1990-10-01eng
dc.description.abstractWe develop a specification in Natural Semantics of a compiler from the lambda calculus with let and letrec (miniSML) to the SECD machine. We prove that the compiler specification is correct by simplifying the approach of Despeyroux [2] and changing the proof technique to work with non-terminating semantics. We then extend the SECD to handle lazy evaluation and outline the proof of the compiler specification for this.eng
dc.description.notesWe are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at digitize@ucalgary.caeng
dc.identifier.department1990-410-34eng
dc.identifier.doihttp://dx.doi.org/10.11575/PRISM/31297
dc.identifier.urihttp://hdl.handle.net/1880/46525
dc.language.isoEngeng
dc.publisher.corporateUniversity of Calgaryeng
dc.publisher.facultyScienceeng
dc.subjectComputer Scienceeng
dc.titleCORRECTNESS OF A COMPILER SPECIFICATION FOR THE SECD MACHINEeng
dc.typeunknown
thesis.degree.disciplineComputer Scienceeng
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
1990-410-34.pdf
Size:
3.77 MB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
1.86 KB
Format:
Plain Text
Description:
Download
Collections
Science Research & Publications