Verification of Integers and Sorting Algorithms in Coq

Project: Research

Project Details

Description

A short project using the Coq proof assistant to explore multiple different definitions of the integers and various properties of them (such as the sign of an integer, or an ordering on the integers), and defining multiple different definitions of sorting algorithms and proving various properties of them (such as proving that insertion sort is a sorting algorithm). Both of these are from scratch, i.e. without relying on the vast majority of the Coq standard library.

Key findings

Key outcomes include exploring different higher inductive definitions of the integers and successfully proving that they coincide (i.e. are ring isomorphic), and exploring different definitions of sorting algorithms and proving that they coincide (e.g. inductive definitions are equivalent to recursive definitions).

Notable outcomes include machine-verifiable proofs of the triangle inequality and verification of insertion sort. Project scope was reduced due to falling ill with COVID-19 during December/January.
StatusFinished
Effective start/end date9/11/2118/01/22

Keywords

  • coq
  • functional programming
  • type theory
  • verification
  • mathematics
  • algorithm
  • sorting algorithm