Type-Theoretical Semantics with Coercive Subtyping
Zhaohui Luo
Department of Computer Science
Royal Holloway, University of London
Type theory
Combines computation and logical inference
Uniformly in a single language
Simple operational semantics + embedded logic
Provides structural mechanisms
Natural description power
Remark: "types" are natural in math. (cf, "sets" in set theory)
Has nice properties
Eg, Normalisation (decidability + consistency), Subject Reduction, Church-Rosser, … …
Is the basis of implementations of
Proof assistants (ALF/Agda, Coq, Lego/Plastic, Matita, NuPRL, … )
I. Type Theory: an Introduction
Basic judgement of type theory
a : A
"a is an object of type A."
Examples
3 : Nat
2, 2+1 : Nat Nat
x:Nat.x : Nat Nat
How do we understand "a : A"
Basics – canonical objects
Examples:
A = Nat, a = 3+4, v = 7.
A = Nat Nat, a = ( x:Nat. x,x+1 )(2), v = 2,3 .
Type of natural numbers
Elimination rule explained
"If C holds for all canonical nats, then C holds for every nat."
General pattern (for all inductive types):
C holds for all canonical objects of …
========================================================================
C holds for every object of …
Inductive/dependent types: examples
Finite types (Unit, Bool, ...)
Types of lists, vectors, trees, …
Types of dependent functions
Types of dependent pairs (tuples)
Types of ordinals, well-orderings, ...

下一页