About
I am an Informatics PhD student at The University of Edinburgh. My thesis concerns ways of making dependently typed functional programming, in languages like Coq, Epigram and ATS, easier. I aim to do this by providing inductive proof automation to support programming with user-defined types and functions, as well providing helpful error feedback with the use of testing. The Coq theorem prover is being used for this research.
I am supported by an Engineering and Physical Sciences Research Council (EPSRC) DTA studentship and I am supervised by Jacques Fleuriot and Alan Smaill. I work at the Centre for Intelligent Systems and their Applications (CISA) and I am a member of the Mathematical Reasoning Group. Before this, I received a first class B.Eng Honours degree in Software Engineering in 2004 at the same institute. I was awarded the class medal and also received a merit scholarship from the The Royal Bank of Scotland.
Papers
- Sean Wilson, Jacques Fleuriot and Alan Smaill, Inductive Proof Automation for Coq (Draft), To appear in: Proceedings of the 2nd Coq Workshop, Edinburgh, UK, July 2010
- Sean Wilson, Jacques Fleuriot and Alan Smaill, Automation for Dependently Typed Functional Programming (Draft), To appear in: Special Issue of Fundamenta Informaticae on Dependently Typed Programming
- Sean Wilson and Jacques Fleuriot, Geometry Explorer: Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs, To appear in: Electronic Notes in Theoretical Computer Science
- Sean Wilson and Jacques Fleuriot, Geometry Explorer: Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs, In: Proceedings of the 12th Workshop on Automated Reasoning (ARW), Edinburgh, UK, July 2005
Events
- Upcoming talk: Dependently Typed Programming 2010, University of Edinburgh, Supporting Dependently Typed Functional Programming with Proof Automation and Testing, July 2010.
- Talk: Dependently Typed Programming 2008, University of Nottingham, Supporting the Development of Dependently Typed Functional Programs (slides), 18 February 2008.
- Informatics Jamboree 2005, Presented a poster entitled "Geometry Explorer: Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs" which received first prize in the poster competition, 25 April 2005.
- Scottish Theorem Proving, Presented a demo of Geometry Explorer, a project that combines dynamic geometry, automated geometry theorem proving and diagrammatic proofs, 22 October 2004.
Downloads
- Inductive proof automation plugin for Coq (version 0.1), including a tactic for performing rippling proofs and a QuickCheck-like testing tool. See the included README file for instructions on how to build the plugin and run the demo script. A high-level description of this plugin can be found here.
- Log files collected from a usability experiment that compared standard Coq error feedback with counterexample-based error feedback for program errors in dependently typed programs.
Other Activities
- Reviewer: 6th International Conference on the Theory and Application of Diagrams (Diagrams 2010).
- Reviewer: 5th International Conference on the Theory and Application of Diagrams (Diagrams 2008).
- Second supervisor: Jonas Halvorsen, Web Based GUI for Natural Deduction Proofs in Isabelle, MSc Thesis, 2007
- Editor: Rob Milne: A Tribute to a Pioneering AI Scientist, Entrepreneur and Mountaineer, Editors: Alan Bundy and Sean Wilson, August 2006
- Reviewer: 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005).
- Reviewer: 4th Mexican International Conference on Artificial Intelligence (MICAI 2005).
- Reviewer: 12th Workshop on Automated Reasoning (ARW 2005).
- Helped organised: 12th Workshop on Automated Reasoning (ARW 2005).
Teaching
- Teaching assistant for the Automated Reasoning (2008) course.
- Teaching assistant for the Multi-agent Semantic Web Systems (2007) course.
- Teaching assistant for the Advances in Programming Languages (2006) course.
- Tutor for the Software Engineering with Objects and Components 1 (2005) course.
- Teaching assistant for the Advances in Programming Languages (2005) course.
- Laboratory demonstrator for the Computer Science 2 (2005) course.
Links
- My old homepage has some fun graphical and physics related demos.
- Matthieu Sozeau's Russell language makes programming with dependent types in Coq more practical.
- Lucas Dixon's IsaPlanner framework makes use of rippling to automate inductive proofs in Isabelle.
- Lambda the Ultimate: programming languages weblog.
- Piled Higher and Deeper: amusing web comic about life in academia.
Contact
- Location:
- The University of Edinburgh
- School of Informatics
- Centre for Intelligent Systems and their Applications
- Informatics Forum, Room 2.05
- Edinburgh
- EH8 9AB
- Email Address:
- sean.wilson@ed.ac.uk