A Framework for Specifying and Reasoning about Computations
Department of Computer Science and Engineering
University of Minnesota
COM2 Level 4
Executive Classroom, COM2-04-02
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 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, Y. Wang and myself.
Biodata:
Gopalan Nadathur is a professor in the Department of Computer Science and Engineering at the University of Minnesota. He has previously held faculty appointments at Duke University and the University of Chicago and visiting appointments at the University of Munich, Ecole Polytechnique (France), the Australian National University and the IT University of Copenhagen. His research interests span the areas of computational logic, programming languages, and logic programming. He co-invented the specification and programming language called Lambda Prolog that was the first to introduce the method now known as higher-order abstract syntax into the programming context. He then led a long-term project that resulted in an efficient implementation of Lambda Prolog called Teyjus. His recent work has concerned reasoning about the specifications of formal systems. Towards this end, he has co-developed a specialized logic that, amongst other things, embodies the ability to construct arguments based on induction and co-induction. This logic, which can embed Lambda Prolog and thereby reason about specifications written in it, has been implemented in the Abella proof assistant. In an ongoing project with Yuting Wang, he is leveraging Abella and Lambda Prolog in building verified compilers for functional programming languages. Gopalan Nadathur is the co-author of a book entitled Programming with Higher-Order Logic published by Cambridge University Press. He is an Editorial Advisor to the Cambridge Journal Theory and Practice of Logic Programming and the moderator for the areas of Programming Languages and Logic and Computer Science of the Computing Research Repository.