Higher inductive types are inductive types that include nontrivial higher-dimensional structure, represented as identifications that are not reflexivity. While work proceeds on type theories with a computational interpretation of univalence and higher inductive types, it is convenient to encode these structures in more traditional type theories with mature implementations. However, these encodings involve a great deal of error-prone additional syntax. We present a library that uses Agda’s metaprogramming facilities to automate this process, allowing higher inductive types to be specified with minimal additional syntax.
Kokke and Swierstra @cite_16 implemented a library for proof search using Agda's old reflection primitives, from before it had elaborator reflection. They describe a Prolog interpreter in the style of @cite_5 . It employs a hint database and a customizable depth-first traversal, with lemmas to assist in the proof search.
@cite_5 @cite_16
2025665265 759633442
This paper documents our experience using declarative languages to give secondary school students a first taste of Computer Science. The course aims to teach students a bit about programming in Prolog, but also exposes them to important Computer Science concepts, such as unification or searching strategies. Using Haskell's Snap Framework in combination with our own NanoProlog library, we have developed a web application to teach this course. As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.