Pages
- 1
- 2
- document
-
Todorov, Ivan (author)The process of using formal verification, in order to ensure that a piece of software meets it functional requirements consists of three main steps: designing a model of the given piece of software, translating the functional requirements, which the piece of software must satisfy, into properties of said model and verifying that the model...master thesis 2024
- document
-
Stuijt Giacaman, Willem (author)The Language Server Protocol (LSP) is a protocol that standardizes the way Integrated Development Environments (IDEs) and text editors communicate with language servers to provide language-specific features like autocompletion, go-to-definition, and diagnostics. While LSP has been widely adopted by mainstream programming languages, its adoption...master thesis 2024
- document
-
Rogers, Eben (author)When writing functional code that composes multiple recursive functions that operate on a datastrcuture, we often incur a lot of computational overhead allocating memory, only to later read, use, and discard this information.<br/>This can be alleviated using fusion, a technique that combines these multiple recursive datastructure traversals into...master thesis 2024
- document
-
Lieverse, Kayleigh (author)Dependently-typed languages allow one to guarantee correctness of a program by providing formal proofs. The type checkers of such languages elaborate the user-friendly high-level surface language to a small and fully explicit core language. A lot of trust is put into this elaboration process, even though it is rarely verified. One such...master thesis 2024
- 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 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...master thesis 2023
- document
-
de Bruin, Ivar (author)Agda is a language used to write computer-verified proofs. It has a module system that provides namespacing, module parameters and module aliases. These parameters and aliases can be used to write shorter and cleaner proofs. However, the current implementation of the module system has several problems, such as an exponential desugaring of module...master thesis 2023
- document
-
de Jong, Jaap (author)How convenient would it be to have an AI that relieves us programmers from the burden of coding? Program synthesis is a technique that achieves exactly that: it automatically generates simple programs that meet a given set of examples or adhere to a provided specification. This is often done by enumerating all programs in the search space and...master thesis 2023
- document
-
Struik, Kalle (author)Refactoring tools are an important tool for developers, but their reliability can be questionable at times. In this paper, we show that it is feasible to formally verify refactoring tools using computer-aided proofs. To this end, we create a Haskell-like language and a refactoring operation on this language to add an extra function argument to...bachelor thesis 2023
- document
-
Jóźwik, Michał (author)When designing critical software, great care must be taken to guarantee its correctness. Refactoring is one of the techniques used to improve code readability, maintainability, and other factors without changing functionality. Thus, to ensure that it is properly applied, automated tools are used to perform refactoring. To ensure that the code...bachelor thesis 2023
- document
-
Padilla Cancio, José (author)This paper concerns itself with correct by construction refactoring of Maybe values to List values in a Haskell-like language (HLL) as a case study on data-oriented refactorings. Our language makes use of intrinsically-typed syntax and de Bruijn indices for variables. Operational semantics are defined using big step semantics. We define a...bachelor thesis 2023
- document
-
Bastenhof, Jeroen (author)Refactoring is a useful tool for increasing the overall quality of software without making changes to how it interacts with the environment. To verify that a refactoring operation correctly transforms an expression, one can provide a formal proof. Using Agda, a dependently-typed language, as a proof assistant, we investigate the feasibility of...bachelor thesis 2023
- document
-
Zandbergen, Timen (author)This paper provides a refactoring from do notation to >>= operators and proves that this refactoring maintains observational equivalence. As programs grow ever larger and more complex, there is a growing need to automatically apply refactorings to these programs in a dependable manner. Current refactoring engines often contain errors, even...bachelor thesis 2023
- document
-
Juhošová, Sára (author)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...master thesis 2023
- document
-
Staal, Martijn (author)Type checkers are invaluable tools which help programmers write correct programs. Fast and efficient type checkers are required to enable adoption of such tools in practice.<br/><br/>This study aims to provide an explorative overview of proposed efficiency improvements for type checkers. This provides language implementers insight in what...bachelor thesis 2023
- document
-
Khakimova, Maria (author)While dependent types can allow programmers to verify properties of their programs, implementing a type checker for a dependent type theory is often difficult. This is due to the fact that, in the presence of dependent types, deciding the equality of types - conversion checking - becomes non-trivial. Due to an identified gap in literature...bachelor thesis 2023
- document
-
Jakovonis, Saulius (author)The success of dynamically typed languages such as Python has resulted in an increased interest in supporting type inference in statically typed lan- guages. Type inference refers to automatic type detection based on surrounding context and allows retaining the type safety (and other advantages) of static types, while matching the ease of use of...bachelor thesis 2023
- document
-
Kocakaya, Hasan (author)Names are essential for structuring and reason-ing about programs. However, the implementation of names differs across many programming lan-guages. There is an bundance of choice between various implementation techniques with regards to name-binding techniques. As such, when design-ing a programming language it is not clear which technique one...bachelor thesis 2023
- document
-
Faraldos Pijoan, Pau (author)Data types and pattern matching are fundamental concepts in programming. Data types define the structure of data, while pattern matching allows efficient manipulation and extraction of the same data. This text provides an overview of different implementation techniques for type systems regarding data types and pattern matching in the existing...bachelor thesis 2023
- document
-
van der Stel, Paul (author)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...master thesis 2022
- 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
Pages
- 1
- 2