Type Theory (类型论) Foundations

Robert Harper 2013

Lecture 1:

Holy Trinity: A Scientific Discovery is TRUE if fulfills:

  1. Proof Theory Logic
  2. Algebraic Category Theory
  3. Program Type Theory

A Program is an ABSTRACT Mathematical Object (“M”) :

“A is true” written as “M A”,

ie M is of Type A.

Note: Program M is not about “Coding”.

Above diagram:

[Left] : Proof Theory Logic

[Right] : Category Theory

Lecture 2:

Lecture 2.1

(Video 15:30 mins)

Type Theory is the theory of construction of programming language:

Higher Order Function <=> Exponential Type

Struct, Tuple <=> Cartesian Product Type

Choices of classes of data <=> ‘Some’ Type

Logic is an application of Type Theory

Logic is a part of Math which is a part of Computer Science in which Type Theory is the ‘Theory of Construction’ of Programming Languages.

Lecture 2.2:

Lecture 3:


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s