Andromeda Andromeda is an experimental implementation of dependent type theory with a reflection rule. See the official Andromeda web site for more information.