Geb

Geb is a categorical programming language whose first-class notions include "programming language" itself. Its constructions are precise, universal mathematics; its categories represent datatypes, programs, and the languages that express them.

Active development is the Lean 4 formalisation under geb-lean/, preceded by the Idris-2 implementation under geb-idris/. The Common Lisp reference implementation and the Agda verification are original efforts, retained for reference. This file indexes the project's documentation.

• Lean formalisation (active)
• Idris-2 implementation
• Agda verification (original effort)
• Common Lisp reference (original, mostly obsolete)

Lean formalisation (active)

• geb-lean/README.md — subproject overview and dependencies.
• geb-lean/docs/index.md — index of the implemented mathematical content.

Idris-2 implementation

• geb-idris/README.md — Geb as a circuit frontend.
• geb-idris/docs/index.md — documentation index.
• geb-idris/EXAMPLES.md — Geb by example.

Agda verification (original effort)

• geb-agda/README.md — formal verification of Geb's core-category properties.

Common Lisp reference (original, mostly obsolete)

• docs/common-lisp/manual.md — the Geb manual generated from the Common Lisp implementation, retained for reference and superseded by the development above.