Teaching and Supervision

• Nov 2006: at ITU of Copenhagen a 2 day workshop on Proof Planning for Inductive Theories.
• July 2004, with Alan Bundy, at IJCAR'04, a one day workshop on The Automation of Inductive Theorem Proving.

If you are interested in doing one of these projects, or something similar, or just want more information, I'd be happy to talk to you about it!

• MSc: An expressive language of signatures for Standard ML
• MSc: A Proof Centric Proof Assistant
• MSc: IsaPlanner PRESS
• MSc: Efficient Rewriting in IsaPlanner
• Honers/MSc: Parsing Everywhere: A Study in Distributed Parsing
• Honers/MSc: The Fastest Possible String Matcher
• Honers/MSc: Distributed Democracy as shared Arguments
• Honers/MSc: Beyond ERA: paper-reviewing with arguments
• Honers/MSc: Small to Asbtract Planning: composing small plan steps to form more abstract plan operators in order to make planning more efficient. Interseresting questions: preserving completeness? Tested on many test-cases.
• Honers: A Proof General for Proof Plans
• Honers: Visualising Graph Rewriting
• Honers: World-Wide Quantomatic
• Honers: Fancy Talks with Processing
• Honers: Arguments with History

• IsaScheme: scheme-based theorem discovery for Isabelle -- (PhD student) Omar Montano Rivas, (main supervisor: Roy McCasland)
• Proof Engineernig -- (PhD student) Iain Whiteside, (co-superviser: David Aspinall)

• MSc: PolyML Firefox Extension -- Karolis Narkevicius 2009-2010
• MSc: Discrimination nets for fast quantum reasoning -- David Joseph Douglas 2009-2010
• Proof Critics and Lemma Speculation in IsaPlanner -- (PhD) Moa Johansson 2005-2009
• Vanity Theorem Proving -- (Honers project) Flaminia Cavallo, 2008-2009
• An elementary, machine assisted proof of a multilinear generalisation of the Cauchy-Schwarz inequality -- (Honers project) Iain Whiteside, 2008-2009
• Relational Rippling - (Honers project + 2 month summer project) Dominic Mulligan, 2006-2007
• Dialogue Planning with Linear Logic (Honers project + 2 month summer project) - Tracy Tsang, 2006-2007
• On Learning Proof Planning Methods - (MSc) Ferdinand Hoermann, 2006-2007
• Plans from Proofs -- (MSc) Guillermo Ivan Gallegos Ayala, 2005-2006
• Best First Rippling - (Honers project) Moa Johansson, 2004-2005