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