本書是關(guān)于現(xiàn)代類型論的專著。與集合論類似，現(xiàn)代類型論是數(shù)學(xué)及諸多領(lǐng)域的
基礎(chǔ)語言。本書介紹了現(xiàn)代類型論(及其元理論)，并以自然語言語義學(xué)和計算機輔助
推理為例對以現(xiàn)代類型論為基礎(chǔ)的應(yīng)用領(lǐng)域進行深入淺出的討論。作為基礎(chǔ)語言，現(xiàn)
代類型論一方面提供了豐富的描述機制，另一方面便于理解與實現(xiàn)，因此與集合論相
比有著多方面的優(yōu)勢。這些優(yōu)點在實際運用中展示出來：作為范例，書中深入研究了
基于現(xiàn)代類型論的自然語言語義學(xué)，以加深讀者對此的理解。書中還介紹了以現(xiàn)代類
型論為基礎(chǔ)的交互式證明技術(shù)在數(shù)學(xué)形式化、計算機程序驗證及自然語言推理諸方面
的應(yīng)用，進一步展示了使用現(xiàn)代類型論作為基礎(chǔ)語言的優(yōu)勢。

本書適合研究自然語言語義學(xué)、計算機科學(xué)和邏輯學(xué)等領(lǐng)域的學(xué)者及研究生和
對相關(guān)內(nèi)容感興趣的讀者。