Proof of Kahn’s Algorithm in Coq

Raul Redpap
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
Graduation Thesis type
Bachelor - Computer Science
Kalmer Apinis
Defence year
PDF Extras