Assignments and Project Ideas

• Project (due April 30). You can either select one of the following two projects, or suggest one of your own:
  • Automate as much of the proof of type safety for MinML in a system of your choice.
  • Design a bytecode language for MinML and implement the abstract machine for executing the bytecodes in a language of your choice.

• Assignment 3 (due April 4). Identify three kinds of checks that the bytecode verifier performs, and write class files (either directly or produced by a Java compiler) that violate each of those checks. Explain in as much detail as you can the steps performed by the verifier that cause it to reject your class file.

• Assignment 2 (due anytime before Spring break). Extend the MinML language with references. There are three new constructs: ref e which allocates a new reference whose contents is the value of e; deref e which returns the contents of e (which must evaluate to a reference); and setref e1 e2 which updates the contents of the reference e1 with the value of e2. Our references are rather close to Java's references and the Jbook treatment of Java objects should be helpful for this assignment.

  Your extension should include the additional type rules, semantics, and AsmGofer implementation which extends minML.gs. Extra credit for also adding an exception handler to catch the division by zero exception. Extra extra credit for a proof of type safety for the new language.

  The main purpose of this assignment is to get you more familiar with Haskell and the AsmGofer style used by the Jbook. It is much easier than directly extending the files that come with the Jbook (which most of you will be doing for your projects), and yet it has the same flavor and hence should be a good stepping stone.

• Assignment 1 (due 1/31 --- one assignment per group please). Do the proof of type safety for MinML. The notes define the language in detail.

• Assignment 0: Download the Jbook software (either from the web site or from the CD that comes with the book). Using Appendix A of the book as a guideline, test everyting to make sure your installation is correct. In particular, make sure you can convert a .class file to a .j file and vice versa and that you can step through the evaluation of sample Java programs using the machines provided with the book.

• Projects that are mostly about writing software:

  1. Work on an ASM implementation of the memory model of the Real Time Specification for Java. This is actually quite relevant to my research. The entire model is too large for a class project but would be quite appropriate for a class project that extends to a paid summer RA. If interested please contact me.

  2. Extend the Jbook software to handle things like garbage collection, stack inspection, memory model for threads, binary compatibility and separate compilation, etc.

• Projects that are mostly about automated proofs:

  1. Use a logical framework or theorem assistant to prove something about Java. The logical frameworks has links to many of the tools. The DECLARE system also appears to be quite suitable and reasonably easy to use. Huisman has several papers and a Ph.D. thesis that might provide some ideas.

  2. Use an automated tool (see previous point for pointers) to completely formalize the proof of type safety for MinML.

• Paper and pencil projects

  1. Do Exercises 7.3.1 and 7.3.2 about proving thread invariants.

  2. Do the proof of type safety for MinML with references and/or exceptions.

  3. Prove something about a Java extension like the RTJS or GJ

  4. The 1993 paper by Yuri Gurevich states the following:

     How can one establish that a [computer] model is faithful to reality?
     The approach is to construct an evolving algebra A that reflects the
     given computer system so closely that the correctness can be
     established by observation and experimentation. (There are tools for
     running evolving algebras.) A can then be refined or coarsened
     and used for numerous purposes. [p.1, Evolving Algebras 1993: Lipari Guide]
     

     Debate this statement in a paper. This is an individual (not group) project!