coq-library-undecidability
coq-library-undecidability copied to clipboard
uds-psl
A library of mechanised undecidability proofs in the Coq proof assistant.
Universal, binary Turing machine with 1 tape The construction is via a universal Krivine machine simulation.
We currently have - `MM 2` two-counter Minsky machines - `MM2` two-counter (alternative) Minsky machines - `MMA 2` two-counter (alternative) Minsky machines - ~`CM2`~ two-counter (alternative) Minsky machines Much of...
This is a draft PR for switching from `MM n` to `MMA n` to put `MMA` upfront in place of `MM`. The list of included reduction so far: - `BSM...
Goals of this PR: - Top-level (universal) Turing machine halting `Definition HaltUTM : tape (finType_CS bool) -> Prop := fun t => HaltsTM UTM [t].` and `Lemma HaltUTM_undec : undecidable...
This PR contributes the undecidability of several first-order axiomatisations of finitary set theories and classical arithmetic. The code was developed with @HermesMarc during preparation of the [extended version](https://www.ps.uni-saarland.de/extras/axiomatisations-ext/) of our...
This PR intends to answer a request from Yves Bertot concerning the undecidability of equality testing between (constructive) real numbers. For the moment, the PR implements the following problems, but...
When @dominik-kirst was hunting the universe problem, I tried to create a dependency graph of the library, but without success. With the help of the Enrico Tassi I managed to...
Hi @yforster, I am not sure if this is a bug but in the current configuration under my fork of `coq-8.12`, the `CI` is launched after every push, _even if...
As pointed out in (https://github.com/coq/coq/issues/10459) and (https://github.com/coq/coq/issues/13584), semantics of `Let ... Qed.` are not coherent / future proof, and also slow down interface file `vos` compilation. Currently, the library contains...
Currently, after each PR the CI runs `opam upgrade` each time resulting in `upgrade coq 8.12.0 to 8.12.1`. This should be done by the cache (and run only once) which...