Cv
C.R. van der Rest
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
5 records found
1
Type systems are a tool for preventing software errors, by classifying (sub)terms according to how they are evaluated. This way, mistakes can be caught at compile-time, ruling out the existence of entire classes of mistakes altogether. Using a programming language with a strong type system to develop critical software can dramatically reduce the prevalence and impact of bugs.
In light of the potentially enormous impact of bugs, it is important that we can trust a type system to be succesful in preventing errors. A key property of type systems that reflects this criterium is type soundness, which establishes that “well-typed programs cannot go wrong”. That is, programs that are deemed safe by the type system should not exhibit certain wrong behaviour when executed. To gain trust in a type system’s ability to prevent errors, we can give a formal system of both a language’s type system and semantics, and mathematically verify that the type system is sound with respect to the defined semantics. While this provides airtight evidence that a type system is succesful in ruling out certain mistakes, the formal specification and verification of programming languages requires a formidable amount of time and expertise on behalf of the language designer, and is therefore infeasible in most cases.... ...
In light of the potentially enormous impact of bugs, it is important that we can trust a type system to be succesful in preventing errors. A key property of type systems that reflects this criterium is type soundness, which establishes that “well-typed programs cannot go wrong”. That is, programs that are deemed safe by the type system should not exhibit certain wrong behaviour when executed. To gain trust in a type system’s ability to prevent errors, we can give a formal system of both a language’s type system and semantics, and mathematically verify that the type system is sound with respect to the defined semantics. While this provides airtight evidence that a type system is succesful in ruling out certain mistakes, the formal specification and verification of programming languages requires a formidable amount of time and expertise on behalf of the language designer, and is therefore infeasible in most cases.... ...
Type systems are a tool for preventing software errors, by classifying (sub)terms according to how they are evaluated. This way, mistakes can be caught at compile-time, ruling out the existence of entire classes of mistakes altogether. Using a programming language with a strong type system to develop critical software can dramatically reduce the prevalence and impact of bugs.
In light of the potentially enormous impact of bugs, it is important that we can trust a type system to be succesful in preventing errors. A key property of type systems that reflects this criterium is type soundness, which establishes that “well-typed programs cannot go wrong”. That is, programs that are deemed safe by the type system should not exhibit certain wrong behaviour when executed. To gain trust in a type system’s ability to prevent errors, we can give a formal system of both a language’s type system and semantics, and mathematically verify that the type system is sound with respect to the defined semantics. While this provides airtight evidence that a type system is succesful in ruling out certain mistakes, the formal specification and verification of programming languages requires a formidable amount of time and expertise on behalf of the language designer, and is therefore infeasible in most cases....
In light of the potentially enormous impact of bugs, it is important that we can trust a type system to be succesful in preventing errors. A key property of type systems that reflects this criterium is type soundness, which establishes that “well-typed programs cannot go wrong”. That is, programs that are deemed safe by the type system should not exhibit certain wrong behaviour when executed. To gain trust in a type system’s ability to prevent errors, we can give a formal system of both a language’s type system and semantics, and mathematically verify that the type system is sound with respect to the defined semantics. While this provides airtight evidence that a type system is succesful in ruling out certain mistakes, the formal specification and verification of programming languages requires a formidable amount of time and expertise on behalf of the language designer, and is therefore infeasible in most cases....
Algebraic effects and handlers is an increasingly popular paradigm for programming with effects. A key benefit is modularity: programs with effects are defined against an interface of operations, allowing the implementation of effects to be defined and refined without changing or recompiling programs. The behavior of effects is specified using equational theories, with equational proofs inheriting the same modularity. However, higher-order operations (that take computations as arguments) break this modularity: while they can often be encoded in terms of algebraic effects, this typically breaks modularity as operations defined this way are not encapsulated in an interface, inducing changes to programs and proofs upon refinement of the implementation. In this paper, we show that syntactic overloading is a viable solution to this modularity problem by defining hefty algebras: a formal framework that captures an overloading-based semantics of higher-order effects by defining modular elaborations from higher-order effect trees into primitive algebraic effects. We demonstrate how this approach scales to define a wide range of known higher-order effects from the literature and develop modular higher-order effect theories and modular reasoning principles that build on and extend the state of the art in modular algebraic effect theories. We formalize our contributions in Agda.
...
Algebraic effects and handlers is an increasingly popular paradigm for programming with effects. A key benefit is modularity: programs with effects are defined against an interface of operations, allowing the implementation of effects to be defined and refined without changing or recompiling programs. The behavior of effects is specified using equational theories, with equational proofs inheriting the same modularity. However, higher-order operations (that take computations as arguments) break this modularity: while they can often be encoded in terms of algebraic effects, this typically breaks modularity as operations defined this way are not encapsulated in an interface, inducing changes to programs and proofs upon refinement of the implementation. In this paper, we show that syntactic overloading is a viable solution to this modularity problem by defining hefty algebras: a formal framework that captures an overloading-based semantics of higher-order effects by defining modular elaborations from higher-order effect trees into primitive algebraic effects. We demonstrate how this approach scales to define a wide range of known higher-order effects from the literature and develop modular higher-order effect theories and modular reasoning principles that build on and extend the state of the art in modular algebraic effect theories. We formalize our contributions in Agda.
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 defined and refined without changing or recompiling programs written against the interface. However, higher-order operations (i.e., operations that take computations as arguments) break this modularity. While it is possible to encode higher-order operations by elaborating them into more primitive algebraic effects and handlers, such elaborations are typically not modular. In particular, operations defined by elaboration are typically not a part of any effect interface, so we cannot define and refine their implementation without changing or recompiling programs. To resolve this problem, a recent line of research focuses on developing new and improved effect handlers. In this paper we present a (surprisingly) simple alternative solution to the modularity problem with higher-order operations: we modularize the previously non-modular elaborations commonly used to encode higher-order operations. Our solution is as expressive as the state of the art in effects and handlers.
...
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 defined and refined without changing or recompiling programs written against the interface. However, higher-order operations (i.e., operations that take computations as arguments) break this modularity. While it is possible to encode higher-order operations by elaborating them into more primitive algebraic effects and handlers, such elaborations are typically not modular. In particular, operations defined by elaboration are typically not a part of any effect interface, so we cannot define and refine their implementation without changing or recompiling programs. To resolve this problem, a recent line of research focuses on developing new and improved effect handlers. In this paper we present a (surprisingly) simple alternative solution to the modularity problem with higher-order operations: we modularize the previously non-modular elaborations commonly used to encode higher-order operations. Our solution is as expressive as the state of the art in effects and handlers.
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 many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components: language fragments. Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.
...
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 many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components: language fragments. Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.
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 exactly once - and fair - they avoid bias when composing enumerators. Finally, these enumerators memoise previously enumerated values whenever possible, thereby avoiding repeatedly recomputing recursive results.
...
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 exactly once - and fair - they avoid bias when composing enumerators. Finally, these enumerators memoise previously enumerated values whenever possible, thereby avoiding repeatedly recomputing recursive results.