Show simple item record

dc.contributor.advisor Felleisen, Matthias
dc.creatorClements, John Brinckerhoff
dc.date.accessioned 2009-06-04T07:55:45Z
dc.date.available 2009-06-04T07:55:45Z
dc.date.issued 2001
dc.identifier.urihttps://hdl.handle.net/1911/17409
dc.description.abstract Programmers rely on the correctness of their tools. Semanticists have long studied the correctness of compilers, but we make the case that other tools deserve semantic models, too, and that using these models can help in developing these tools. We examine these ideas in the context of DrScheme's stepper. The stepper operates within the existing evaluator, placing breakpoints and reconstructing source expressions from information placed on the stack. We must ask whether we can prove the correspondence between the source expressions emitted by the stepper and the steps in the formal reduction semantics. To answer this question, we develop a high-level semantic model of the extended compiler and run-time machinery. Rather than modeling the evaluation as a low-level machine, we model the relevant low-level features of the stepper's implementation in a high-level reduction semantics. The higher-level model greatly simplifies the correctness proof. We expect the approach to apply to other semantics-based tools.
dc.format.extent 43 p.
dc.format.mimetype application/pdf
dc.language.iso eng
dc.subjectComputer science
dc.title Modeling an algebraic stepper
dc.type.genre Thesis
dc.type.material Text
thesis.degree.department Computer Science
thesis.degree.discipline Engineering
thesis.degree.grantor Rice University
thesis.degree.level Masters
thesis.degree.name Master of Science
dc.identifier.citation Clements, John Brinckerhoff. "Modeling an algebraic stepper." (2001) Master’s Thesis, Rice University. https://hdl.handle.net/1911/17409.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record