Cycle séminaires

Graph Programs

Detlef Plump

Exposé du 13/3/2013, dans le cadre d'une réunion du projet Climt



 
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