FLOLAC 2016
報名資訊
課程簡介
行事曆
函數編程
λ 演算與型別
基礎邏輯
Martin-Löf 型別理論
依值型別編程
邀請演講
特別講座
中文
English
依值型別編程 (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