|||
Browse
Source
Search
Public
Clear
MiniLaTeX Demo
Guest:Home
Pinned Docs
Home pages
Sign out guest
TOC on
Expand
Notes on Type Theory
1
Introduction
2
Propositions as Types
3
Natural Numbers
4
Binary represention
5
Lambda Calculus
6
Type Inference
7
Recursors
8
Homotopy Type Theory
9
Mathematical Notes
10
References

Notes on Type Theory
James Carlson

I am writing these notes to myself as I study Philip Wadler's PLFA notes. They are my attempt to clairify things to myself, nothing more. As such, there may be errors, even grievous errors, as am a beginner at this subject. So if you find something that is wrong, please do let me know (jxxcarlson at gmail)

(( Work in Progress ))

Section 1: Introductipn

A brief introduction to type theory in the context of the natural numbers in which the definitions are motivated by the Peano axioms. Sets versus types, function types and rules of inference, defnitional versus propositional eequality.

Section 2: Propositions as Types

The Curry-Howard isomorphism and intuitionistic logic as formulated in type theory. Worked-out example of how to prove the associative law for the natural numbers using the Peano axioms. Discussion of dependent types and the predicate calculus, the Law of the Excluded Middle, higher order logics. Brief discussion of inference rules such as congruence.

Section 3: Agda

The beginning of some notes on Agda. Rewrite.

Section 4: Lambda Calculus

Bare-bones description of the syntax and semantics of the lambda calculus; normal forms and divergence of . Remarks on the simply-typed lambda calculus.

Section 4: Type Inference

A sketch of the basic idea; unification.

Section 4: Mathematical Notes

For now, just some remarks on the connection between the theory of groupoids and type theory.

Manuals
Feedback
Keys OFF
Toggle Chat