View Proposal
-
Proposer
-
Joe Wells
-
Title
-
assemble and test the Isabelle/Isar proof language definition
-
Goal
-
-
Description
- Isabelle/Isar is a widely used proof assistant and proving environment for formal verification. There is no single place where a complete
and up-to-date definition of the Isabelle/Isar input language can be found. Some of the pieces are in research publications, some pieces
are in PhD dissertations, some pieces are in software documentation, and some pieces are in the Isabelle/Isar source code. And only the
source code is certain to be up-to-date. This project is about gathering the pieces, assembling them, and writing some tests to confirm
that the definition that the project synthesizes is correct.
- Resources
-
-
Background
-
logic, mathematics, functional programming, debugging, LaTeX
-
Url
-
-
Difficulty Level
-
Variable
-
Ethical Approval
-
None
-
Number Of Students
-
1
-
Supervisor
-
Joe Wells
-
Keywords
-
-
Degrees
-
Bachelor of Science in Computer Science
Master of Engineering in Software Engineering
Master of Science in Computing (2 Years)
Master of Science in Data Science
Bachelor of Science in Computing Science