Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.entcs.2007.09.022 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
signature compilation,edinburgh logical framework,edinburgh lf,proof-checking time,empirical result,lf signature,substantial improvement,signature compiler,lf checker,custom proof checker,logical framework | Programming language,Computer science,Automated proof checking,Compiler,Theoretical computer science,Java,Logical framework | Journal |
Volume | ISSN | Citations |
196, | Electronic Notes in Theoretical Computer Science | 3 |
PageRank | References | Authors |
0.48 | 4 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Zeller | 1 | 3 | 0.48 |
| Aaron Stump | 2 | 3 | 0.48 |
| Morgan Deters | 3 | 283 | 17.25 |