型別論與邏輯 / Type Theory and Logic

Introduction to Martin-Löf’s intuitionistic type theory.

Outline

  1. Simple type theory (slides)
    • Propositions as types
    • Sets, (typing) judgements, and derivations
    • Propositional set formers
    • Intuitionism and computability
  2. Dependent type theory (slides, derivation of the Axiom of Choice)
    • Dependent products and sums
    • Universe hierarchy
    • Computation and equality judgements
    • Classical vs intuitionistic logic
    • Set of natural numbers
    • Identity types
    • Peano axioms and algebraic properties
  3. Meta-theoretical reasoning (slides, scribbles, Implicational.agda, ImplicationalC.agda)
    • Meta-language vs object language
    • The Curry–Howard isomorphism
    • Two-valued semantics of propositional logic
    • Soundness and completeness

References

zh-tw/logictype.txt · 上一次變更: 2014/07/05 18:56 由 joshs
CC Attribution-Share Alike 3.0 Unported
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0