ICFP 2019 (series) / TyDe 2019 (series) / TyDe 2019 /
Monadic typed tactic programming by reflection
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 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 18 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:50 - 12:10 | Dependently Typed ProgrammingTyDe at Aurora Borealis Chair(s): William J. Bowman University of British Columbia | ||
10:50 20mTalk | Syntax with Shifted Names TyDe Pre-print | ||
11:10 20mTalk | Tic Tac Types (Functional Pearl) TyDe Link to publication | ||
11:30 20mTalk | Monadic typed tactic programming by reflection TyDe Liang-Ting Chen Swansea University Pre-print | ||
11:50 20mTalk | Deferring the Details and Deriving Programs TyDe Liam O'Connor UNSW Link to publication |