A Framework for Specifying and Reasoning about Computations
Professor Gopalan Nadathur (University of Minnesota)
LOGIC AND COMPUTATION SEMINARDATE: 2011-11-29
TIME: 15:30:00 - 16:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
The computational structure of formal systems is often described through syntax directed rules in the style of structural operational semantics. Such presentations are typically intended to help in prototyping and in proving properties of these systems. This talk will survey techniques that we have developed to provide rigorous, computer-based support for such activities. Specifically, I will discuss the higher-order abstract syntax approach to treating binding structure concisely and declaratively, the use of enriched recursive relational specifications to encode rule based descriptions, a logic of definitions that includes (co-)induction principles for reasoning about such relational specifications and a new generic quantifier called nabla that allows for the treatment of names in specifications and free variables that arise during computation. I will also outline a two level logic approach to reasoning about specifications. These ideas have led to several actual computer systems such as Teyjus, Bedwyr, Abella and Tac that will be touched upon during the talk.
Note: The talk will describe ideas that have been contributed to by D. Baelde, A. Gacek, R. McDowell, D. Miller, A. Tiu and myself.
BIO:
http://www-users.cs.umn.edu/~gopalan/
