Abstract
This paper describes optimizations for checking proofs represented in the Edinburgh Logical Framework (LF). The optimizations allow large proofs to be checked efficiently which cannot feasibly be checked using the standard algorithm for LF. The crucial optimization is a form of result caching. To formalize this optimization, a path calculus for LF is developed and shown equivalent to a standard calculus. © Springer-Verlag Berlin Heidelberg 2002.
Cite
CITATION STYLE
Stump, A., & Dill, D. L. (2002). Faster proof checking in the edinburgh logical framework. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2392, 392–407. https://doi.org/10.1007/3-540-45620-1_32
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
