Signature Compilation for the Edinburgh Logical Framework

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. Key words: Edinburgh LF, signature compilation

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Michael Zeller, Aaron Stump, Morgan Deters
• Keywords: ENTCS 2008, LF Signature, Signature, Signature Compiler