View Proposal

Proposer
James McKinna
Title
Interactive Theorem Proving in Agda
Goal
To develop a fully formal proof of Fundamental Theorem of Arithmetic
Description
The Fundamental Theorem of Arithmetic (FTA), is as its name implies, one of the elementary cornerstones of number theory. Agda is an interactive theorem prover based on intuitionistic type theory, with a rich and highly developed library of elementary mathematical and computational structures. A glaring omission from the library is a complete formalisation of FTA. A concrete objective would be a complete proof of this result, and its successful incorporation into the library.
Resources
standard computing facilties
Background
functional programming; mathematics; logic
Url
Difficulty Level
Variable
Ethical Approval
None
Number Of Students
1
Supervisor
James McKinna
Keywords
Degrees
Back to List