A nano "theorem prover".
Browse cluster: Functional Programming & Type Theory →ESCoC is a minimal theorem prover implemented in JavaScript (approximately 500 lines including parser and type-checker) that extends the Calculus of Constructions to support inductive reasoning through recursive definitions and scope expansion. Built on the principle that mathematical elegance guides discovery, it modifies CoC by allowing variables to be bound within input types of dependent functions and enabling recursive type definitions, enabling inductive datatypes to be expressed through self-referential encodings without adding new primitives. The system demonstrates how Boolean and natural number types, along with equality proofs, can be implemented through these minimal extensions to an existing formal foundation.