Data

Tools

Indexes

Applications

Experiments

Open Source Science

kruskal-finite

Tools for dealing with finiteness and choice

https://github.com/dmxlarchey/kruskal-finite

Science Score: 26.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Committers with academic emails
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (5.5%) to scientific vocabulary
Last synced: 10 months ago · JSON representation

Repository

Tools for dealing with finiteness and choice

Basic Info
  • Host: GitHub
  • Owner: DmxLarchey
  • License: mpl-2.0
  • Language: Coq
  • Default Branch: main
  • Size: 41 KB
Statistics
  • Stars: 0
  • Watchers: 2
  • Forks: 0
  • Open Issues: 0
  • Releases: 6
Created over 2 years ago · Last pushed over 1 year ago
Metadata Files
Readme License Authors Codemeta

README.md

(**************************************************************) (* Copyright Dominique Larchey-Wendling [*] *) (* *) (* [*] Affiliation LORIA -- CNRS *) (**************************************************************) (* This file is distributed under the terms of the *) (* Mozilla Public License Version 2.0, MPL-2.0 *) (**************************************************************)

What is this library?

This sub-project is part of the larger project Coq-Kruskal described here: https://github.com/DmxLarchey/Coq-Kruskal.

This is a collection of Coq 8.14+ tools based on the following notion of finiteness - a type is finite if it is listable: there is a (computable) list collecting all its members - a predicate is finite if its span is listable

Dependencies

There is a dependency with Kruskal-Trees because: - in the finite.v file, we prove finiteness results about the types idx n and vec X n which are actually defined in Kruskal-Trees; - in the examples/trees.v, we moreover show that there are finitely many rose trees (ie arbitrarily but finite branching trees) of a given (or bounded) number of nodes, and we need rtree X and ltree X (and also list_sum).

How to install

This library is CI tested with Coq 8.14-8.20 and should install smoothly with opam install coq-kruskal-finite.

Owner

  • Name: Dominique Larchey-Wendling
  • Login: DmxLarchey
  • Kind: user
  • Location: Nancy, France
  • Company: CNRS

CodeMeta (codemeta.json) 

{
  "@context": "https://doi.org/10.5063/schema/codemeta-2.0",
  "type": "SoftwareSourceCode",
  "author": [
    {
      "id": "https://orcid.org/0000-0001-9860-7203",
      "type": "Person",
      "affiliation": {
        "type": "Organization",
        "name": "Departement of Formal Method, TYPES team, LORIA, CNRS"
      },
      "email": "dominique.larchey-Wendling@loria.fr",
      "familyName": "Larchey-Wendling",
      "givenName": "Dominique"
    }
  ],
  "codeRepository": "git+https://github.com/DmxLarchey/Kruskal-Finite.git",
  "dateCreated": "2024-01-19",
  "dateModified": "2024-11-21",
  "datePublished": "2024-01-19",
  "description": "This is a collection of tools to abstractly manipulate the notion of finiteness in Coq.",
  "downloadUrl": "https://github.com/DmxLarchey/Kruskal-Finite/archive/refs/tags/1.5.tar.gz",
  "funder": {
    "type": "Organization",
    "name": "CNRS"
  },
  "isPartOf": "https://github.com/DmxLarchey/Coq-Kruskal",
  "keywords": [
    "coq",
    "rose trees",
    "dependent types",
    "Kruskal tree theorem"
  ],
  "license": "https://spdx.org/licenses/MPL-2.0",
  "name": "Kruskal-Finite",
  "operatingSystem": [
    "Linux",
    "MacOS"
  ],
  "programmingLanguage": "Coq",
  "softwareRequirements": "opam, ocaml",
  "version": "1.5",
  "developmentStatus": "active",
  "issueTracker": "https://github.com/DmxLarchey/Kruskal-Finite/issues"
}

GitHub Events

Total
  • Release event: 3
  • Delete event: 2
  • Push event: 4
  • Pull request event: 1
  • Create event: 3
Last Year
  • Release event: 3
  • Delete event: 2
  • Push event: 4
  • Pull request event: 1
  • Create event: 3

Committers

Last synced: about 1 year ago

All Time
  • Total Commits: 20
  • Total Committers: 1
  • Avg Commits per committer: 20.0
  • Development Distribution Score (DDS): 0.0
Past Year
  • Commits: 5
  • Committers: 1
  • Avg Commits per committer: 5.0
  • Development Distribution Score (DDS): 0.0
Top Committers
Name Email Commits
Dominique Larchey-Wendling l****y@g****m 20

Issues and Pull Requests

Last synced: about 1 year ago

All Time
  • Total issues: 0
  • Total pull requests: 5
  • Average time to close issues: N/A
  • Average time to close pull requests: about 8 hours
  • Total issue authors: 0
  • Total pull request authors: 1
  • Average comments per issue: 0
  • Average comments per pull request: 0.0
  • Merged pull requests: 5
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 1
  • Average time to close issues: N/A
  • Average time to close pull requests: 16 minutes
  • Issue authors: 0
  • Pull request authors: 1
  • Average comments per issue: 0
  • Average comments per pull request: 0.0
  • Merged pull requests: 1
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
Pull Request Authors
  • DmxLarchey (9)
Top Labels
Issue Labels
Pull Request Labels

Dependencies

.github/workflows/main.yml actions
  • actions/checkout v2 composite
  • coq-community/docker-coq-action v1 composite