Verified Functional Graph Algorithms using The Rocq Prover (Coq)

Frieberger, Leopold (2025) Verified Functional Graph Algorithms using The Rocq Prover (Coq). Bachelor's Thesis, Computing Science.

Preview	Text Bachelors-Thesis-Leopold-Frieberger-Repository.pdf Download (696kB) | Preview
	Text Toestemming.pdf Restricted to Registered users only Download (177kB)

Abstract

The graph data structure is used ubiquitously among computer scientists, other researchers, and in industry. In most cases, it is represented imperatively using adjacency matrices or arrays. This does not lend itself to a functional style of programming which works best on recursion over an inductively defined datatype. This mismatch is unfortunate because functional programming offers notable benefits in clarity and modularity. Given the somewhat exotic nature of functional graph representations, formal verification becomes crucial to ensure rigorous correctness and reliability. We investigate various strategies of representing graphs in functional programming and focus on the formal verification of algebraic graphs by Mokhov (2017) and inductive graphs by Erwig (2001). To this end, we use the interactive theorem prover Rocq (formerly known as Coq). Our contribution consists of developing a graph model, an initial version of a search algorithm for algebraic graphs, termination of recursively defined operations on inductive graphs, extraction to Haskell, and more.

Item Type:	Thesis (Bachelor's Thesis)
Supervisor name:	Frumin, D. and Perez Parra, J.A.
Degree programme:	Computing Science
Thesis type:	Bachelor's Thesis
Language:	English
Date Deposited:	25 Jul 2025 06:36
Last Modified:	25 Jul 2025 06:36
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/36509

Actions (login required)

View Item