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

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
20m
Talk
Syntax with Shifted Names
TyDe
Stephen Dolan , Leo White Jane Street
Pre-print
11:10
20m
Talk
Tic Tac Types (Functional Pearl)
TyDe
Sean Innes University of Bristol, Nicolas Wu Imperial College London
Link to publication
11:30
20m
Talk
Monadic typed tactic programming by reflection
TyDe
Liang-Ting Chen Swansea University
Pre-print
11:50
20m
Talk
Deferring the Details and Deriving Programs
TyDe
Link to publication