coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Is Coq SN ?
- Date: Mon, 29 Feb 2016 14:42:02 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f44.google.com
- Ironport-phdr: 9a23:XydqvhMwWAAoKFapL7kl6mtUPXoX/o7sNwtQ0KIMzox0KPj6rarrMEGX3/hxlliBBdydsKIbzbSG+Pm5CSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb7isMSKM01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4+VWMfjhpBBUDh4RDkU5Ht+n/4sex82ySeMMDeQrU9WDDk5KBuHky7wBwbPiI0pTmEwvd7i7hW9Uqs
Forgive my type-theory naiveté, but shouldn't we want some part of Coq to not be strongly normalizing, so that it is possible to express and reason about non-terminating functions?
-- Jonathan
- Re: [Coq-Club] Is Coq SN ?, (continued)
- Re: [Coq-Club] Is Coq SN ?, Maxime Dénès, 02/28/2016
- Re: [Coq-Club] Is Coq SN ?, Abhishek Anand, 02/28/2016
- Re: [Coq-Club] Is Coq SN ?, roux cody, 02/28/2016
- Re: [Coq-Club] Is Coq SN ?, Luo, Zhaohui, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Frédéric Blanqui, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Frédéric Blanqui, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, roux cody, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Jonathan Leivent, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Benoît Viguier, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Jonathan Leivent, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Frédéric Blanqui, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Luo, Zhaohui, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, Thorsten Altenkirch, 02/29/2016
- Re: [Coq-Club] Is Coq SN ?, roux cody, 02/28/2016
- Re: [Coq-Club] Is Coq SN ?, Abhishek Anand, 02/28/2016
- Re: [Coq-Club] Is Coq SN ?, Maxime Dénès, 02/28/2016
Archive powered by MHonArc 2.6.18.