Event
Model-Based Systems Engineering Colloquium: Timothy Griffin
Monday, November 7, 2011
11:00 a.m.
1146 A.V. Williams Building
Kimberly Edwards
301 405 6579
kedwards@umd.edu
Model-Based Systems Engineering Colloquium
Building Algebraic Structures with Combinators
Timothy Griffin
University of Cambridge
Host
John Baras
| video |
Abstract
I'll describe ongoing work with my student Vilius Naudziunas on a domain-specific language for implementing various algebraic structures (semirings, ordered semigroups, etc). Expressions in the language are made up of constants (representing simple algebras such as min-plus) and combinators that construct new structures from components (such as direct and lexicographic products).
The key feature of the language is that it has been designed so that a fixed class of important properties (such as distributivity, idempotence, commutativity, and so on) are automatically proved or refuted by the type system of the language. This allows a user to specify complex algebraic structures and obtain these proofs (or refutations) automatically. It is hoped that the language and its implementation will facilitate the rapid exploration of the algebraic design space.
We have implemented a prototype using the Coq theorem prover. All of the essential theorem proving --- for the "typing rules" --- is performed at "language design time." Users writing algebraic expressions at "specification time" do not run Coq directly. Rather, they run code that has been extracted automatically from the (constructive) proofs of our library of Coq theorems.
Biography
Timothy G. Griffin has a BS in Mathematics from the University of Wisconsin, Madison, and a PhD in Computer Science from Cornell University. Tim was on the faculty of UNICAMP in Brazil and then a researcher at Bell Laboratories. Since 2005 Tim has been on the faculty of the Computer Laboratory at the University of Cambridge. Tim's recent research has focused on algebraic modeling of Internet routing protocols.
