Overcoming Performance Barriers:
Efficient Proof Search in Logical Frameworks
Dr. Brigitte Pientka
School of Computer Science
Date:
Time:
Location: 367 Votey
Abstract
The logical framework Twelf provides an experimental platform to specify, implement and execute formal systems. One of its applications is in proof-carrying code and proof-carrying authentication, where it is successfully used to specify and verify formal guarantees about the run-time behavior of programs. These real-world applications have exposed some critical bottlenecks: execution of many logical specifications is severely hampered and some are not executable at all, thereby limiting its application in practice. In this talk, I will describe three optimizations which substantially improve the performance and extend the power of the existing system. First, I give an optimized unification algorithm for logical frameworks which allows us to eliminate unnecessary occurs-checks. Second, I present a novel execution model based on selective memoization and, third, I will discuss term indexing techniques to sustain performance in large-scale examples. As experimental results will demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in real-world applications.
(Presented by the Computer Science Student Association ( http://www.cs.uvm.edu/~cssa/), University of Vermont.)