Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423741 | Electronic Notes in Theoretical Computer Science | 2008 | 7 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics