Martin-Löf. Intuitionistic Type Theory

raw.githubusercontent.comsite

Notes by Giovanni Sambin of a series of type theory lectures given in Padua, June 1980.

similar

Intuitionistic Type Theory archive-pml.github.io
site category #math link ↗

Per Martin-Lof.
Bengt. Programming in Martin-Löf's Type Theory cse.chalmers.se
site category #theoretical-computer-science link ↗

This book describes different type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective.
The Univalent Foundations Program Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of… homotopytypetheory.org
site category #theoretical-computer-science link ↗

The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
Type Theory and Functional Programming cs.kent.ac.uk
site category #math link ↗

Simon Thompson.
Knuth. Things a Computer Scientist Rarely Talks About web.stanford.edu
site category #theoretical-computer-science link ↗

A general illustration of relations between faith and science.
Introduction to Logic logic.stanford.edu
site category #math link ↗

Michael Genesereth, Eric J. Kao (Stanford University).

Theoretical Computer Science › Type Theory > Lecture Notes: “Notes by Giovanni Sambin of a series of type theory lectures given in Padua, June 1980.”