LEGO (proof assistant)

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.