動的に変更可能な情報フローを用いたプログラム意味論

開催日時
2018/04/25 水 16:30 - 17:30
場所
3号館110講演室
講演者
室屋晃子
講演者所属
京大・数理研/University of Birmingham
概要

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.