M.Sc. and UG student past projects

• Brian Paxton, AI/CS 1992, The Implementation of a Modular Prolog System Based on Standard ML Modules.
  Modular SB-Prolog is SB-Prolog extended with module facilities patterned after those described in "A calculus for the construction of modular Prolog programs" by D. Sannella and L. Wallen (Journal of Logic Programming 12:147-177, 1992).
• Paul Varnish, M.Sc. 1992, Generating Proof Obligations for Extended ML Development Steps.
  The EML proof obligation generator is here.
• Donald Baillie, M.Sc. 1999, Proving Theorems about Algebraic Specifications.
  The CASLtoPVS system converts basic specifications in CASL to PVS.
• Alison Keane, M.Sc. 1999, A Tool for Investigating Type Errors in ML Programs (also available in a not-very-good html translation).
  The code of her system, which is a point-and-click system for type debugging in the SML core language, is here.
• Will Bryson, CS 2000, Route Planning for the Dervish Mine Detonating Vehicle (winner of the Scottish Software Federation's "Young Software Engineer of the Year" first prize for the best Computer Science final year project in Scotland, see report).
  See here for more about the Dervish project.
• Iain Denniston, CS 2001, A tool for investigating type errors in SML programs. Iain's code is available from me on request.
• Kenneth MacKenzie, M.Sc. 2001, Extending Extended ML.
  Kenneth's EML parser and typechecker, based on Moscow ML version 2.0, is available from the Extended ML web page.
• Paul Flanagan, CS 2003, Effect Systems for Exceptions and Mutable Variables. Paul's code for effect inference is available from me on request.
• Neil Wilkie, SE 2005, Random Testing of ML Programs. Neil's QuickECheck system, a tool for testing ML programs based on Christopher League's QCheck/SML, is available here.