26,098 papers · page 89 of 1,305
Unix and Smalltalk are very different in the details, but bear curious similarities in their broad outlines. Prior work has made these comparisons at a high level and sketched a path for retrofitting Smalltalk's advantages onto Unix (without compromising the advantages of the lat…
Formal Methods (FM) will not arrive with fanfare. It will spread quietly, not as a revolution, but as a patch: reviewed, merged, and dismissed. In the coming century, the decades-old practice of simply testing code will collapse under the weight of cyberattacks and development co…
Abstract One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to main…
Abstract OCaml Blockly is a block-based programming environment for a subset of the functional language OCaml, developed based on Google Blockly. The distinct feature of OCaml Blockly is that it knows the scoping and typing rules of OCaml. As such, for any complete program in OCa…
Abstract The tensor notation used in several areas of mathematics is a useful one, but it is not widely available to the functional programming community. In a practical sense, the (embedded) domain-specific languages ( dsl s) that are currently in use for tensor algebra are eith…
Abstract One of the natural problems of operational semantics is to characterise the relationship between eager and lazy evaluation. In the context of $\lambda$ -calculus, this is expressed by the classic theorem that call-by-value evaluation of a program to (weak-head) normal fo…
Abstract This paper reports on the experiences of using an early assessment intervention, specifically employing a Use-Modify-Create scaffold, to teach first-year undergraduate functional programming. The particular intervention that was trialled was the use of an early assessmen…
Abstract This paper introduces Choice Trees (CTrees), a monad for modeling nondeterministic, recursive, and impure programs in Rocq . Inspired by Xia et al .’s ((2019) Proc. ACM Program. Lang. 4 (POPL)) ITrees, this novel data structure embeds computations into coinductive trees …
Abstract We present a novel approach to synthesizing recursive functional programs from input–output examples. Synthesizing a recursive function is challenging because recursive subexpressions should be constructed while the target function has not been fully defined yet. We addr…
The setting is a tutorial on program verification in Agda. Please consult the programme for further details. [ See also Appendix A .]
Abstract Structural induction is pervasively used by functional programmers and researchers for both informal reasoning as well as formal methods for program verification and semantics. In this paper, we promote its dual—structural coinduction—as a technique for understanding cor…
Abstract Functional programmers have many things for which to thank the late David Turner: design decisions he made in his languages SASL, KRC, and Miranda over the last 50 years are still influential and inspirational now. In particular, Turner was a strong advocate of lazy eval…
Abstract The formal theory of monads shows that much of the theory of monads can be developed in the abstract at the level of 2-categories. This means that results about monads can be established once and for all and simply instantiated in settings such as enriched category theor…
The goal of this thesis is to verify smart contracts in Blockchain.In particular, we focus on smart contracts in Bitcoin and Solidity.In order to specify the correctness of smart contracts, we use weakest preconditions.For this, we develop a model of smart contracts in the intera…
Abstract Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additional…
Abstract We propose a notion of syntax with metavariables that generalises Miller’s decidable pattern fragment of second-order unification for simply typed $\lambda$ -calculus. Using categorical semantics, we show that, under some conditions, a generalisation of Miller’s unificat…
Abstract The tail recursion modulo cons transformation can rewrite functions that are not quite tail-recursive into a tail-recursive form that can be executed efficiently. In this article, we generalize tail recursion modulo cons (TRMc) to modulo context (TRMC) and calculate a ge…
Abstract This theoretical pearl shows how a graphical, relational, point-free, and calculational approach to linear algebra, known as graphical linear algebra, can be used to reason not only about matrices (and matrix algebra, as can be found in the literature) but also vector sp…