Proof of Kahn’s Algorithm in Coq
Name
Raul Redpap
Abstract
Coq is a functional programming language that can be used to write proofs of theorems. The purpose of the work is to investigate and provide an overview of Coq and to prove the property that Kahn’s algorithm terminates for every input and that the returned sequence is indeed a topological sorting. We mainly focus on the creation of formal proof and the description of tactics used in proofs, but also provides a brief overview of Kahn's algorithm and topological sorting.
Graduation Thesis language
Estonian
Graduation Thesis type
Bachelor - Computer Science
Supervisor(s)
Kalmer Apinis
Defence year
2019