GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → uds-psl → coq-library-undecidability

uds-psl / coq-library-undecidability

Licence: other
A library of mechanised undecidability proofs in the Coq proof assistant.

Programming Languages

Coq
218 projects

Labels

coq

Projects that are alternatives of or similar to coq-library-undecidability

toychain
A minimalistic blockchain consensus implemented and verified in Coq
Stars: ✭ 103 (+22.62%)
Mutual labels:  coq
Actuary
Formalization of the basic actuarial mathematics using Coq
Stars: ✭ 17 (-79.76%)
Mutual labels:  coq
system-F
Formalization of the polymorphic lambda calculus and its parametricity theorem
Stars: ✭ 20 (-76.19%)
Mutual labels:  coq
coq-ecosystem
No description or website provided.
Stars: ✭ 39 (-53.57%)
Mutual labels:  coq
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Stars: ✭ 62 (-26.19%)
Mutual labels:  coq
coqdocjs
Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]
Stars: ✭ 28 (-66.67%)
Mutual labels:  coq
coq-100-theorems
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
Stars: ✭ 41 (-51.19%)
Mutual labels:  coq
bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
Stars: ✭ 20 (-76.19%)
Mutual labels:  coq
coq-tal
Formalization of Typed Assembly Language (TAL) in Coq
Stars: ✭ 15 (-82.14%)
Mutual labels:  coq
PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Stars: ✭ 43 (-48.81%)
Mutual labels:  coq
stablesort
Stable sort algorithms and their stability proofs in Coq
Stars: ✭ 19 (-77.38%)
Mutual labels:  coq
koika
A core language for rule-based hardware design 🦑
Stars: ✭ 103 (+22.62%)
Mutual labels:  coq
hs-to-coq
Convert Haskell source code to Coq source code.
Stars: ✭ 64 (-23.81%)
Mutual labels:  coq
CoqCheatSheet
Reference sheet for the Coq language.
Stars: ✭ 15 (-82.14%)
Mutual labels:  coq
kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Stars: ✭ 119 (+41.67%)
Mutual labels:  coq
coq-elpi
Coq plugin embedding elpi
Stars: ✭ 92 (+9.52%)
Mutual labels:  coq
hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Stars: ✭ 38 (-54.76%)
Mutual labels:  coq
coq-program-verification-template
Template project for program verification in Coq
Stars: ✭ 26 (-69.05%)
Mutual labels:  coq
imm
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Stars: ✭ 15 (-82.14%)
Mutual labels:  coq
opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Stars: ✭ 101 (+20.24%)
Mutual labels:  coq
View All Similar Projects ➔

Coq Library of Undecidability Proofs

CI

The Coq Library of Undecidability Proofs contains mechanised reductions to establish undecidability results in Coq. The undecidability proofs are based on a synthetic approach to undecidability. A problem P is considered undecidable if its decidability in Coq implies the enumerability of the complement of halting problem for Turing machines (SBTM_HALT in TM/SBTM.v). Since the Turing machine halting is enumerable (SBTM_HALT_enum in TM/SBTM_enum.v), enumerability of its complement would classically imply its decidability.

As in the traditional literature, undecidability of a problem P in the library is often established by constructing a many-one reduction from an undecidable problem to P.

For more information on the structure of the library, the synthetic approach, and included problems see Publications below, our Wiki, look at the slides or the recording of the talk on the Coq Library of Undecidability proofs at CoqPL '20.

The library is a collaborative effort, growing constantly and we invite everybody to contribute undecidability proofs!

Problems in the Library

The problems in the library can mostly be categorized into seed problems, advanced problems, and target problems.

Seed problems are simple to state and thus make for good starting points of undecidability proofs, often leading to easier reductions to other problems.

Advanced problems do not work well as seeds, but they highlight the potential of our library as a framework for mechanically checking pen&paper proofs of potentially hard undecidability results.

Target problems are very expressive and thus work well as targets for reduction, with the aim of closing loops in the reduction graph to establish the inter-reducibility of problems.

Seed Problems

Advanced Problems

Halting Problems for Traditional Models of Computation

  • Halting problem for the weak call-by-value lambda-calculus (HaltL in L/L.v)
  • Halting problem for multi-tape Turing machines (HaltMTM in TM/TM.v)
  • Halting problem for single-tape Turing machines (HaltTM 1 in TM/TM.v)
  • Halting problem for simple binary single-tape Turing machines (HaltSBTM in TM/SBTM.v)
  • Halting problem for program counter based binary single-tape Turing machines (PCTM_HALT in TM/PCTM.v)
  • Halting problem for Binary Stack Machines (BSM_HALTING in StackMachines/BSM.v)
  • Halting problems for Minsky machines (MM_HALTING and MMA_HALTING n in MinskyMachines/MM.v)
  • Halting problem for partial recursive functions (MUREC_HALTING in MuRec/recalg.v)
  • Halting problem for the weak call-by-name lambda-calculus (wCBN in LambdaCalculus/wCBN.v)

An equivalence proof that most of the mentioned models of computation compute the same n-ary functional relations over natural numbers is available in Models_Equivalent.v.

Problems from Logic

  • Provability in Minimal, Intuitionistic, and Classical First-Order Logic (FOL*_prv_intu, FOL_prv_intu, FOL_prv_class in FOL/FOL.v), including a formulation for the minimal binary signature (FOL/binFOL.v)
  • Validity in Minimal and Intuitionistic First-Order Logic (FOL*_valid, FOL_valid_intu in FOL/FOL.v)
  • Satisfiability in Minimal and Intuitionistic First-Order Logic (FOL*_satis, FOL_satis_intu in FOL/FOL.v)
  • Finite satisfiability in First-Order Logic, known as "Trakhtenbrot's theorem" (FSAT in FOL/FSAT.v based on TRAKHTENBROT/red_utils.v)
  • Semantic and deductive entailment in first-order ZF set-theory with (FOL/ZF.v) and without (FOL/minZF.v and FOL/binZF.v) function symbols for set operations
  • Semantic and deductive entailment in Peano arithmetic (FOL/PA.v)
  • Entailment in Elementary Intuitionistic Linear Logic (EILL_PROVABILITY in ILL/EILL.v)
  • Entailment in Intuitionistic Linear Logic (ILL_PROVABILITY in ILL/ILL.v)
  • Entailment in Classical Linear Logic (CLL_cf_PROVABILITY in ILL/CLL.v)
  • Entailment in Intuitionistic Multiplicative Sub-Exponential Linear Logic (IMSELL_cf_PROVABILITY3 in ILL/IMSELL.v)
  • Provability in Hilbert-style calculi (HSC_PRV in HilbertCalculi/HSC.v)
  • Recognizing axiomatizations of Hilbert-style calculi (HSC_AX in HilbertCalculi/HSC.v)
  • Satisfiability in Separation Logic (SLSAT in SeparationLogic/SL.v and MSLSAT in SeparationLogic/MSL.v)
  • Validity and satisfiability in Second-Order Peano Arithmetic (SOL/PA2.v)
  • Validity and satisfiability in Second-Order Logic in the empty signature (SOL/SOL.v)

Other Problems

Target Problems

  • Halting problem for the call-by-value lambda-calculus (HaltL in L/L.v)
  • Validity, provability, and satisfiability in First-Order Logic (all problems in FOL/FOL.v)

Installation Instructions

If you can use opam 2 on your system, you can follow the instructions here.

Install from released package via opam

This installation method only works if the opam package is already released. Make sure you have done opam update and check the output of opam info coq-library-undecidability to see whether a package is available. If no package is available, use one of the two methods below.

We recommend creating a fresh opam switch:

opam switch create coq-library-undecidability 4.07.1+flambda
eval $(opam env)

Then the following commands install the library:

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq-library-undecidability.1.0.1+8.15

Install from git via opam

You can use opam to install the current state of this branch as follows.

We recommend creating a fresh opam switch:

opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda
eval $(opam env)

Then the following commands install the library:

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam pin add coq-library-undecidability.dev+8.15 "https://github.com/uds-psl/coq-library-undecidability.git#coq-8.15"

Manual installation

You need Coq 8.15 built on OCAML >= 4.07.1, the Smpl package, the Equations package, and the MetaCoq package for Coq. If you are using opam 2 you can use the following commands to install the dependencies on a new switch:

opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install . --deps-only

Building the undecidability library

  • make all builds the library
  • make TM/TM.vo compiles only the file theories/TM/TM.v and its dependencies
  • make html generates clickable coqdoc .html in the website subdirectory
  • make clean removes all build files in theories and .html files in the website directory

Compiled interfaces

The library is compatible with Coq's compiled interfaces (vos) for quick infrastructural access.

  • make vos builds compiled interfaces for the library
  • make vok checks correctness of the library

Troubleshooting

Windows

If you use Visual Studio Code on Windows 10 with Windows Subsystem for Linux (WSL), then local opam switches may cause issues. To avoid this, you can use a non-local opam switch, i.e. opam switch create 4.07.1+flambda.

Coq version

Be careful that this branch only compiles under Coq 8.15. If you want to use a different Coq version you have to change to a different branch. Due to compatibility issues, not every branch contains exactly the same problems. We recommend to use the newest branch if possible.

Publications

Papers and abstracts on the library

A Coq Library of Undecidable Problems. Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, Maximilian Wuttke. CoqPL '20. https://popl20.sigplan.org/details/CoqPL-2020-papers/5/A-Coq-Library-of-Undecidable-Problems

Computability in Constructive Type Theory. Yannick Forster. PhD thesis. https://dx.doi.org/10.22028/D291-35758

Papers and abstracts on problems and proofs included in the library

How to contribute

Fork the project on GitHub, add a new subdirectory for your project and your files, then file a pull request. We have guidelines for the directory structure of projects.

Contributors

  • Yannick Forster
  • Dominique Larchey-Wendling
  • Andrej Dudenhefner
  • Edith Heiter
  • Marc Hermes
  • Johannes Hostert
  • Dominik Kirst
  • Mark Koch
  • Fabian Kunze
  • Gert Smolka
  • Simon Spies
  • Dominik Wehr
  • Maximilian Wuttke

Parts of the Coq Library of Undecidability Proofs reuse generic code initially developed as a library for the lecture "Introduction to Computational Logics" at Saarland University, which was written by a subset of the above contributors, Sigurd Schneider, and Jan Christian Menz.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].