LEGO is an interactive theorem prover and proof assistant that was developed by Gordon Plotkin and others in the late 1980s and early 1990s. It is based on a typed lambda calculus and supports higher-order logic, which allows users to construct formal proofs and check the correctness of those proofs mechanically. Key features of LEGO include: 1. **Type System**: LEGO uses a rich type system, which allows for the expression of a wide variety of mathematical and logical concepts.
Articles by others on the same topic
There are currently no matching articles.