View Proposal

---

Proposer

Marko Doko

Title

Formalizing Computational Models using the Coq Proof Assistant

Goal

Develop a formalization within the Coq proof assistant.

Description

Very expressive type systems commonly used by functional programming languages can be used to specify very complex data types. Those data types can be so complex that they allow encoding of entire mathematical theorems inside a single data type! This expressiveness of type systems enables creation of tools such as the Coq proof assistant (https://coq.inria.fr/). These tools allow the user to specify mathematical structures, state results about those structures (lemmas, theorems), and prove those results correct. Using proof assistants allows us to create machine-checked proofs, which we can trust with an extremely high degree of confidence, much higher than if the proofs have only been looked over by humans. The aim of this project is to serve as an introduction to using proof assistants through first specifying a mathematical object, and then proving some basic properties of it. The project consists of picking one computational model (e.g., finite automata, λ-calculus, Turing machines), learning enough about the Coq proof assistant to specify the selected computational model within Coq, and proving some fundamental properties about it. You can choose to focus on any computational model you like - pick the one you're the most familiar with, or the one which interests you the most. The project is highly flexible in terms of scope. It can be molded according to the student's ambition and interest throughout the project's duration. What will you get out of this project? In terms of practical skills, you will gain experience in writing formal specification, using dependent types, and programming in functional languages. In terms of building up your wider understanding, you will get a first-hand experience of the deep interconnectedness between mathematics and programming. If you enjoy programming, but have always found mathematical proofs difficult and too abstract, this project will give you a completely different outlook on proofs. If you are someone who always had a knack for constructing proofs, you will gain an even deeper appreciation for programming.

Resources

Background

Good programming skills. Understanding of formal mathematical arguments. Experience with functional programming is usefull, but definitely not necessary.

Url

Difficulty Level

High

Ethical Approval

None

Number Of Students

2

Supervisor

Marko Doko

Keywords

Degrees