coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A library of undecidable problems for Coq

From: Yannick Forster <forster AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] A library of undecidable problems for Coq
Date: Mon, 25 Feb 2019 18:02:26 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=forster AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=forster AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT thyone.hiz-saarland.de
Ironport-phdr: 9a23:s9t/9BCw8pB2lZIruWD3UyQJP3N1i/DPJgcQr6AfoPdwSPT5o8bcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzUhMJ+gq1Urw6uqRNkzo7IYoyYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d4YADfAOPeBer4n8u1QOrga1CwmrBOP10T9ImmH53bcn2OkmHwHG2xYgH8kSsHvKttX4L78SUfuvwKnVyzXDbupa2Szn54fSaBAhpeuDXbRtfsbL1EYgCRrIg1ONooLrODOV0/4Cs2md7+d4WuKvinInqwFsoje03Msjlo7JhocNxlDZ8yV5wZ85JcaiR0Fhe96kFIFftyeHOIdsX8wtXWdlszs5xL0eoZO3YSYHxZs9yxPbavGLaYqF7gj9WOufPzt0nG9pdbywihqo9UWty/fwWtS33VtLtCZJj9rBu3YQ3BLJ8MeHUOFy/kK51DaPyQ/T7uZELFgolarbK58hxbgwmYQJvUTDHy/3mVz6jLSMeUo+4Oio7/7oYrP7qZOGKoB7lBnyMqUomsOhHeQ1KhUCUmaU9Oim0LDu/Ff1TbdQgvEonKTVrojWJcEBqa64Bw9V3Jwj6xG6Dzq+3tQYmmMHLElZeB2ZlYjkIEnOIOviAfeihVSskS5nx+vcMbL7GJXNKmLMkLH8crpn9kFT1hI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioynkZYdq2017MWbmq5F7JoORa3e33p1+YIF2ELtQl2Yuvwk0GPS3YHaXGoRL4x/BkjE8S7C4aGXYmkmriI2iv9EpAANTMOMUyFDXq9L9bMYPwLci/HepYwwAxBbqCoTsoa7T/rsQb7z7R9Ke+Oon8ArtT+0tkw/OTajxU78zAyA8nPijjRHVExpXsBQnoN5I46uVZ0kA/RybM+nvpZUMda7ulNWwE2c5LRnbQjVoLCHznZd9LMc26IB9WrBTZrEoAtw84JZUs7G9SwywvK1jCuCrkZ0bCGVsQ5

Dear Coq-Clubbers,

we're happy to announce our library of undecidable problems in Coq,
compatible with Coq 8.8 and 8.9:

https://github.com/uds-psl/coq-library-undecidability

The library is based on a synthetic approach to undecidability proofs
relying on the computability of all functions definable in Coq. The
library already contains many well-known problems, including the following:

- The halting problems for Turing machines, Minsky machines and the
call-by-value lambda-calculus
- The Post correspondence problem
- Provability in linear logic and first-order logic
- Solvability of Diophantine equations, including a formalisation of the DPRM theorem

The library is maintained by Dominique Larchey-Wendling and myself. Contributors to the library include Edith Heither, Dominik Kirst and Gert Smolka. There are links to relevant published work on the website.

Feel free to open an issue or send us an email if you think about doing
formal undecidability proofs or want to contribute to the library!

Yannick

--
PhD student, Programming Systems Lab, Saarland University
https://www.ps.uni-saarland.de/~forster/

[Coq-Club] A library of undecidable problems for Coq, Yannick Forster, 02/25/2019