Timothy G. Griffin
|Computer Laboratory > Timothy G. Griffin > CAS|
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 postdoc will be involved in all aspects of design and implementation extending an existing prototype.
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.