Type Theory and Formal Proof: An Introduction

Type Theory and Formal Proof: An Introduction

2014

Ratings1

Average rating3.5

15

Read the first half (up to encoding logical notions in λC). The first three chapters are pretty clear and easy to understand, but once it gets to type dependent on types and terms, they stopped giving syntax rules and things becomes more sloppy, requiring more work from the reader to understand the full implication of the typing system.
Would recommend this to all readers who know a bit of logic, but make sure to at least skim through the exercises and proofs portion of the text, as they become increasingly important.

June 10, 2024Report this review