View Proposal

Proposer
Fairouz Kamareddine
Title
Proving correctness of Turing machine specifications
Goal
Check that the specifications of a Turing machine are correct and that the machine works as expected
Description
You learned how to write and implement Turing machines to solve certain tasks. But, how do you ensure that the machine is correct and meets its specification? How do you show the properties of your Turing machine (e.g., whether it terminates). This project is to implement the language of Turing machines in Lean (or your choice of provers) and to check the properties of different Turing machines as well as the universal machine.
Resources
Background
Url
Difficulty Level
High
Ethical Approval
None
Number Of Students
1
Supervisor
Fairouz Kamareddine
Keywords
Degrees
Back to List