A Signature Compiler for the Edinburgh Logical Framework

Michael Zeller, Aaron Stump, and Morgan Deters

In the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007), Bremen, Germany, 15 July 2007.

This paper describes the Signature Compiler, which can compile an LF signature to a custom proof checker in either C++ or Java, specialized for that signature. Empirical results are reported showing substantial improvements in proof-checking time over existing LF checkers on benchmarks.