Assignments
- Please do all the exercises in Ch. 4 of Felleisen and Flatt's
manuscript.
- How about the following simple assignment. Research and report on
some of the type unsoundness results for at least two major programming
languages. Please submit your results Oct. 21 in class.
Project Ideas
- Automate some of the proofs we discussed in one of the theorem
provers or logical frameworks.
- Starting from this article on
abstract machines, implement and compare the machines and relate them to
standard reduction for the call-by-value lambda calculus. You might also
consider the machines in the article New
Developments in Abstract Machines.
- Starting from standard reduction for the call-by-need lambda
calculus, develop an abstract for call-by-need evaluation.
- Starting from an interpreter for multi-stage
programming, develop a standard reduction for the language.
- How would you automatically prove the unique decomposition lemma?
Develop an approach and implement a prototype.
sabry ... cs indiana edu