依值型別編程 (Dependently Typed Programming)

• 講者: 穆信成 Shin-Cheng Mu

Outline

• A quick introduction to Agda
• Inductive Family
• Practicals

Course Materials

• handouts
• Prelude.agda
• 1-Intro.agda
• 2-IndFamilies.agda
• 3-Logic.agda
• 4-Membership.agda
• 5-ProofsAboutEquality.agda
• 6-BinomialHeap.agda
• 7-VerifiedCompiler.agda