stablesort/rocq-stablesort.opam at master · pi8027/stablesort · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
# 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@ens-lyon.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 Rocq"
description: """
This library provides a characterization of stable mergesort functions using
relational parametricity, and deduces several functional correctness results,
including stability, solely from the characteristic property. This library
allows the users to prove their mergesort correct just by proving that the
mergesort in question satisfies the characteristic property. The functional
correctness lemmas are overloaded using a canonical structure
(`StableSort.function`) that bundles the characteristic property, and
automatically apply to any declared instance of this structure.

As instances of the characteristic property, this library provides two kinds
of optimized mergesorts.
The first kind is non-tail-recursive mergesort. In call-by-need evaluation,
they compute the first k smallest elements of a list of length n in
O(n + k log k) time, which is known to be the optimal 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.
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}%"]
run-test: [make "-j%{jobs}%" "build-icfp25"]
install: [make "install"]
depends: [
  "coq" {>= "8.19"}
  "coq-mathcomp-ssreflect" {>= "2.3.0"}
  "coq-paramcoq" {>= "1.1.3"}
  "coq-mathcomp-zify" {with-test}
  "coq-equations" {with-test}
]

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