1,720,952 research outputs found
Practical generic programming over a universe of native datatypes
No full textDatatype-generic programming makes it possible to define a construction once and apply it to a large class of datatypes. It is often used to avoid code duplication in languages that encourage the definition of custom datatypes, in particular state-of-the-art dependently typed languages where one can have many variants of the same datatype with different type-level invariants. In addition to giving access to familiar programming constructions for free, datatype-generic programming in the dependently typed setting also allows for the construction of generic proofs. However, the current interfaces available for this purpose are needlessly hard to use or are limited in the range of datatypes they handle. In this paper, we describe the design of a library for safe and user-friendly datatype-generic programming in the Agda language. Generic constructions in our library are regular Agda functions over a broad universe of datatypes, yet they can be specialized to native Agda datatypes with a simple one-liner. Furthermore, we provide building blocks so that library designers can too define their own datatype-generic constructions.Programming Language
Practical Verification of QuadTrees
No full textAgda2hs 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.https://github.com/JonathanBrouwer/research-project GitHub reposity of the projectCSE3000 Research ProjectComputer Science and Engineerin
Practical Verification of a Free Monad Instance
No full textFormal 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 proof assistant language Agda, along with the proof of its correctness, can be translated to the readable Haskell equivalent, retaining only the functionally relevant aspects and leaving the proof related aspects of the code behind. This paper describes research done into the current abilities of agda2hs on the use case of verifying properties of free monads, a higher order type with potential for use in implementation of domain specific languages and purely functional and modular handling of effects. In order to represent an aspect of the type in a general way I used containers, a uniform way of representing types that store data. This led me to a limitation of agda2hs: while the tool in its current state can only handle direct translations from a common subset of the two languages, in order to translate my definition of the data type I needed a more fine grained control of the translation process which the tool could not provide.CSE3000 Research ProjectComputer Science and Engineerin
Comparing Code extraction from Agda to Java to existing Methods
No full textDependent 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.CSE3000 Research ProjectComputer Science and Engineerin
A Computer-Checked Library of Category Theory: Functors and F-Coalgebras
No full textThis 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.CSE3000 Research ProjectComputer Science and Engineerin
Code extraction from Agda to HVM
No full textDependently 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.CSE3000 Research ProjectComputer Science and Engineerin
The monad and examples from Haskell: A computer-checked library for Category Theory in Lean
No full textCategory 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.https://github.com/sgciprian/ctCSE3000 Research ProjectComputer Science and Engineerin
Extracting LLVM Intermediate Representation from Agda
No full textAgda, 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.CSE3000 Research ProjectComputer Science and Engineerin
A computer-checked library of category theory: Defining functors and their algebras
No full textCategory 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.CSE3000 Research ProjectComputer Science and Engineerin
Dependent Type-Checking Modulo Associativity and Commutativity
No full textWriting 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.https://github.com/LHolten/agda-commassoc Source code for the Agda implementation of definitional AC functions.Computer Science | Software Technolog
- …
