Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 11:30 - 11:50 at Aurora Borealis - Dependently Typed Programming Chair(s): William J. Bowman

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.

Sun 18 Aug

tyde-2019-papers
10:50 - 12:10: TyDe 2019 - Dependently Typed Programming at Aurora Borealis
Chair(s): William J. BowmanUniversity of British Columbia
tyde-2019-papers10:50 - 11:10
Talk
Pre-print
tyde-2019-papers11:10 - 11:30
Talk
Sean InnesUniversity of Bristol, Nicolas WuImperial College London
Link to publication
tyde-2019-papers11:30 - 11:50
Talk
Liang-Ting ChenSwansea University, UK
Pre-print
tyde-2019-papers11:50 - 12:10
Talk
Link to publication