Published March 2, 2022 | Version v1
Publication Metadata-only

A Formalisation of Algorithms for Sorting Network

Théry, Laurent
Other:
Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Description

This notes explains how standard algorithms that construct sorting networks have been formalised and proved correct in the Coq proof assistant using the SSReflect extension.

Additional details

Identifiers Origin repository
Created:
December 3, 2022
Modified:
December 1, 2023