在數理邏輯和計算機科學中，構造微積分（CoC）是ThierryCoquand創建的一種類型理論。它既可以作為一種類型化的編程語言，也可以作為數學的構造基礎。基于這第二個原因，CoC及其變體一直是Coq和其他證明輔助工具的基礎。它的一些變體包括歸納構造的微積分（增加了歸納類型），（共同）歸納構造的微積分（增加了共同歸納），以及歸納構造的預測性微積分（刪除了一些不可預測性）。

CoC是一個高階類型的λ微積分，最初由ThierryCoquand開發。它因處于Barendregt的lambdacube的頂端而聞名。在CoC中可以定義從術語到術語的函數，以及術語到類型，類型到類型，以及類型到術語的函數。CoC是強規范化的，因此也是一致的。根據哥德爾不完全性定理，不可能從CoC內部證明一致性。

CoC是與Coq證明助手一起開發的。隨著該理論功能的增加（或可能的責任的刪除），它們在Coq中也可用。CoC的變種被用于其他證明助手，如Matita。

構造微積分可以被認為是庫里-霍華德同構的延伸。庫里-霍華德同構將簡單類型的λ微積分中的一個術語與直覺命題邏輯中的每個自然演繹證明聯系起來。構造微積分將這種同構擴展到完整的直覺主義謂詞微積分中的證明，其中包括量化語句的證明（我們也將稱之為命題）。

在構造微積分中，一個術語是用以下規則構造的。{displaystyle(λx:A.B)},{displaystyle(λx:A.B)}是變量。證明，是類型為命題的術語；命題，也被稱為小類型；謂詞，是返回命題的函數；大類型，是謂詞的類型(P{displaystylemathbf{P}}}就是一個大類型的例子）。{displaystylemathbf{T}}是大類型的例子；T}本身，這是大類型的類型。

構造的微積分允許證明類型判斷。構造微積分的有效判斷可以從一組推理規則中推導出來。在下文中，我們使用{displaystyle/Gamma}是指一個類型賦值序列。