Cv

C.R. van der Rest

Authored

3 records found

Hefty Algebras

Modular Elaboration of Higher-Order Algebraic Effects

Algebraic effects and handlers is an increasingly popular approach to programming with effects. An attraction of the approach is its modularity: effectful programs are written against an interface of declared operations, which allows the implementation of these operations to be d ...
How can we enumerate the inhabitants of an algebraic datatype? This paper explores a datatype generic solution that works for all regular types and indexed families. The enumerators presented here are provably both complete and unique - they will eventually produce every value ex ...
Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require m ...

Contributed

9 records found

Programming With Effects

Improving the quality of code in IO intensive applications through effect handlers

Effect handler orient programming (EHOP) is a recently proposed programming paradigm that aims to provide a high-level abstraction in code. Using this paradigm, programmers are able to define operations as an effect, which are implemented by an effect handler. Functions can then ...
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 d ...
Grading and giving feedback to student submissions automatically is becoming more and more necessary with an increasing amount of students. To verify the correctness of student-written definitional interpreters, a program equivalence approach has been implemented, improved, and e ...
Algebraic effects and handlers have become a popular abstraction for effectful computation, with implementations even in mainstream programming languages, such as OCaml. The operations of an algebraic effect define the syntax of the effect, while handlers define the semantics. Th ...
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 unif ...
Effect Handler Oriented Programming is a promising new programming paradigm, delivering separation of of concerns with regards to side effects in an otherwise functional environment. This paper discusses the applicability of this new paradigm to static code analysis programs. Di ...
Definitional interpreters are difficult to test with a pre-defined test suite. This paper tries to determine the effectiveness of automatic testing of definitional interpreters, using concolic execution. First we develop a model for concolic execution of a functional language. ...
Manually testing definitional interpreters and their type checkers is a tedious and error-prone process which can largely benefit from automation. This study evaluates the effectiveness of property-based testing on errors in type checkers. Metrics used include the ability to catc ...
Effect handler oriented programming (EHOP) is a recently proposed programming paradigm, which aims to provide a separation of concerns by isolating the handling of side-effects from the main application logic. Nowadays, as the core concepts behind EHOP are being added to more and ...