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.
• Jack Williams, CS 2013, Spreadsheet Programming with User Defined Types and Functions. Jack's Jeksy system adds user-defined functions and user-defined record types to the Jeks spreadsheet application.
• Craig Innes, MInf 2014, Programming as an Interactive Experience. Craig produced a programming tool for simple 2D graphics and animation in Haskell which embodies the ideas in Bret Victor's talk Inventing on Principle. A change in the source code leads to an immediate change in the resulting image/animation. Going in the other direction, altering the image leads to an immediate corresponding change in the source code, and time can be manipulated in the animation.
• Alexandros Spathoulas, M.Sc. 2014, Assessing Tools for Finding Bugs in Concurrent Java. The test suite used in this study is available here.
• Mac Chong, B.Sc. 2015, Teaching Tool for Demonstrating Digital Security Weaknesses, and Rory Mathers, B.Sc. 2016, Teaching Tool for Computer Security 'Learn Security'. Mac produced, and Rory extended and improved, a well-engineered and polished Android app for demonstrating and explaining some of the OWASP top-ten web application security vulnerabilities and countermeasures for defending against them, demonstrating attacks on a simulated banking website and aimed at users with a low to moderate level of prior knowledge of computer security. The ability to look at an attack in progress from the viewpoint of the victim, attacker and server, and to switch viewpoints in the middle of the attack, makes the demonstration much richer and more compelling than a simple linear demonstration would be. The app is available from the Google Play Store.

  ---

  Don Sannella. Please mail me if you have any comments on this page.
  Last modified: Wed Aug 29 11:51:59 BST 2007