94 research outputs found
wouter-swierstra/predicate-transformers: ICFP Code
No full text<p>This release contains the code automatically extracted from our 2019 ICFP paper.</p>
wouter-swierstra/predicate-transformers: ICFP Code
No full text<p>This release contains the code automatically extracted from our 2019 ICFP paper.</p>
Program Logics for Ledgers
Get PDFDistributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant
Pi-Ware: Hardware Description and Verification in Agda
No full textThere is a long tradition of modelling digital circuits using functional programming languages. This paper demonstrates that by employing dependently typed programming languages, it becomes possible to define circuit descriptions that may be simulated, tested, verified and synthesized using a single language. The resulting domain specific embedded language, Pi-Ware, makes it possible to define and verify entire families of circuits at once. We demonstrate this by defining an algebra of parallel prefix circuits, proving their correctness and further algebraic properties
HEMAN
No full textMusical pattern annotations dataset in paper: Investigating Musical Pattern Ambiguity in a Human Annotated Dataset. Iris Yuping Ren, Oriol Nieto, Hendrik Vincent Koops, Anja Volk, and Wouter Swierstra. ICMPC2018
A functional specification of effects
Get PDFThis dissertation is about effects and type theory.
Functional programming languages such as Haskell illustrate how to encapsulate side effects using monads. Haskell compilers provide a handful of primitive effectful functions. Programmers can construct larger computations using the monadic return and bind operations.
These primitive effectful functions, however, have no associated definition. At best, their semantics are specified separately on paper. This can make it difficult to test, debug, verify, or even predict the behaviour of effectful computations.
This dissertation provides pure, functional specifications in Haskell of several different effects. Using these specifications, programmers can test and debug effectful programs. This is particularly useful in tandem with automatic testing tools such as QuickCheck.
The specifications in Haskell are not total. This makes them unsuitable for the formal verification of effectful functions. This dissertation overcomes this limitation, by presenting total functional specifications in Agda, a programming language with dependent types.
There have been alternative approaches to incorporating effects in a dependently typed programming language. Most notably, recent work on Hoare Type Theory proposes to extend type theory with axioms that postulate the existence of primitive effectful functions. This dissertation shows how the functional specifications implement these axioms, unifying the two approaches.
The results presented in this dissertation may be used to write and verify effectful programs in the framework of type theory
A Hoare logic for the state monad: Proof pearl
No full textThis pearl examines how to verify functional programs written using the state monad. It uses Coq\u27s Program framework to provide strong specifications for the standard operations that the state monad supports, such as return and bind. By exploiting the monadic structure of such programs during the verification process, it becomes easier to prove that they satisfy their specification
Sorted, verifying the problem of the Dutch national flag in type theory
Get PDFContains fulltext :
92350.pdf (Publisher’s version ) (Open Access
On the semantics of exceptions for high level and low level languages
Get PDFThe thesis deals with correctness of a compiler of a simple language featuring exceptions. We present formal semantics, both denotational semantics of a~high-level language and operational semantics of a low-level language for a~simple stack machine. We study the method of stack unwinding and then iteratively, improving upon a naive solution, we present a different method that is structurally recursive and thus suitable for implementation in total dependently typed languages. Finally, we provide an implementation of the compiler in the dependently typed functional programming language Agda, along with a mechanically verifiable proof of adherence of the implementation to the semantics
On the semantics of exceptions for high level and low level languages
No full textThe thesis deals with correctness of a compiler of a simple language featuring exceptions. We present formal semantics, both denotational semantics of a~high-level language and operational semantics of a low-level language for a~simple stack machine. We study the method of stack unwinding and then iteratively, improving upon a naive solution, we present a different method that is structurally recursive and thus suitable for implementation in total dependently typed languages. Finally, we provide an implementation of the compiler in the dependently typed functional programming language Agda, along with a mechanically verifiable proof of adherence of the implementation to the semantics
- …
