Gwaith-i-Mírdain

We are creating 21st-century proof assistants, particularly for higher-dimensional type theories. Current projects:

Narya: An experimental proof assistant for higher-dimensional type theory, including Multi-Modal, Multi-Directional, Higher/Parametric/Displayed Observational Type Theory.
Olorin: An in-browser graphical proof assistant for learning proofs, using Narya as a backend proof-checker.

The only content on this site currently is the:

Development blog: Unformed thoughts mostly about proof assistant design and implementation, plus progress reports on our projects.