A Domain-Specific Language for the Specification of Path Algebras.
Vilius Naudziunas, Timothy G. Griffin · 2011
Path algebras are used to describe path problems in directed graphs. Constructing a new path algebra involves defining a carrier set, several operations, and proving that many algebraic properties hold. We describe work-in-progress on the development of a domain-specific language for specifying path algebras where implementations and proofs are automatically constructed in a bottom-up fashion. Our initial motivation came from the development of Internet routing protocols, but we believe that the approach could have much wider applications. We have implemented the language using the Coq theorem prover.