Cycle séminaires |
Résumé |
GP is an experimental rule-based language for high-level problem solving in the domain of graphs, freeing programmers from handling low-level data structures. The language has a simple syntax and semantics, to facilitate formal reasoning about programs. In this talk, I will introduce GP by a number of example programs and discuss its structural operational semantics. In particular, I will show how to define branching and loop constructs via failing computations and how to check graph properties by reduction rules without destroying the input graph. At the end, I will briefly present a Hoare-style calculus for verifying graph programs.
Last modified: Wed Jul 10 23:49:36 CEST 2013 |