Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory
Timothy G. Griffin
Computer Laboratory >  Timothy G. Griffin CAS

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.