Constructive substitutes for König's lemma (artifact)

Larchey-Wendling, Dominique

doi:10.4230/artifacts.23151

Artifact

Constructive substitutes for König's lemma (artifact) Software

Author Dominique Larchey-Wendling

Part of: Collection: Supplementary Materials
License: Mozilla Public License 2.0
Publication Date: 2025-07-03

Document Identifiers

DOI: 10.4230/artifacts.23151
URN: urn:nbn:de:0030-drops-231514

Author Details

Dominique Larchey-Wendling

Université de Lorraine, CNRS, LORIA, F-54000 Nancy, France

Content

Software: https://github.com/DmxLarchey/Constructive-Konig
archived version

Version/Status

Content created at: 2024-11-28
Status: Active (at the time of publication 2025-07-03)

Cite As Get BibTex

Dominique Larchey-Wendling. Constructive substitutes for König's lemma (artifact) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/artifacts.23151

Description

This project is composed of a Coq artifact for the TYPES 2024 post-proceedings paper of the same name.

Subject Classification

Keywords

Kőnig’s lemma
FAN theorem
constructive mathematics
inductive covers
inductive bars
almost full relations
inductive type theory
Coq

Programming Languages

Coq/Rocq

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata Views

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail