Signature Compilation for the Edinburgh Logical Framework

Michael Zeller; Aaron Stump; Morgan Deters

doi:10.1016/j.entcs.2007.09.022

Back

Signature Compilation for the Edinburgh Logical Framework

Journal article

Open access

Signature Compilation for the Edinburgh Logical Framework

Michael Zeller, Aaron Stump and Morgan Deters

Electronic notes in theoretical computer science, Vol.196(C), pp.129-135

01/22/2008

DOI: 10.1016/j.entcs.2007.09.022

Files and links (1)

url

https://doi.org/10.1016/j.entcs.2007.09.022View

Published (Version of record) Open Access

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.

Edinburgh LF

signature compilation

Details

Title: Subtitle: Signature Compilation for the Edinburgh Logical Framework
Creators: Michael Zeller - Washington University in St. Louis
Aaron Stump - Washington University in St. Louis
Morgan Deters - Washington University in St. Louis
Resource Type: Journal article
Publication Details: Electronic notes in theoretical computer science, Vol.196(C), pp.129-135
DOI: 10.1016/j.entcs.2007.09.022
ISSN: 1571-0661
eISSN: 1571-0661
Publisher: Elsevier B.V
Language: English
Date published: 01/22/2008
Academic Unit: Computer Science
Record Identifier: 9984259492502771

Metrics

5 Record Views