• از افقی فلسفی (12)
  • مقدمه (12)
  • مارتین-لاف اوّل (17)
    • احکام و اثبات (17)
    • دو شکل از احکام (21)
  • مارتین-لاف دوّم (24)
    • احکام تحلیلی و ترکیبی (24)
    • وارسی، درستی و معرفت پذیری (27)
• مروری کلّی بر یکسان سازی (33)
  • مقدّمه (33)
  • یکسان سازی مرتبه اول (38)
    • یکسان سازی نحوی (38)
    • الگوریتم رابینسن (39)
    • دستگاه U (43)
    • یکسان سازی معادله ای (47)
  • یکسان سازی مرتبه بالا (50)
    • مقدّماتی از حساب لمبدا (51)
    • الگوریتم هوئت (54)
    • یکسان سازی به کمک حساب (58)
    • زیر مجموعه های تصمیم پذیر (60)
• حساب (62)
  • زبان (63)
    • جانشینی (64)
    • احکام (66)
    • نوع سازی (67)
    • برابری معنایی (69)
  • ویژگی های مقدّماتی (71)
• یکسان سازی برای حساب (92)
  • نحو و قواعد نوع سازی (94)
    • نحو (94)
    • نوع سازی دوجهته (97)
    • قواعد نوع سازی (98)
  • یکسان سازی محدودیّت-بنیان (104)
  • جانشینی وارون پذیر (108)
  • هرس کردن (110)
  • الگوریتم یکسان سازی برای حساب (113)
    • یکسان سازی فرا-متغیّرهای یکسان (116)
  • درستی الگوریتم (119)
• حساب های ساخت ها (127)
  • حساب ساخت ها (129)
  • حساب ساخت ها بانضمام -نوع (136)
    • نحو و قواعد (137)
    • برخی ویژگی های نظری (139)
    • سازگاری منطقی و تصمیم پذیری (146)
  • نتیجه گیری و کارهای بعدی (153)
• جانشینی پی در پی کلّی (154)
• مراجع (157)
• واژه‌نامه انگلیسی به فارسی (162)