型別論與邏輯 / Type Theory and Logic

• 講者: 柯向上 Hsiang-Shang Ko

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

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
3. Natural number arithmetic (slides, scribbles, NatArith.agda, NatArithC.agda, Russell.agda, RussellC.agda, )
   • Set of natural numbers
   • Identity types
   • Peano axioms and algebraic properties
4. 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

• Nicolaas Govert de Bruijn. Type-theoretical checking and philosophy of mathematics. In Twenty-Five Years of Constructive Type Theory, pages 41–56. Clarendon Press, 1998.
• Michael Dummett. Elements of Intuitionism. Oxford University Press, second edition, 2000.
• Georges Gonthier. Formal proof — the four-color theorem. Notices of the AMS, 55(11):1382–1393, 2008.
• Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2012.
• Arend Heyting. Intuitionism: An Introduction. Amsterdam: North-Holland Publishing, third revised edition, 1971.
• Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
• Per Martin-Löf. Constructive mathematics and computer programming. Philosophical Transactions of the Royal Society of London, 312(1522):501–518, 1984.
• Per Martin-Löf. Truth of a proposition, evidence of a judgement, validity of a proof. Synthese, 73(3):407–420, 1987.
• Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Clarendon Press, 1994.
• Bengt Nordström, Kent Peterson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.