Category Theory is a widely used field of Mathematics. Some concepts from it are often used in functional programming. This paper will focus on the Monad and a few implementations of it from Haskell. We will also present the computer-checked library we have written to help us in this task.

Category theory is a branch of abstract mathematics that aims to give a high-level overview of relations between objects. Proof assistants are tools that aid in verifying the correctness of mathematical proofs. To reason about category theory using such assistants, fundamental notions have to be defined. Computer-checked libraries contain all relevant structures and theorems in an accessible way for end users. However, current libraries of category theory are not welcoming to people without in-depth domain knowledge. This paper introduces a library of category theory tailored towards newcomers to the field as well as the learning journey of the authors. We describe the project’s structure, design choices and provide examples of the main features. Moreover, a detailed overview is provided of F-algebras and their relation with inductive data types found in functional programming languages. Construction and evaluation of types like lists and binary trees can be defined in terms of algebras. They provide a general framework for recursion over these types which allow us to reason about them with simple functions.

Existing implementations of category theory for proof assistants aim to be as generic as possible in order to be reusable and extensible, often at the expense of readability and clarity. We present a (partial) formalisation of category theory in the proof assistant Lean limited in purpose to explaining currying, intended to be faithful to the language and definitions used in mathematics literature. We also present some design features of our library and contrast the extent and educational merit with other implementations.

Category theory is a branch of mathematics that is used to abstract and generalize other mathematical concepts. Its core idea is to take the emphasis off the details of the elements of these concepts and put it on the relationships between them instead. The elements can then be characterized in terms of their relationships using various universal properties. The goal of this project was to implement a pedagogical library of category theory in the computer proof assistant Lean, a software tool for formalizing mathematics, and provide a different perspective on various functional programming concepts by finding parallels between them and the universal properties of category theory.

This research project aims to develop a computer-checked library of category theory within the Lean proof assistant, with a specific emphasis on concepts and examples relevant to functional programming. Category theory offers a robust mathematical framework that allows for the abstraction and comprehension of concepts across diverse fields, including computer science. Additionally, the project will explore the application of final coalgebras, particularly in the context of understanding infinite data structures. By creating a formalized category theory library within Lean, our objective is to enhance our understanding of functional programming and programming language concepts. Moreover, we aim to facilitate the study of these topics by providing a comprehensible library and a rigorous foundation for program reasoning, thereby benefiting researchers and practitioners in the field.

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, this paper investigates how Agda2hs can be used to automate the verification process in Agda, while keeping the advantages of having our code available in Haskell. This paper shows how Agda2hs enables the partial verification of a simple Haskell concurrency model. The model is first ported to Agda, staying as close to the original code as possible, and directly compared to the Haskell translation provided by Agda2hs to showcase the readability of the code it produces. Consequently, it is shown how Agda's proof techniques can be used to provide straightforwards proofs of the presence or absence of deadlocks in simple concurrent programs written in this model. Finally, the model's limitations, in particular its deterministic nature, are discussed.

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. We implement the new back-end for Agda in Haskell and we describe the benefits and drawbacks of targeting Java. Firstly we go into the existing methods of compiler Agda, then we go into how to compile Agda to Java and what the main challenges where creating the compiler and what solutions were implemented to solve these. Afterwards Agda2Java is compared to the existing methods of compiling Agda code by means of benchmarks and analyzing the execution time. We show that at its current state, Java does not seem to be a promising back-end for Agda, but that there is work being done on Java that might change this perception.

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 agda2hs project identifies a common subset of Agda and Haskell and translates this subset from Agda to readable Haskell, which enables programmers to write and verify code in Agda, and use it in Haskell. This provides the guarantees of verification to the translated code in Haskell, a language that does not support verification. The objective of this paper is to investigate the possibility of producing a verified implementation of the Haskell library Data.Sequence using the common subset identified by agda2hs. A description of the implementation and verification of Data.Sequence in Agda is provided. A proof technique using arbitrarily nested types is examined in detail. Possible reductions to the cost of the verification process are discussed.

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 if there are other potential target languages that could do a better job. The purpose of this paper is to investigate the efficacy of Forth as a target language for Extraction from Agda, in the hopes that Forth may prove to have the potential to be a better target language than the currently used target languages, Haskell and Javascript. Forth is a stack-based, imperative language, meaning that values are pushed and popped from a stack through the use of ’words’ instead of passing and returning values with functions, as is the case in most languages. Agda is a dependently typed, purely functional language. A dependent type is a type whose definition depends on another value, which allows for types with very specific information, such as a ’Vec n’ representing an array of length ’n’. These dependent types are used to write code with more certainty about its correctness and behaviour. Overall, Forth can be used as a target language to compile Agda code, however many of the advantages of Forth are squandered by executing code written and structured with Agda in mind, making it a rather ineffective target language when compared to other solutions such as Haskell.

Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in an interactive theorem prover and then transpile it into a more popular programming language. We use Agda2HS as a case study to determine what challenges users find in using such a tool, improve selected features, and then conduct a user study to evaluate the usability. We find that detailed documentation, support for commonly-used features in the target programming language, features that facilitate verification, integration of the tool into the target ecosystem, and user studies are necessary for the accessibility of such a tool.

Writing software that follows its specification is important for many applications. One approach to guarantee this is formal verification in a dependently-typed programming language. Formal verification in these dependently-typed languages is based on proof writing. Sadly, while proofs are easy to check for computers, writing proofs can be tedious for developers. One particular proof component that currently requires developers attention in many systems, is associative and commutative (AC) reasoning. We contribute an extension of dependent type-systems to fully automate AC reasoning. This alleviates developers from this task and allows them to concentrate on other proof components. Our approach works by modifying the conversion checker and doesn't compromise soundness or completeness. Furthermore, our approach reuses existing type-checking components, making it easier to implement. We also implemented our theory as an extension of the Agda type-checker. This allowed us to use this implementation to experiment with some example programs. This thesis can help language designers decide if they want automatic AC reasoning in their language. For language users it can serve as inspiration on how to use such a type-system and finally for researchers we have ideas for future work.

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 and perform an empirical benchmark analysis. We show that LLVM’s Intermediate Representation language is a usable and promising target, although some optimizations are necessary before broader application. More indirect paths towards LLVM IR appear more suitable, because of the large translation gap.

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 largely unexplored in the context of Agda2hs. In this paper, we investigate the Reader monad, which gives us a way to model the global state. As monads are in practice commonly combined with other monads, we also investigate the transformer ReaderT. This paper provides the implementation of Reader and ReaderT in Agda, verifies its properties based on laws of type classes functor, applicative, and monad, as well as monad transformer laws for ReaderT, and assesses whether Agda2hs produces their correct and useful translation.

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, rudimentary structures can be translated to Haskell from Agda with agda2hs. In this paper the translation and verification of infinite structures to readable Haskell code is researched. This allows for future work to be done on verification of more complex libraries because the concept of infinite structures is used often in Haskell. The results of the research were that translation of rudimentary infinite structures is possible, but functions creating infinite structures cannot be translated at this point in time.

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 assistant. The functions are first converted to total functions and the preconditions the are proven. Verifying an abstract class is time consuming, since it requires an implemented instance of the abstract class. Stating the properties of the library is possible, but difficult since it requires generalised properties that need to be valid for all instances of the abstract class. The verification process is not completed yet, so no definitive conclusions are made, but the properties that are verified did not produce any issues. agda2hs is used to compile the Agda code to Haskell, this ensures that the verified Agda code is verified Haskell code. This requires the library to fall within the common subset of 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. ‘agda2hs’ attempts to bring this formal verification to the Haskell ecosystem, by providing a translation between Haskell and Agda programs. This project will serve to test the viability of this framework by re-writing the Haskell library ‘Data.Map’ in the subset of Agda defined by agda2hs and verifying properties of various functions in the library using Agda and dependent types.

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 functionally pure way. We show successfully verified lenses for record types and tuples, and also present a lens operating on lists that could not be translated properly. We discuss the obstacles encountered during development, and offer thoughts on possible improvements to agda2hs.

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. When executing Agda code, it is first compiled into a different programming language. This process is called code extraction. This step is applied since most of the typed code becomes unnecessary after type-checking and can therefore be removed. Currently, the Agda compiler supports only Haskell and JavaScript as target languages. However, exploring Rust as a target language could potentially lead to better performance, and it would allow access to the Rust library ecosystem. Overall, the agda2rust backend could be a viable alternative to what is currently available. While it is not fully feature-complete and will not outperform any existing backends yet, agda2rust provides a way to seamlessly integrate algorithms and data structures implemented and proven in Agda into an existing Rust codebase.

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. This paper describes the implementation of a new Agda compiler that targets the Higher-Order Virtual Machine (HVM). Firstly we outline the theoretical benefits of using an optimal functional language such as HVM. Secondly, we present the problems we faced and the solutions we devised in the implementation of the agda2hvm compiler. Lastly, we compare our implementation to the current best Agda compilers by running benchmarks and analyzing both time and space performance. We obtained results ranging from our compiler being exponentially faster than the state-of-the-art to being exponentially slower.

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 invariants, preconditions and post-conditions of the QuadTree library. Using these techniques, the properties of the library have been proven. Additionally, recommendations are made to reduce the time needed for verification.