constructive-konig

Coq artifact for "Constructive substitutes for König's lemma"

https://github.com/dmxlarchey/constructive-konig

Science Score: 44.0%

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

✓
CITATION.cff file
Found CITATION.cff file
✓
codemeta.json file
Found codemeta.json file
✓
.zenodo.json file
Found .zenodo.json file
○
DOI references
○
Academic publication links
○
Academic email domains
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (9.1%) to scientific vocabulary

Last synced: 6 months ago · JSON representation ·

Repository

Coq artifact for "Constructive substitutes for König's lemma"

Basic Info

Host: GitHub
Owner: DmxLarchey
License: mpl-2.0
Language: Rocq Prover
Default Branch: main
Size: 191 KB

Statistics

Stars: 0
Watchers: 1
Forks: 0
Open Issues: 0
Releases: 0

Created about 1 year ago · Last pushed 8 months ago

Metadata Files

Readme License Citation Authors Codemeta

(**************************************************************) (* 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 *) (**************************************************************)

Constructive substitutes for Knig's lemma (artifact)

This project is composed of the Coq artifact for the TYPES 2024 post-proceedings paper Constructive substitutes for Knig's lemma by Dominique Larchey-Wendling, to be published circa mid july 2025 as LIPIcs volume 336.

The standalone Coq file constructive_konig.v contains the developement and is largely commented. It has minimal dependencies, only on the standard library (distributed with Coq), and only on the List, Arith, Lia, Permutation and Utf8 modules within the standard library. It is intented to be read and executed within an IDE for Coq such as eg CoqIDE or vscoq.

Any version of Coq starting from 8.14 and up to at least 8.20 should be ok to compile and/or review the file constructive_konig.v. Since this is a single file, there is no need to pre-compile before reviewing.

Remarks

Concerning the use of Utf8 symbols in the code, we did not experience any display issues with CoqIDE in any of the opam installed versions from 8.14 and 8.20. Similarly, viewing the code in the Chrome browser directly on GitHub looks fine on our systems. Depending on the operating system, distribution or the IDE/browser, such issues might possibly arise if OS installed Utf8 symbols are incomplete/inconsistent with the IDE/browser.

Anyway, to possibly avoid such issues, we suggest the usage of an opam installed version of CoqIDE rather than the default OS version of the tool. This also allows to easily switch between different versions of Coq when developping general purpose code.

Owner

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

Repositories: 9
Profile: https://github.com/DmxLarchey

Citation (CITATION.cff)

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
  - family-names: Larchey-Wendling
    given-names: Dominique
    orcid: https://orcid.org/0000-0001-9860-7203
title: "Constructive substitutes for König's lemma (artifact)"
version: 1.0
date-released: 2024-11-28
url: https://github.com/DmxLarchey/Constructive-Konig

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": "https://github.com/DmxLarchey/Constructive-Konig",
  "dateCreated": "2024-11-28",
  "datePublished": "2024-12-04",
  "description": "This project is composed of the Coq artifact for the TYPES 2024 post-proceedings paper \"Constructive substitutes for Knig's lemma\" by Dominique Larchey-Wendling, to be published circa mid july 2025 as LIPIcs volume 336.",
  "funder": {
    "type": "Organization",
    "name": "CNRS"
  },
  "keywords": [
    "Knigs lemma",
    "FAN theorem",
    "constructive mathematics",
    "inductive covers",
    "inductive bars",
    "almost full relations",
    "inductive type theory",
    "Coq"
  ],
  "license": "https://spdx.org/licenses/MPL-2.0",
  "name": "Constructive substitutes for Knig's lemma (artifact)",
  "operatingSystem": [
    "Linux",
    "MacOS"
  ],
  "programmingLanguage": "Coq/Rocq",
  "softwareRequirements": "https://github.com/rocq-prover",
  "developmentStatus": "active"
}

GitHub Events

Total

Push event: 20
Pull request event: 2
Create event: 4

Last Year

Push event: 20
Pull request event: 2
Create event: 4

Issues and Pull Requests

Last synced: 11 months ago

All Time

Total issues: 0
Total pull requests: 1
Average time to close issues: N/A
Average time to close pull requests: 1 day
Total issue authors: 0
Total 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

Past Year

Issues: 0
Pull requests: 1
Average time to close issues: N/A
Average time to close pull requests: 1 day
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

ecosyste.ms

Data

Tools

Indexes

Applications

Experiments

Open Source Science