Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add TTFP, PFM and CTT Lecture Notes #3

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,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)
Expand All @@ -51,6 +51,14 @@ 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)

- Practical Foundations of Mathematics (PFM)

* [Online Copy](http://www.paultaylor.eu/~pt/prafm/html/)

### Proof Assistants

Expand Down Expand Up @@ -162,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

Expand Down