From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8004 Path: news.gmane.org!not-for-mail From: matias@lifia.info.unlp.edu.ar Newsgroups: gmane.science.mathematics.categories Subject: Re: Martin-Lof type theory gentle introduction please Date: Fri, 07 Feb 2014 11:34:31 -0300 Message-ID: References: Reply-To: matias@lifia.info.unlp.edu.ar NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; DelSp="Yes"; format="flowed" Content-Transfer-Encoding: 8bit X-Trace: ger.gmane.org 1391954755 21575 80.91.229.3 (9 Feb 2014 14:05:55 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 9 Feb 2014 14:05:55 +0000 (UTC) Cc: Categories mailing list To: "Vasili I. Galchin" Original-X-From: majordomo@mlist.mta.ca Sun Feb 09 15:06:04 2014 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 1WCV1H-0002fo-Ks for gsmc-categories@m.gmane.org; Sun, 09 Feb 2014 15:06:03 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:41728) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1WCV06-0007IW-7F; Sun, 09 Feb 2014 10:04:50 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1WCV03-0002uv-R8 for categories-list@mlist.mta.ca; Sun, 09 Feb 2014 10:04:47 -0400 In-Reply-To: Content-Disposition: inline Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8004 Archived-At: Almost two decades ago I studied Type Theory in Uruguay on a course organized, if I remember correctly, by Gustavo Betarte and Alvaro Tasistro. In those times we used "Programming in Martin Lof type theory" by Nordstrom. I don't know if this is still considered to be the best introduction. In any case, anyone interested in Type Theory may also be interested in a 2000 document made recently available by Bob Walters in http://rfcwalters.blogspot.com.ar/2013/10/interview-with-bill-lawvere-by-felice.html It contains historical information that I am pretty sure is not available in other sources and that should help any newcomer to understand Type Theory in a broader categorical context. Mat?as Menni. "Vasili I. Galchin" escribi?: > Hello Cat List, > > I have downloaded many papers about Martin-Lof type theory papers > ( .... maybe I just need to pound my head against the wall like other > areas that I have I learned until a light goes on my mind?). However, > any help on gentle tutorials on this subject would be much > appreciated. > > Kind regards, > > Vasili [For admin and other information see: http://www.mta.ca/~cat-dist/ ]