coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cut Elimination Theorem

From: Carlos Olarte <carlos.olarte AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Cut Elimination Theorem
Date: Wed, 16 May 2018 20:03:43 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=carlos.olarte AT gmail.com; spf=Pass smtp.mailfrom=carlos.olarte AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f54.google.com
Ironport-phdr: 9a23:PMlgPBbU/Y2EJRuuzgo9a+X/LSx+4OfEezUN459isYplN5qZr865bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57G7ZhcN/gr9VrhKvuRJwwY3aboaOOfpiZ6PdeM8WRWpdUspPUSFKH4Oyb5EID+oEJetVsZPyp0EKrRu5HgmnGfrhyjtSiX/swa01zfkqHAba0wM6BdIOtHPUrM7vOKcVVeC61rPIzSndYP5N1jf97ZLHchElof2WQb1wds/RxFApGgjYgFuQronlMCmU1uQLq2WU9fBgVO2ui245sQ1xpSKvxsg0hobXgIIV0UnI9SF5wYYyI920UkB7YcS8HJtftiGaK4t2Qt45TG1ypCk6zbgGtJimdyYJ0JQq3xzSZvOdf4SV/B7uVPydLDRmiH5/eL+yiA6+/VW+xuD/TMW4zVhHojZfntXRtH0A1wbf58iER/Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5ocq0XDHivvlET4ia+aalwo+uao5unoeLnmqZicN4h7igH6LKsigNCwAeM9MgQWXmib//qz1KH78ED7T7hGlOA6nrfZvZzAJskXuLS1Dg9a34o77hawFTam0NAWnXkdK1JFfQqKgJTzNFHUJPD4Cuy/j06rkDdv3f/GJKHhDYvWI3jMlbfuZ7d960pGxAUvytBf4opYCqsdL/LrRk/xqNvYAwclPAyz2ubrEcly1ocDWW2UGaKZK6PTsVqQ5u01OeWMZYkVuCz8K/c//fLug2U5yhchevyi2oJSY3SlFNxnJV+YaDzimIQvC2AP6yE3VujtkxWlVTdJe3v6C6k1/DU8E8ShCY7ZWo2Fj7mI3SP9FZpTMDMVQmuQGGvlIt3XE8wHbzifd5c4w240EIO5Qopk7imA8Qrzyr5pNO3Ro3RKupfq1dwz7OrWx0hrqW5ESv+F2mTIdFla23sSTmZvjq96qE15jFyE1Pog2qEKJZlo//pMFzwCG9vcwuh9UY2gXwvAepKWTQ7jTIj6Rz42Sd01zpkFZEMvQ9g=

Dear Lourdes,

I'm aware of some proofs of cut-elimination for linear logic:
- https://perso.ens-lyon.fr/olivier.laurent/yalla/
- https://github.com/meta-logic/coq-ll

For propositional logic, I found this one:
- https://arxiv.org/abs/1503.08744

Best regards,
Carlos.

> On 16 May 2018, at 19:41, Lourdes Del Carmen Gonzalez Huesca
> <luglzhuesca AT gmail.com>
> wrote:
>
> Dear list,
>
> I was wondering if there is a formalization of Gentzen's hauptsatz or the
> cut elimination theorem.
> I have been googling with no particular results.
>
> I will really appreciate if someone can share any pointers for this or
> directions to related work in Coq.
>
>
> Many thanks!
>
> Greetings,
> Lourdes
>

[Coq-Club] Cut Elimination Theorem, Lourdes Del Carmen Gonzalez Huesca, 05/16/2018
- Re: [Coq-Club] Cut Elimination Theorem, Carlos Olarte, 05/16/2018
- Re: [Coq-Club] Cut Elimination Theorem, Daniel Schepler, 05/16/2018
  - Re: [Coq-Club] Cut Elimination Theorem, Lourdes Del Carmen Gonzalez Huesca, 05/18/2018