Institute of Information Science Academia Sinica
Topic: Monadic typed tactic programming by reflection
Speaker: Dr. 陳亮廷 (Swansea University, UK)
Date: 2019-09-17 (Tue) 10:00 – 12:00
Location: Auditorium 101 at IIS new Building
Host: Shin-Cheng Mu


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.