Logical frameworks are languages for specifying logics and reasoning with them formally, with machine support. Examples are logics to prove the safety of programs or authenticate access rights to protected data. The project investigates theoretical foundations and efficient implementation techniques for logical frameworks. Specifically, the project addresses performance bottlenecks in current, large-scale applications of the Twelf logical framework aimed at improving safety and security of mobile code within the national cyber infrastructure. The techniques include methods for proof compression based on intrinsic redundancy, and methods to increase the degree of automation in proof search and verification.
Logic is a key discipline in computer science because it allows us to make definitive judgments such as "yes, this program is safe to run" or "yes, this agent is allowed to access these data". The critical notion is that of a formal proof, which can convince a code recipient of its safety or an operating system of access rights. Logical frameworks represent such proofs as data structures. This project investigates methods to manipulate these data structures efficiently so they can be used in realistic, large-scale applications. The system under construction is also used to teach undergraduates the concepts of formal logic as they are applied in computer science and mathematics.
