本書共分4章: 第1章介紹不帶類型的λ-演算、簡單類型的λ-演算和F系統(tǒng), 主要討論語法和β-歸約語義; 第2章介紹Coq,重點(diǎn)是從函數(shù)式程序設(shè)計(jì)的角度展開討論, 內(nèi)容涉及自然數(shù)函數(shù)、列表、多態(tài)數(shù)據(jù)結(jié)構(gòu)、依賴類型、高階函數(shù)、柯里-霍華德關(guān)聯(lián)以及余歸納類型; 第3章介紹OCaml這門通用程序設(shè)計(jì)語言, 除了基本的程序設(shè)計(jì)概念, 還討論函子和單子這樣比較高級的語言特征; 第4章提供了部分習(xí)題的參考答案, 以方便感興趣的讀者自行學(xué)習(xí)。