From 70c5dd462188a4f55c58c0392467aa2eef15ef8b Mon Sep 17 00:00:00 2001
From: = <=>
Date: Fri, 2 Oct 2020 02:43:46 +0700
Subject: [PATCH] =?UTF-8?q?Add=20Programming=20in=20Martin-Lof=E2=80=99s?=
 =?UTF-8?q?=20Type=20Theory=20book?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 README.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/README.md b/README.md
index 45c7d63..0424f22 100644
--- a/README.md
+++ b/README.md
@@ -188,6 +188,7 @@ A curated list of awesome mathematics resources.
 * [Proofs and Types](http://www.paultaylor.eu/stable/prot.pdf) - Jean-Yves Girard
 * [Intuitionistic Type Theory](https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf) - Per Martin-Lof
 * [Type Theory and Functional Programming](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/) - Simon Thompson
+* [Programming in Martin-Lof’s Type Theory](http://www.cse.chalmers.se/research/group/logic/book/book.pdf) - Bengt Nordstrom, Kent Petersson, Jan M. Smith
 
 ### Homotopy Type Theory