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.