Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Is Coq SN ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is Coq SN ?


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page