Lambda TamerThe Lambda Tamer project tackles the issues surrounding computer formalization of programming languages and their tools, based around the Coq proof assistant. The Lambda Tamer methodology centers on higher-order and dependently-typed abstract syntax and aggressive automation. The main project output is a library of Coq definitions, theorems, and tactics in support of building certified compilers f
