Formally proving the correctness of the (un)currying refactoring: Using Agda with a simple Haskell-like programming language

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

Proving correctness of refactoring tuples to records: A correct-by-construction approach on a Haskell-like language

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

The monad and examples from Haskell: A computer-checked library for Category Theory in Lean

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 computer-checked library we have written to help us in this task.

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

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

Deriving a Symbolic Executor for Definitional Interpreters Suitable for the Study of Heuristics

Recent years have seen a surge of interest for dynamic testing techniques, one of which is symbolic execution. It is the main point of interest of this research paper, in which we give an overview of a framework for symbolically executing definitional interpreters. We will also discuss techniques that we made use of in developing the symbolic...

Validating Definitional Interpreters Using Property-Based Testing

This paper presents an evaluation of different generation methods of input expressions to definitional interpreters. We compare three different ways of generating expressions of a specified algebraic data type. The approaches that we describe are QuickCheck, SmallCheck and a uniform generation technique, as laid out in their original papers....