coq-stablesort.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "kazuhiko.sakaguchi@inria.fr"
version: "dev"

homepage: "https://github.com/pi8027/stablesort"
dev-repo: "git+https://github.com/pi8027/stablesort.git"
bug-reports: "https://github.com/pi8027/stablesort/issues"
license: "CECILL-B"

synopsis: "Stable sort algorithms and their stability proofs in Coq"
description: """
This library provides a generic and modular way to prove the correctness,
including stability, of several mergesort functions. The correctness lemmas in
this library are overloaded using a canonical structure
(`StableSort.function`). This structure characterizes stable mergesort
functions, say `sort`, by its abstract version `asort` parameterized over the
type of sorted lists and its operators such as merge, the relational
parametricity of `asort`, and two equational properties that `asort`
instantiated with merge and concatenation are `sort` and the identity
function, respectively, which intuitively mean that replacing merge with
concatenation turns `sort` into the identity function.
From this characterization, we derive an induction principle over
traces—binary trees reflecting the underlying divide-and-conquer structure of
mergesort—to reason about the relation between the input and output of
`sort`, and the naturality of `sort`. These two properties are sufficient to
deduce several correctness results of mergesort, including stability. Thus,
one may prove the stability of a new sorting function by defining its abstract
version, proving the relational parametricity of the latter using the
parametricity translation (the Paramcoq plugin), and manually providing the
equational properties.

As an application of the above proof methodology, this library provides two
kinds of optimized mergesorts.
The first kind is non-tail-recursive mergesort. In call-by-need evaluation,
they allow us to compute the first k smallest elements of a list of length n
in the optimal O(n + k log k) time complexity of the partial and incremental
sorting problems. However, the non-tail-recursive merge function linearly
consumes the call stack and triggers a stack overflow in call-by-value
evaluation.
The second kind is tail-recursive mergesorts and thus solves the above issue
in call-by-value evaluation. However, it does not allow us to compute the
output incrementally regardless of the evaluation strategy.
Therefore, there is a performance trade-off between non-tail-recursive and
tail-recursive mergesorts, and the best mergesort function for lists depends
on the situation, in particular, the evaluation strategy and whether it should
be incremental or not.
In addition, each of the above two kinds of mergesort functions has a smooth
(also called natural) variant of mergesort, which takes advantage of sorted
slices in the input."""

build: [make "-j%{jobs}%"]
# The filter below has been added by hand to avoid running the test suite with
# Coq 8.17.
run-test: [ [make "-j%{jobs}%" "build-misc" ] { coq:version < "8.17~" | "8.18~" <= coq:version } ]
install: [make "install"]
depends: [
  "coq" {>= "8.13"}
  "coq-mathcomp-ssreflect" {>= "1.13.0"}
  "coq-paramcoq" {>= "1.1.3"}
  "coq-mathcomp-zify" {with-test}
  "coq-equations" {with-test}
]

tags: [
  "logpath:stablesort"
]
authors: [
  "Kazuhiko Sakaguchi"
  "Cyril Cohen"
]