Print Email Facebook Twitter Tactics in Agda using reflection Title Tactics in Agda using reflection Author van der Stel, Paul (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Cockx, J.G.H. (mentor) Zaidman, A.E. (graduation committee) Swierstra, Wouter (graduation committee) Liesnikov, B. (mentor) Degree granting institution Delft University of Technology Programme Computer Science | Software Technology Date 2022-09-21 Abstract In this thesis, we develop a new library for Agda named Attic, which allows us to create and compose proof tactics that can be used to generate terms through reflection. Such tactics can be converted to Agda macros, allowing them to be used in term positions where they can generate term solutions of the expected type. Tactics can make the development of proofs faster by making proofs easier to read and write.This project can be seen as a sister project to Ataca, which is an earlier attempt at developing tactics that operate through reflection. Attic explores new mechanisms of operation, such as non-determinism with iterators to allow for multiple solutions, and the use of deferred unification, so that the final proof term is only fully constructed at the end of tactic evaluation.To allow for the representation of both finite and infinite sequences that can be consumed step-by-step, we have implemented the iterator data type in Agda. Although iterators existed in other systems previously, an Agda implementation had not been made. These iterators underpin the branching mechanism in tactic instructions, and support operations that can be used to generate, transform and filter values.Finally, we have implemented a number of tactics and operations that are commonly found in other proof assistants. We also compare the resulting library to the Ataca library and examine the differences in runtime for a small test case. While Attic is not yet a complete solution, we present new ideas that may be incorporated in future tactic systems. Subject agdaproof assistanttacticslibrary To reference this document use: http://resolver.tudelft.nl/uuid:76ad7694-6261-4e40-94a0-e99d14452a59 Part of collection Student theses Document type master thesis Rights © 2022 Paul van der Stel Files PDF pvds_thesis.pdf 2.1 MB Close viewer /islandora/object/uuid:76ad7694-6261-4e40-94a0-e99d14452a59/datastream/OBJ/view