From 1c6f4dd29b3f838f633f1109755a0950a02d7f86 Mon Sep 17 00:00:00 2001 From: Mark Farrell Date: Sun, 30 Aug 2015 19:48:37 +0000 Subject: [PATCH 1/6] Add Type Theory and Functional Programming --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 8aeaa6b..fb0b26a 100644 --- a/README.md +++ b/README.md @@ -51,6 +51,10 @@ read closely on a second pass. * [Online supplements](http://www.cis.upenn.edu/~bcpierce/attapl/) * [Dead-tree copy](http://www.amazon.com/exec/obidos/ASIN/0262162288/benjamcpierce) + + - Type Theory and Functional Programming (TTFP) + + * [Online Copy](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf) ### Proof Assistants From 9350826c8a4e792615b8aac3a7058df94f539b53 Mon Sep 17 00:00:00 2001 From: Mark Farrell Date: Tue, 1 Sep 2015 11:11:36 +0000 Subject: [PATCH 2/6] Update README.md --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index fb0b26a..f597afc 100644 --- a/README.md +++ b/README.md @@ -16,6 +16,10 @@ read closely on a second pass. ## The Resources +### IRC Channel + + - ```##typetheory``` on ```irc.freenode.net```. + ### Textbooks - Practical Foundations of Programming Languages (PFPL) From 74f3cb88cbadbf6e509a40ee7f9f30318f1524b9 Mon Sep 17 00:00:00 2001 From: Steven Shaw Date: Tue, 13 Oct 2015 23:14:08 +1000 Subject: [PATCH 3/6] Update PFPL to 2nd edition --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index f597afc..b7b1e22 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,7 @@ read closely on a second pass. but I think PFPL does a better job explaining the foundations it works from and then covers more topics I find interesting. - * [Online copy](http://www.cs.cmu.edu/~rwh/plbook/1sted-revised.pdf) + * [Online copy](http://www.cs.cmu.edu/~rwh/plbook/2nded.pdf) * [Dead-tree copy](http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570/ref=sr_1_1?ie=UTF8&qid=1439346858&sr=8-1&keywords=practical+foundations+for+programming+languages) - Types and Programming Languages (TAPL) From abba98c26bd2481985adf89886fc7cca0575aa0f Mon Sep 17 00:00:00 2001 From: Mark Farrell Date: Sat, 28 Nov 2015 10:58:54 -0500 Subject: [PATCH 4/6] Add Practical Foundations of Mathematics --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index b7b1e22..a52e857 100644 --- a/README.md +++ b/README.md @@ -59,6 +59,10 @@ read closely on a second pass. - Type Theory and Functional Programming (TTFP) * [Online Copy](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf) + + - Practical Foundations of Mathematics (PFM) + + * [Online Copy](http://www.paultaylor.eu/~pt/prafm/html/) ### Proof Assistants From 5a6731b9e23bf5b3838f1b46d9e2252a0f613680 Mon Sep 17 00:00:00 2001 From: Mark Farrell Date: Wed, 9 Dec 2015 10:43:00 -0500 Subject: [PATCH 5/6] Update README.md --- README.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/README.md b/README.md index a52e857..22da131 100644 --- a/README.md +++ b/README.md @@ -16,10 +16,6 @@ read closely on a second pass. ## The Resources -### IRC Channel - - - ```##typetheory``` on ```irc.freenode.net```. - ### Textbooks - Practical Foundations of Programming Languages (PFPL) From 4ec748a54ac10d2e7d5333827e5e9c744cd18f88 Mon Sep 17 00:00:00 2001 From: Mark Farrell Date: Tue, 15 Dec 2015 13:35:01 -0500 Subject: [PATCH 6/6] Add Constable Notes --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 22da131..9bd6175 100644 --- a/README.md +++ b/README.md @@ -170,6 +170,7 @@ major proof assistants are * [Equality in Lazy Computation System](http://www.nuprl.org/documents/Howe/EqualityinLazy.html) (of general interest) * [Naive Computational Type Theory](http://www.nuprl.org/documents/Constable/naive.pdf) * [Innovations in CTT using NuPRL](http://www.nuprl.org/documents/Allen/05-jal-final.pdf) + * [Two Lectures on Constructive Type Theory](https://www.cs.uoregon.edu/research/summerschool/summer15/notes/OPLSS-Short-2015-2.pdf) - Homotopy Type Theory