Tactics in Agda using reflection

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...

Extracting LLVM Intermediate Representation from Agda

Agda, a promising dependently typed function language, needs more mainstream adoption. By the process of code extraction, we compile proven Agda code into a popular existing language, allowing smooth integration with existing workflows. Due to Agda’s pluggable nature, this process is relatively straightforward. We implement a solution in Haskell...

Practical Verification of Lenses: Implementing Formally Verified Lenses using agda2hs

agda2hs is a tool which translates a subset of Agda to readable Haskell. Using agda2hs, programmers can implement libraries in this subset of Agda, formally verify them, and then convert them to Haskell. In this paper we present a new, verified implementation of the lens data type, which is used to access data structures in a readable yet...

Practical Verification of Concurrent Haskell Programs

The formal verification of concurrent programs is of particular importance, because concurrent programs are notoriously difficult to test. Because Haskell is a purely functional language, it is relatively easy to reason about the correctness of such programs and write down manual proofs. However, since these methods are still prone to error,...

Code Extraction from a Dependently Typed Language to a Stack Based Language

Dependently typed languages such as Agda can provide users certain guarantees about the correct- ness of the code that they write, however, this comes at the cost of excess code that is not used at run time. Agda code is currently compiled to another language before it is run, there are not many target languages in popular use, so it is unclear...

Comparing Code extraction from Agda to Java to existing Methods

Dependent programming languages such as Agda show a lot of promise in creating new ways of writing code, but currently suffer from a lack of support and features. In this paper we attempt to create a new back-end for Agda targeting Java which has a huge and thriving ecosystem.<br/><br/>We implement the new back-end for Agda in Haskell and we...

Practical Verification of the Reader Monad

Agda2hs is a tool that allows developers to write verified programs using Agda and then translate these programs to Haskell while maintaining the verified properties. Previous research has shown that Agda2hs can be used to produce a verified implementation of a wide range of programs. However, monads that model effectful computations were...

Code extraction from Agda to HVM

Dependently typed languages such as Agda have the potential to revolutionize the way we write software because they allow the programmer to catch more bugs at compile time than classical languages. Nonetheless, dependently typed languages are hardly used in practice. One of the reasons is the lack of mature compilers for them.<br/>This paper...

Practical Verification of a Free Monad Instance

Formal verification of software is a largely underrepresented discipline in practice. While it is not the most accessible topic, efforts are made to bridge the gap between theory and practice. One tool conceived for this exact purpose is agda2hs, a tool intended to allow developers to create their programs correct-by-design. A program written a...

Agda2Rust: A Study on an Alternative Backend for the Agda Compiler

Agda is a functional programming language with built-in support for dependent types. A dependent type depends on a value. This allows the developer to specify strict constraints for the types used in an application. Writing code with dependent types results in fewer type-related errors slipping through the compilation process. <br/>When...

Practical Verification of Infinite Structures in agda2hs

Agda allows for writing code that can be mathematically proven and verified to be correct, this type of languages is generally known as a proof assistant. The agda2hs library makes an effort to translate Agda to readable Haskell, in a way the Haskell is still consistent. In previous work it is shown that with the current agda2hs implementation,...

Verifying correctness of Haskell programs using the programming language Agda and framework agda2hs

Equational reasoning based verification address some of the limitations of classical testing. The Curry-Howard correspondence shows a direct link between type systems and mathematical logic based proofs. Agda is a language with totality and dependent types which makes use of the CH isomorphism to support equational reasoning in its programs. ...

Practical Verification of the Inductive Graph Library

Formal verification works better than testing, since the correctness of a program is proven. It is researched if it is possible and feasible to formally verify the Inductive Graph Library. The library is an abstract class in Haskell and is ported manually to Agda. Agda is a total and dependently typed language and thus can be used as a proof...

Producing a verified implementation of sequences using agda2hs

Purely functional languages are advantageous in that it is easy to reason about the correctness of functions. Dependently typed programming languages such as Agda enable us to prove properties in the language itself. However, dependently typed programming languages have a steep learning curve and are usable only by expert programmers. The...

Practical Verification of the Haskell Ranged-sets Library

agda2hs is a project that aims to combine the best parts of Haskell and Agda by providing a common subset between them. It allows programmers to im- plement libraries in Agda, verify their correctness and then translate the result to Haskell so they can be used by Haskell programmers. In this paper, a verified Agda implementation of the Ranged...

Practical Verification of QuadTrees

Agda2hs is a program which compiles a subset of Agda to Haskell. In this paper, an implementation of the Haskell library QuadTree is created and verified in this subset of Agda, such that Agda2hs can then produce a verified Haskell implementation. To aid with this verification, a number of techniques have been proposed which are used to prove...