Andromeda

Andromeda is a prover for dependent type theories à la Martin-Löf.

See the official Andromeda web site for more information, such as installation instructions and links to the ICFP 2019 materials.