Institute of Information Science Academia Sinica
講 題: Monadic typed tactic programming by reflection
講 者: 陳亮廷 博士 (Swansea University, UK)
時 間: 2019-09-17 (Tue) 10:00 – 12:00
地 點: 資訊所新館101演講廳
邀請人: 穆信成

We present a work in progress —a shallow embedding of a typed tactic language Mtac using elaborator reflection in a dependently typed language to allow users to write high-level tactics within the same language. In contrast to the original implementation of Mtac in Coq, this implementation is completely written in Agda using its reflection mechanism. To focus on the difference from its Coq counterpart, we give an example of tactics and briefly sketch the implementation of the core design and the pattern matching construct.