Type Systems

Explanation:

• Axioms are typing judgements that are manifestly true.

• Inference rules produce true consequences given true premises

• Common notation for rules

  ?1 |- M1: ?1, …, ?N |- MN:?N
  
  ? |- M: ?

Natural deduction rules for (simply typed ?-calculus) [? is arbitrary]

• ?, x:? |- x: ?
• ? |- c: ?(c)
• ? |- M:? ? ?, ? |- N:? (? elimination)
  ? |- (M N): ?.
• ?, x:? |- M: ?. (? introduction)
  ? |- (?x:? M): ? ? ?

Previous slide

Next slide

Back to first slide

View graphic version