A MetaPRL Eclipse Plug-in
- Supervisor Dr. Joseph Kiniry
- Subject Area Software Engineering
- Pre-requisite Strong knowledge of Java and basic software engineering principles
- Co-requisite (things you must learn along the way) Eclipse use and plug-in development
- Subject Coverage Integrated Development Environments, Higher-order Theorem Provers
- Project Type Design and Implementation
- Hardware/Software: Any machine running x86/Linux or Mac OS X
Description
A logical framework is a general-purpose, logic-independent formal system in which one can describe and reason about and within multiple logics. The MetaPRL system, developed by Jason Hickey's group at Caltech (and with whom Joe Kiniry is related) is the latest-and-greatest logical framework in development.
While MetaPRL has a basic command-line interface and a relatively rich-but-fragile JavaScript-based interface, it is lacking a powerful front-end akin to that provided by other similar projects.
The purpose of this project is to develop the initial version of such a front-end, using the Eclipse platform as a foundation for such.
Mandatory
- Show expertise with the Eclipse Platform, particularly the plug-ins architecture.
- Specify a JML-annotated Java interface for the I/O interface and proof interface of MetaPRL.
- Design, implement, and test a MetaPRL plugin for the Eclipse Platform supporting MetaPRL specification authoring and proof interaction.
- Release the plugin to the world under an appropriate FLOSS license.
Discretionary
- Support plug-in indefinitely and help kickstart a community focused on the evolution and maintenance of the plug-in.
- Coauthor, submit, and publish a paper on this work.