-
Translation Certification for Smart Contracts
Authors:
Jacco O. G. Krijnen,
Manuel M. T. Chakravarty,
Gabriele Keller,
Wouter Swierstra
Abstract:
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high financial value, in an adversarial environment and, once committed to the blockchain, they cannot be changed anymore. Smart contracts are typically developed i…
▽ More
Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control assets, which are often of high financial value, in an adversarial environment and, once committed to the blockchain, they cannot be changed anymore. Smart contracts are typically developed in a high-level contract language and compiled to low-level virtual machine code before being committed to the blockchain. For a smart contract user to trust a given piece of low-level code on the blockchain, they must convince themselves that (a) they are in possession of the matching source code and (b) that the compiler faithfully translated the source code's semantics.
Classic approaches to compiler correctness tackle the second point. We argue that translation certification also addresses the first. We describe the proof architecture of a novel translation certification framework, implemented in Coq, for a functional smart contract language. We demonstrate that we can model the compilation pipeline as a sequence of translation relations that facilitate a modular proof approach and are robust in the face of an evolving compiler implementation.
△ Less
Submitted 22 February, 2022; v1 submitted 13 January, 2022;
originally announced January 2022.
-
A Computational Evaluation of Musical Pattern Discovery Algorithms
Authors:
Iris Ren,
Anja Volk,
Wouter Swierstra,
Remco C. Veltkamp
Abstract:
Pattern discovery algorithms in the music domain aim to find meaningful components in musical compositions. Over the years, although many algorithms have been developed for pattern discovery in music data, it remains a challenging task. To gain more insight into the efficacy of these algorithms, we introduce three computational methods for examining their output: Pattern Polling, to combine the pa…
▽ More
Pattern discovery algorithms in the music domain aim to find meaningful components in musical compositions. Over the years, although many algorithms have been developed for pattern discovery in music data, it remains a challenging task. To gain more insight into the efficacy of these algorithms, we introduce three computational methods for examining their output: Pattern Polling, to combine the patterns; Comparative Classification, to differentiate the patterns; Synthetic Data, to inject predetermined patterns. In combining and differentiating the patterns extracted by algorithms, we expose how they differ from the patterns annotated by humans as well as between algorithms themselves, with rhythmic features contributing the most to the algorithm-human and algorithm-algorithm discrepancies. Despite the difficulty in reconciling and evaluating the divergent patterns extracted from algorithms, we identify some possibilities for addressing them. In particular, we generate controllable synthesised data with predetermined patterns planted into random data, thereby leaving us better able to inspect, compare, validate, and select the algorithms. We provide a concrete example of synthesising data for understanding the algorithms and expand our discussion to the potential and limitations of such an approach.
△ Less
Submitted 23 October, 2020;
originally announced October 2020.
-
Combining predicate transformer semantics for effects: a case study in parsing regular languages
Authors:
Anne Baanen,
Wouter Swierstra
Abstract:
This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our previous work in this area focused on the semantics for a single effect, parsing requires a combination of effects: non-determinism, general recursion and mutable state. Reasoning about such combinations of effects is n…
▽ More
This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our previous work in this area focused on the semantics for a single effect, parsing requires a combination of effects: non-determinism, general recursion and mutable state. Reasoning about such combinations of effects is notoriously difficult, yet our approach using predicate transformers enables the careful separation of program syntax, correctness proofs and termination proofs.
△ Less
Submitted 30 April, 2020;
originally announced May 2020.
-
Forty hours of declarative programming: Teaching Prolog at the Junior College Utrecht
Authors:
Jurriën Stutterheim,
Wouter Swierstra,
Doaitse Swierstra
Abstract:
This paper documents our experience using declarative languages to give secondary school students a first taste of Computer Science. The course aims to teach students a bit about programming in Prolog, but also exposes them to important Computer Science concepts, such as unification or searching strategies. Using Haskell's Snap Framework in combination with our own NanoProlog library, we have deve…
▽ More
This paper documents our experience using declarative languages to give secondary school students a first taste of Computer Science. The course aims to teach students a bit about programming in Prolog, but also exposes them to important Computer Science concepts, such as unification or searching strategies. Using Haskell's Snap Framework in combination with our own NanoProlog library, we have developed a web application to teach this course.
△ Less
Submitted 22 January, 2013;
originally announced January 2013.
-
From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine
Authors:
Wouter Swierstra
Abstract:
This paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda.
This paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda.
△ Less
Submitted 13 February, 2012;
originally announced February 2012.
