coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bas Spitters <b.a.w.spitters AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Consistency of Coq ?
- Date: Fri, 7 Jul 2017 08:07:07 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f171.google.com
- Ironport-phdr: 9a23:Gqu0dhwlltCL/HfXCy+O+j09IxM/srCxBDY+r6Qd2+sfIJqq85mqBkHD//Il1AaPBtSEraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPUMVfWTFfDIygdIYPE/YNMPxEo4Xhu1cDrx2zDhSsCuP1zT9Ig2f70LAg3OQ6DArIwRQgH9MSsHTIstr1LrwSWv2ywabT1znMdela2Dnn5IjTahAhoO2MXa5ufsrL0kkiDAzFjlCKpozkOzOZzPgCs2+e7+d5U++klmApqwZ0oje1x8csjJHEiZgPylHL9CV53pw5JdqiSE50edKkEZ1QtzubN4RsWM8iTXtotSAnwbMFoZ62ZDYGxIgjyhLFaPGKc5KE7gz+WOuQOzt0mXBodK+5ih2v60av0Pf8WdOx0FtSripKjN3MtncV2hzW8MeHS/998l642TaTywzf8+9ELV02mKbGMZIhzbkwlp0csUTHACD6gln5jKiTdkk8++io7froYqn+q5OCK4N5jhvyP6cul8ClH+g0LwkDU3KG9em+ybHv5Uj5T69Ljv0ynKnZqpfaJcEDq6GiGQNayJwv6hilAze9yNQYnGUHLE5bdxKdlIjkIF7OIPXiAve+h1Sgiitkx/fDPrH5GJXCMmDDkKv9fbZ680NT1A0zzclG651IDrEBPen8V1TqtN3YCx85Kxa7z/zmCNV7zIMeWHiADrWXMKPI4he04bcEJPDET4sIsn6pIP88ovXqkHURmFkHfKDv04FBO16iGfEzCUyCKUH0g8sdHH0R9l40CuWslxuZST9Pe3uoRIoz4zg6DMStCoKVFdPlu6CIwCruRs4eXWtBEF3ZVC6wL4g=
https://coq.inria.fr/faq
"Proofs of consistency of *subsystems* of the theory of Coq can be
found in the literature."
Is this what is intended?
Proof-irrelevant model of CC with predicative induction and judgmental
equality
Lee-Werner
https://arxiv.org/abs/1111.0123
It might be good to add some references to the FAQ.
- [Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Amin Timany, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Frédéric Blanqui, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Amin Timany, 07/07/2017
Archive powered by MHonArc 2.6.18.