[Agda] Using Agda in proving computer system correct

[Liang-Ting Chen]

>
> Still, library support of general
> metaprogramming tools is lacking. I also wasn't satisfied by naked and
> raw De Bruijn indices that Agda uses for its internal representation
> (which is very error-prone and inefficient) and not having static
> information on how many times a term was quoted was quite unpleasant,
> but these are technical details that are pretty solvable. Additional
> features like defining data types using reflection also can be added.


A high-level typed tactic language can be implemented via Agda's reflection
framework, and I have an
early implementation of Mtac [1] in Agda as a proof of concept. See
https://github.com/L-TChen/MtacAR.

Just like Mtac, it gives you pattern matching against expressions, name
generation/restriction, abstraction, typed meta variable and reusing Agda's
interactive environment. No de Bruijn index manipulation is needed.

However, it is not ready for "production use" yet. For example, backward
reasoning, e.g., Mtac2, requires a cumulative hierarchy of universes to be
useful, because subgoals might not be in the same universe. And, the
efficiency is pretty bad compared to Agsy, i.e. `C-c C-a`. I am distracted
by something else for now, but hopefully it will be actively developed
again...

[1] B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, and V.
Vafeiadis, “Mtac: A monad for typed tactic programming in Coq,” J. Funct.
Program., vol. 25, Aug. 2015.  DOI:
https://doi.org/10.1017/S0956796815000118

-- 
Best regards,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190804/c91a8efe/attachment.html>