Article ID Journal Published Year Pages File Type
423741 Electronic Notes in Theoretical Computer Science 2008 7 Pages PDF
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