of Paul van der Stel
A proof assistant is a software tool which helps with the creation of formal proofs, by rigorously verifying the proof that a human writes in the proof language. Typically, this works by formulating a goal, for which a formal proof must then be written, in the formal language of the proof assistant. Some proof assistants use tactics, which change the goals that must be proven. Some tactics add sub-goals, while others might prove or transform them. The goal is considered proved when all sub-goals (as created by the tactics) are proven.
The language Agda is both a general-purpose programming language and a proof assistant, through the propositions-as-types paradigm. Agda is dependently typed, and a type in Agda may also represent a proposition in logic. The existence of a value that inhibits that type (“term”) is considered a proof that the corresponding logic proposition is true.
Agda has no built-in concept of proof tactics. It is possible to type check programs that are not yet complete. Incomplete parts of the program can be indicated using a hole. Such a hole represents a part of the program that is still missing, and is yet to be filled in by the author of the program. The goal of this project is to investigate the design of a tactic library for Agda, which allows the programmer to re-use or define tactics, which may help with filling in the holes with appropriate terms. The focus lies on building this library in Agda itself, making use of the reflection API and the general-purpose nature of Agda, instead of building it in a separate language. Such usage allows for both compile-time and edit-time usage of the tactics, resulting in more interactive proof development.
Delahaye, D. (2000, November). A tactic language for the system Coq. In International Conference on Logic for Programming Artificial Intelligence and Reasoning (pp. 85-95). Springer, Berlin, Heidelberg. Korkut, J. (2018). Edit-Time Tactics in Idris (Doctoral dissertation, Wesleyan University). Pédrot, P. M. (2019). Ltac2: tactical warfare. In The Fifth International Workshop on Coq for Programming Languages, CoqPL (pp. 13-19).
Student: Paul van der Stel
Supervisor(s): Jesper Cockx