[Colloquium] Brigitte Pientka talk--4/9/03

[Meridel Trimble]

--------------------------------------------------------------------------------
-------- 

TOYOTA TECHNOLOGICAL INSTITUTE 
--------------------------------------------------------------------------------
-------- 

Date: Wednesday, April 9th, 2003

Time: 2:30 p.m. 

Place: Ryerson Hall 251 

Speaker: Brigitte Pientka
Carnegie Mellon University

http://www-2.cs.cmu.edu/~bp/

Title: Logic Form and Its Application to Question Answering

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. 
*Refreshments will be served after the talk in Ryerson 255* 

If you wish to meet with the speaker, please send e-mail to Meridel Trimble 
mtrimble at uchicago.edu