 document

Holten, Lucas (author)Writing software that follows its specification is important for many applications. One approach to guarantee this is formal verification in a dependentlytyped programming language. Formal verification in these dependentlytyped languages is based on proof writing. Sadly, while proofs are easy to check for computers, writing proofs can be...master thesis 2023
 document

Stanciu, Ciprian (author)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...bachelor thesis 2023
 document

Todorov, Rado (author)Category theory is a branch of abstract mathematics that aims to give a highlevel 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. Computerchecked libraries contain all...bachelor thesis 2023
 document

Farkas, Csanád (author)Category Theory is a widely used field of Mathematics.<br/>Some concepts from it are often used in functional programming.<br/>This paper will focus on the Monad and a few implementations of it from Haskell.<br/>We will also present the computerchecked library we have written to help us in this task.bachelor thesis 2023
 document

Orav, Markus (author)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...bachelor thesis 2023
 document

Broekhoff, Jochem (author)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...bachelor thesis 2022
 document

Massar, Marnix (author)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...bachelor thesis 2022
 document

Janjić, Luka (author)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 correctbydesign. A program written a...bachelor thesis 2022
 document

Peeters, Hector (author)Agda is a functional programming language with builtin 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 typerelated errors slipping through the compilation process. <br/>When...bachelor thesis 2022
 document

Haršáni, Alex (author)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...bachelor thesis 2022
 document

Schrijver, Remco (author)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,...bachelor thesis 2022
 document

Schifferstein, Michelle (author)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,...bachelor thesis 2022
 document

Meluzzi, Matteo (author)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...bachelor thesis 2022
 document

Milliken, Louis (author)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...bachelor thesis 2022
 document

Sabharwal, Dixit (author)Equational reasoning based verification address some of the limitations of classical testing. The CurryHoward 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. ...bachelor thesis 2021
 document

Anand, Shashank (author)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...bachelor thesis 2021
 document

Savu, Ioana (author)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...bachelor thesis 2021