LEGO
#Fleeting_Notes
LEGO
『Sets in types, types in sets』によるとCICかも
LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack in Edinburgh using New Jersey ML. It implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT).
ref: https://www.dcs.ed.ac.uk/home/lego/html/intro.html
確認用
Q. LEGO
調査用
Google.icon LEGO(日)
Google.icon Lego(英)
Wikipedia.icon
LEGO - Wikipedia(日)
LEGO(検索) - Wikipedia(日)
Wikipedia.icon
Lego - Wikipedia(英)
Lego(検索) - Wikipedia(英)