The Current Status of My Dissertation Efforts

1. Prelim Success, paper work done
2. Conversions
   1. HOL Light (John H) fully converted to SML '97
   2. Supporting Packages possibly done enough
      1. "more_list" done
      2. "ascii" done
      3. "string/more_string" done
      4. "lift/finmap" lots & more done, lots left
      5. "sets" done
      6. "part_fun"untouched, do I need?--don't think so
   3. Mutual Recursion (Myra/Elsa) Done (Thanks John H for a key function).
   4. Nested Recursion (Elsa) Done (Thanks again to John H for some key functions and Elsa for some fabulous assistance with debugging.)
   5. holML(Myra) The Up-To-Date Version
      1. Common Eval Done
      2. Rest Eval Done
      3. Determinacy Done
      4. Types Untouched: Will I Need a Symbolic Elaborator? -- Don't think so, think we will just do dynamic semantics for this project
   6. New Code (write or adapt)
      1. Reduce arithmetic terms to zero done
      2. Boyer-Moore Taut Checkerdone
      3. HOL (rjb) Taut Checkerdone
      4. HOL Arith Underway
      5. Code "User" PRI Done
      6. System Extender Rule written, needs work
      7. Parser (general ML into abstract syntax) Done: less infix base values, and coercing "long" vars
      8. Symbolic Evaluator --working
      9. Symbolic Elaborator -- Probably not needed.
      10. Base Environment--need to extend with types/constructors to model HOL termssome
   7. Proofs to Do
      1. Zero
      2. BMTP Taut
      3. HOL Taut
      4. HOL Arith
   8. Timing Studies
      1. Use of the Raise/Handle Simplification for Terms (Draft)
      2. My Taut vs the HOL Taut
      3. My Arith vs the HOL Arith
   9. Write the Dissertation
      1. Intro (mainly drawn from Prelim)
      2. Related Work
      3. Analysis of Extension (draw from FM-Trends paper)
      4. Symbolic Evaluation
      5. Proofs Completed
      6. Timing Results
      7. Conclusions
      8. Appendices
         1. ML & SML/NJ
         2. HOL
         3. ??

   Last Updated: 15 May 1998