Assignments

• A Bytecode Verifier (Due 5/3). This assignment is about writing a bytecode verifier for methods containing instructions from this language:

  data Instruction = 
    Push Int
  | Inc
  | Pop
  | If Int         
  | Store Int
  | Load Int
  | New String
  | Init String
  | Use String
  | Halt
  

  (The instructions Jsr Int and Ret Int would be considered extra credit.) The verification rules for each instruction are in the paper handed previously. The general strategy for the implementation is described starting the bottom of page 144 of (or section 4.9.2) The Java Virtual Machine Specification, second edition. Step 4 on page 145 describes the simplest possible merging of values in which two values which are not the same are merged to an unusable value. No need to attempt to use sets of values like in the JBook.

• A Bytecode Interpreter (Due 4/15). This assignment is about writing (in Haskell) a bytecode interpreter for the small fragment of the JVM bytecode language described in this paper. The precise set of instructions is the following:

  data Instruction = 
    Push Int
  | Inc
  | Pop
  | If Int           -- Added April 11, 2003; should have been there all along
  | Store Int
  | Load Int
  | New String
  -- | Super String  -- Deleted April 7, 2003
  | Init String
  | Use String
  -- | Jsr String    -- Replaced April 7, 2003; see next line
  | Jsr Int
  | Ret Int
  | Halt
  

• Type Safety for NanoML revised (Due 3/25). Formalize the proof of type safety in Twelf. Here is the file that specifies the type checker and evaluation rules. To run Twelf on the CS machines, the easiest way is to use emacs. Add the following in the initialization file for emacs:

  (setq twelf-root "/l/twelf/")
  (load (concat twelf-root "emacs/twelf-init.el"))
  

  The documentation and examples are under the directory /l/twelf.

• Trustful MinML interpreter (Due 3/6).

• Type Safety for NanoML (Due 2/25). (Postscript, PDF, Latex source).

• MinML Semantics and Type System (Due 2/13)

• MinML Semantics (See Assignment 3)

• Introduction to Haskell (Due 1/23)

Project Ideas

• Formalizing a small subset of Java in AsmGofer

• Proving type safety for a small language

• Complete a major proof in the Jbook

• Formalize a small type safety proof in an automated system like Isabelle

• Write a paper on some topic related to the class

• Extend the software of the Jbook to handle an additional aspect of Java, e.g., garbage collection