coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Cut Elimination Theorem

From: Lourdes Del Carmen Gonzalez Huesca <luglzhuesca AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Cut Elimination Theorem
Date: Wed, 16 May 2018 12:41:06 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=luglzhuesca AT gmail.com; spf=Pass smtp.mailfrom=luglzhuesca AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f44.google.com
Ironport-phdr: 9a23:Y6yNQBNFvLybsxpphCUl6mtUPXoX/o7sNwtQ0KIMzox0LfnzrarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTypPAoShb4sVEuUOI/1YpJTzqVQQqRu1GBehC/n1yj9NmHD227Ax3eUmEQHA3Q0vBdYOv2rVrd7oNqkSTP66zLLUwjrZcvhb3jP96JXHchAloPCMXa9wftTKyUYzDQzIlVqQqYn/MDOU0uQBqXSU7+1lVe+2jWMstgJ/oiC3y8syloXEgpgZx1PE+Clj3oo5ON61RFR0bNOrFpZbqjuUOJFsQsw4RmFloCY6xaMCuZ68ZCUKzY4oxx/ba/CedIiI4w7vWP+fITp3i39pYr2/hxG18Uivzu3zSNO430pNripAitXMt3YN2ALP6sWfVPdx4kOs1SyM2g3T8O1IP104mKnBJ5MuzbM8jp8Tvl7CHi/ylkX2lqiWdkA89+is9uTnbbHmp56cN49plA7+KbghldakDOQ3NwgBRWmb+eCm2LL/+k35Ra1GjucqnanBrJDaOcMbq7alDA9Sy4Yv8gqwDzO70NsDhnQHN1JEeBefj4fzIV3OIfb4De2+g1u2ijtryerGbfXdBcDGKWGGm7P8d5587VRdwUw914Nx/ZVRX5UGPej/V1S5mNHcRjQwKQm5xa7ID9Nv34cTSyqvH6KCO6qa5VuV6eY9I/SBf4QckDn4IvkhofXpiClqyhcmYaC10M5POziDFfN8LhDBOCu+spI6CW4P+zEGYqnvgVyGXyRUYi/rDa057zA/TomhCNWaH9z/sPm6xC6+W6ZuSCVeEFnVSCXncoyFX7EHbyfAepY8wAxBbqCoTsoa7T/rtAL+zOA6fO/d+yldspO7kdYpu6vckhY98TEyBMOYgTmA

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