 |
Computer Laboratory
Timothy G. Griffin
|
 |
|
CAS = Combinators for Algebraic Structures (formerly Metarouting)
The CAS project is using Coq to implement a language of combinators that can be
used to construct complex algebraic structures for solving generalized path-finding
problems. Such structures include semirings and their generalisations. The key
idea of CAS is that the structures built with combinators carry proofs of their
algebraic properties. Coq's extraction to OCaml is then used to build an OCaml
library where the combinators produce structures with certificates of correctness.
The CAS project was initially inspired by problems arising in the design of
network routing protocols and this area of applications has motivated the
current choice of combinators in CAS. However, we expect that the system
will find other applications in areas such as optimisation and Operations
Research.
I expect that the prototype implementation will be made public sometime in 2022.
- Publications.
The project started with the
Metarouting
paper in SIGCOMM 2005.
Most of my
publications
since have aimed at extending the metarouting ideas in one way
or another.
My MPhil course (An Algebraic Approach to Internet Routing)
has been very important in this evolution.
- Past PhD students:
Alexander J. T. Gurney, John Billings, Philip J. Taylor,
M. Abdul Alim, Vilius Naudžiūnas,
Matthew L. Daggitt.
- Past funding has come from EPSRC, Cisco, and Boeing.
- Current funding is a gift from Huawei.
