LVR Coq

Authors: Martin Jakomin & Mateja Rojko

Some sorting algorithms proved by Coq, created as a project work at course LVR (Logic in Computer Science). Project contains the sorting algorithms and their proof of correctness.

---

Algorithms

• Insertion Sort.
• Selection Sort (Work in progress).

Project structure

• Coq/ contains the source code:
  • Coq/insertion_sort.v contains the insertion sort and its proof.
  • Coq/selection_sort.v contains the selection sort and its proof.
  • Coq/sort_lectures.v contains some useful lemmas used in our proofs (property of Andrej Bauer)