Coq Library of Undecidability Proofs version 1.1.2+8.20

What's Changed

• Higher-order beta-matching by @mrhaandi in #220

Coq Library of Undecidability Proofs version 1.1.1+8.18

Change license from CeCILL v2 to MPL-2.0 (more permissive) (#208)

* relicense to MPL-2.0 using a script

* changing license field in opam file, thx to @Zimmi48

* renamed MPL-2.0 license file for GitHub automatic recognition

Coq Library of Undecidability Proofs version 1.1+8.17

v1.1+8.17

Merge pull request #195 from mrhaandi/prepare-8.17

Coq Library of Undecidability Proofs version 1.1

Merge pull request #190 from JoJoDeveloping/coq-8.16

Remove dependency on Synthetic.Undecidability for non-_undec files

Coq Library of Undecidability Proofs version 1.0.1

This release is intended to serve as the base for a release of coq-library-complexity.1.0+8.16.

It will almost immediately be succeeded by a release of v1.1.

Trakhtenbrot in Coq, IJCAR 2020 selected papers (LMCS) v1.1

This release is tailored version of the Coq Library of Undecidability Proofs focusing on the TRAKHTENBROT development and in sync with the submission of an extended version for the selected papers of IJCAR 2020 paper, submitted to LMCS via Arxiv:

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens by Dominik Kirst and Dominique Larchey-Wendling

An overview file called summary.v is provided which links the results list in the submission with source code references. Please consult the README.md file for compilations instructions.

Hilbert Tenth problem in Coq (LMCS) v1.1

Hilbert’s Tenth problem in Coq

Dominique Larchey-Wendling [email protected], Yannick Forster [email protected]

This repository contains the Coq formalisation of the paper Hilbert’s tenth problem in Coq, submitted as a revised preprint to Logical Methods in Computer Science. Consult the README.md for installation instructions.

Trakhtenbrot in Coq, IJCAR 2020 selected papers (LMCS) v1.0

This release is tailored version of the Coq Library of Undecidability Proofs focusing on the TRAKHTENBROT development and in sync with the submission of an extended version for the selected papers of IJCAR 2020 paper, submitted to LMCS via Arxiv:

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens by Dominik Kirst and Dominique Larchey-Wendling

An overview file called summary.v is provided which links the results list in the submission with source code references. Please consult the README.md file for compilations instructions.

FSCD 2021 v1.0

Synthetic Undecidability of MSELL via FRACTRAN (FSCD 2021)

This repository is a tailored/frozen version of the Coq Library of Undecidability Proofs designed to provide a faster path towards code review of the FSCD'21 paper Synthetic Undecidability of MSELL via FRACTRAN mechanised in Coq by Dominique Larchey-Wendling.

Coq Library of Undecidability Proofs version 1.0.0

v1.0.0+8.12

Cleanup coqdoc and _CoqProject (#97)