Sciweavers

ENTCS
2008
81views more  ENTCS 2008»
13 years 11 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 a...
Michael Zeller, Aaron Stump, Morgan Deters