證明或反駁Barendregt-Geuvers-Klop猜想。(計算機科學中更多未解決的問題)在被稱為證明理論和類型理論的數理邏輯分支中，純類型系統（PTS），以前被稱為廣義類型系統（GTS），是一種類型化的lambda計算形式，它允許任意數量的排序和其中任何一個排序之間的依賴關系。這個框架可以被看作是Barendregt的lambdacube的泛化，在這個意義上，cube的所有角落都可以被表示為只有兩種類型的PTS的實例。事實上，Barendregt(1991)在這個背景下構建了他的立方體。純類型系統可能掩蓋了類型和術語之間的區別，并折疊了類型層次，正如構造微積分的情況一樣，但通常不是這樣的，例如簡單類型的lambda微積分只允許術語依賴于術語。純類型系統是由StefanoBerardi（1988）和JanTerlouw（1989）獨立提出的。Barendregt在他后來的論文中詳細地討論了它們。在他的博士論文中，Berardi定義了一個類似于lambdacube的構造邏輯的立方體（這些規范是不依賴的）。這個立方體的一個修改后來被Geuvers稱為L立方體，他在他的博士論文中把Curry-Howard對應關系擴展到這個環境中。基于這些想法，Barthe和其他人通過增加一個雙重否定算子定義了經典純類型系統（CPTS）。同樣，在1998年，TijnBorghuis引入了模態純類型系統（MPTS）。Roorda討論了純類型系統在函數式編程中的應用；而Roorda和Jeuring提出了一種基于純類型系統的編程語言。來自lambdacube的系統都是已知的強規范化的。

一般來說，純類型系統不需要是這樣的，例如吉拉德悖論中的系統U就不是。(粗略地說，Girard發現了純類型系統，在這個系統中，人們可以表達類型構成類型的句子)。此外，所有已知的不是強規范化的純類型系統的例子甚至不是（弱）規范化的：它們包含不具有規范形式的表達式，就像無類型的λ微積分。這是否總是如此，即一個（弱）規范化的PTS是否總是具有強規范化屬性，這是這個領域的一個主要的開放問題。這被稱為Barendregt-Geuvers-Klop猜想（以HenkBarendregt,HermanGeuvers和JanWillemKlop命名）。

一個純類型系統是由一個三聯體定義的{displaystyle{frac{GammavdashA:BquadB=_{beta}B'quadGammavdashB':s}{GammavdashA:B'}quad{text{（轉換）}}。

以下編程語言有純類型系統。SAGEYarrowHenk2000