From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7756 Path: news.gmane.org!not-for-mail From: Urs Schreiber Newsgroups: gmane.science.mathematics.categories Subject: Re: Publicity Date: Sat, 8 Jun 2013 22:30:02 +0200 Message-ID: References: Reply-To: Urs Schreiber NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: ger.gmane.org 1370814166 30240 80.91.229.3 (9 Jun 2013 21:42:46 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 9 Jun 2013 21:42:46 +0000 (UTC) To: "categories@mta.ca" Original-X-From: majordomo@mlist.mta.ca Sun Jun 09 23:42:48 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1UlnNu-00089I-Ul for gsmc-categories@m.gmane.org; Sun, 09 Jun 2013 23:42:47 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:39317) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1UlnMg-0007e6-DL; Sun, 09 Jun 2013 18:41:30 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1UlnMg-0007Ap-KG for categories-list@mlist.mta.ca; Sun, 09 Jun 2013 18:41:30 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7756 Archived-At: On 6/8/13, Marta Bunge wrote: > The assertion "the theory of programming > languages and the field of logic can be seen as essentially identical to > category theory " is pure nonsense, even more so as it is given an > outrageous name - "computational trinitarianism" even if spoken in jest. The term "computational trinitarianism" http://ncatlab.org/nlab/show/computational+trinitarianism refers to the theorem relating category theory and type theory http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory The further relation between type theory to logic and programming languages is similarly well established. The term "computational trinitarianism" was invented by Bob Harper in an expositional blog post http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ designed to alert an unspecialized public about these nice and useful facts. I guess that's what the author of that article about Spivak's paper picked up. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]