Sciweavers

ENTCS
2008

Signature Compilation for the Edinburgh Logical Framework

13 years 3 months ago
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
Michael Zeller, Aaron Stump, Morgan Deters
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Michael Zeller, Aaron Stump, Morgan Deters
Comments (0)