Book details
Type Theory & Functional Programming
Categories Category theory , Type theory , Functional programming
This book develops constructive type theory as both a logic and a functional programming system, beginning with the mathematical and programming foundations needed to study it. It covers natural deduction, lambda calculus, dependent types, the Curry–Howard correspondence, formal properties of the system, and examples including program extraction from proofs.