We introduce a new semantic framework---dynamic Geometry of Interaction (dynamic GoI)---for functional programming, as a combination of two styles of program semantics: information-flow and graph-rewriting. A program is interpreted as a network (graph), and program evaluation is modelled using information flow on networks that can be dynamically reconfigured at run-time via graph rewriting. Our starting point is a particular instance of the information-flow semantics, which is Girard's Geometry of Interaction (GoI), a semantic framework to interpret proofs in Linear Logic. It is then interleaved with graph rewriting, on the key principle that the dynamic rewriting is guided and controlled by information flow. This talk gives an overview of development of the dynamic GoI framework, with discussion on its ability to model both intensional and extensional aspects of program evaluation.
2018/04/25 水 16:30 - 17:30
京大・数理研/University of Birmingham