LEGO (proof assistant)
LEGO is a proof assistant developed by Randy Pollack at the University of Edinburgh. It implements several type theories: the Edinburgh Logical Framework (LF), the Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT).
External links
This article is issued from Wikipedia - version of the Friday, March 22, 2013. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.