title: Iterating on multiple collections in synchrony

authors:
Stefano Perna
Val Tannen
Limsoon Wong

abstract: Abstract Modern programming languages typically provide some form of comprehension syntax which renders programs manipulating collection types more readable and understandable. However, comprehension syntax corresponds to nested loops in general. There is no simple way of using it to express efficient general synchronized iterations on multiple ordered collections, such as linear-time algorithms for low-selectivity database joins. Synchrony fold is proposed here as a novel characterization of synchronized iteration. Central to this characterization is a monotonic isBefore predicate for relating the orderings on the two collections being iterated on and an antimonotonic canSee predicate for identifying matching pairs in the two collections to synchronize and act on. A restriction is then placed on Synchrony fold, cutting its extensional expressive power to match that of comprehension syntax, giving us Synchrony generator . Synchrony generator retains sufficient intensional expressive power for expressing efficient synchronized iteration on ordered collections. In particular, it is proved to be a natural generalization of the database merge join algorithm, extending the latter to more general database joins. Finally, Synchrony iterator is derived from Synchrony generator as a novel form of iterator. While Synchrony iterator has the same extensional and intensional expressive power as Synchrony generator, the former is better dovetailed with comprehension syntax. Thereby, algorithms requiring synchronized iterations on multiple ordered collections, including those for efficient general database joins, become expressible naturally in comprehension syntax.


venue: jfp

title: Back to futures

authors:
Klaas Pruiksma
Frank Pfenning

abstract: Abstract Common approaches to concurrent programming begin with languages whose semantics are naturally sequential and add new constructs that provide limited access to concurrency, as exemplified by futures . This approach has been quite successful, but often does not provide a satisfactory theoretical backing for the concurrency constructs, and it can be difficult to give a good semantics that allows a programmer to use more than one of these constructs at a time. We take a different approach, starting with a concurrent language based on a Curry–Howard interpretation of adjoint logic, to which we add three atomic primitives that allow us to encode sequential composition and various forms of synchronization. The resulting language is highly expressive, allowing us to encode futures, fork/join parallelism, and monadic concurrency in the same framework. Notably, since our language is based on adjoint logic, we are able to give a formal account of linear futures , which have been used in complexity analysis by Blelloch and Reid-Miller. The uniformity of this approach means that we can similarly work with many of the other concurrency primitives in a linear fashion, and that we can mix several of these forms of concurrency in the same program to serve different purposes.


title: A well-known representation of monoids and its application to the function 'vector reverse'

abstract: Abstract Vectors—or length-indexed lists—are classic example of a dependent type. Yet, most tutorials stay clear of any function on vectors whose definition requires non-trivial equalities between natural numbers to type check. This pearl shows how to write functions, such as vector reverse, that rely on monoidal equalities to be type correct without having to write any additional proofs. These techniques can be applied to many other functions over types indexed by a monoid, written using an accumulating parameter, and even be used to decide arbitrary equalities over monoids ‘for free.’


title: Read/write factorizable programs

authors:
Siddharth Bhaskar
Jakob Grue Simonsen

abstract: Abstract In the cons-free programming paradigm, we eschew constructors and program using only destructors. Cons-free programs in a simple first-order language with string data capture exactly P, the class of polynomial-time relations. By varying the underlying language and considering other data types, we can capture several other complexity classes. However, no cons-free programming language captures any functional complexity class for fundamental reasons. In this paper, we cleanly extend the cons-free paradigm to encompass functional complexity classes. Namely, we introduce programs with data that can either only be destructed or only be constructed, which we enforce by a type system on the program variables. We call the resulting programs read/write - (or RW -)factorizable, show that RW-factorizable string programs capture exactly the class FP of polynomial-time functions, and that tail-recursive RW-factorizable programs capture exactly the class FL of logarithmic-space functions. Finally, we state and solve the nontrivial problem of syntactic composition of two RW-factorizable programs.


title: Is sized typing for Coq practical?

authors:
Jonathan Chan
Yufeng Li
William J. Bowman

abstract: Abstract Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim. Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven’t they been adapted to Coq? In this paper, we venture to answer this question with CIC $\widehat{\ast}$ , a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq’s kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user. In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is impractical in terms of performance.


title: Folding left and right matters: Direct style, accumulators, and continuations

abstract: Abstract The equivalence of folding left and right over Peano numbers and lists makes it possible to minimalistically inter-derive (1) structurally recursive functions in direct style, (2) structurally tail-recursive functions that use an accumulator, and (3) structurally tail-recursive functions in delimited continuation-passing style, using Ohori and Sasano’s lightweight fusion by fixed-point promotion. When the fold-left and the fold-right functions account for primitive iteration for Peano numbers, this equivalence is unconditional. When they account for primitive recursion for Peano numbers, this equivalence is modulo left permutativity of their induction-step parameter – a property which is more general than associativity and commutativity. And when they account for primitive iteration or for primitive recursion over lists, this equivalence is modulo left permutativity of their induction-step parameter if these two fold functions have the same type. Since the 1980s, however, the two fold functions for lists do not have the same type: the arguments for their induction-step parameter are swapped, a re-ordering that complicated Bird and Wadler’s duality theorems and whose history is reviewed in an appendix. Without this re-ordering, Bird and Wadler’s second duality theorem more visibly accounts for “re-bracketing,” which is a key step to make recursive programs tail recursive in the general area of program development, from Cooper in the 1960s and onwards.


title: Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant - ERRATUM


title: Classical (co)recursion: Mechanics

authors:
Paul Downen
Zena M. Ariola

abstract: Abstract Recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, corecursion is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a foundation for primitive corecursion based on computation, giving a terminating calculus analogous to the original computational foundation of recursion. We show how the implementation details in an abstract machine strengthens their connection, syntactically deriving corecursion from recursion via logical duality. We also observe the impact of evaluation strategy on the computational complexity of primitive (co)recursive combinators: call-by-name allows for more efficient recursion, but call-by-value allows for more efficient corecursion.


title: Certified, total serialisers with an application to Huffman encoding

abstract: The other day, I was assembling lecture material for a course on Agda. Pursuing an application-driven approach, I was looking for correctness proofs of popular algorithms. One of my all-time favourites is Huffman data compression (Huffman, 1952). Even though it is probably safe to assume that you are familiar with this algorithmic gem, a brief reminder of the essential idea may not be amiss.


title: Normalization by evaluation for modal dependent type theory

authors:
Jason Z. S. Hu
Junyoung Jang
Brigitte Pientka

abstract: Abstract We present the Kripke-style modal type theory, Mint , which combines dependent types and the necessity modality. It extends the Kripke-style modal lambda-calculus by Pfenning and Davies to the full Martin-Löf type theory. As such it encompasses dependently typed variants of system K , T , K 4, and S 4. Further, Mint seamlessly supports a full universe hierarchy, usual inductive types, and large eliminations. In this paper, we give a modular sound and complete normalization-by-evaluation (NbE) proof for Mint based on an untyped domain model, which applies to all four aforementioned modal systems without modification. This NbE proof yields a normalization algorithm for Mint, which can be directly implemented. To further strengthen our results, our models and the NbE proof are fully mechanized in Agda and we extract a Haskell implementation of our NbE algorithm from it.


title: Programming language semantics: It's easy as 1,2,3

abstract: Abstract Programming language semantics is an important topic in theoretical computer science, but one that beginners often find challenging. This article provides a tutorial introduction to the subject, in which the language of integers and addition is used as a minimal setting in which to present a range of semantic concepts in simple manner. In this setting, it is easy as 1,2,3.


title: PhD Abstracts

abstract: series editor for further details.


title: Level-p-complexity of Boolean functions using thinning, memoization, and polynomials

authors:
Julia Jansson
Patrik Jansson

abstract: Abstract This paper describes a purely functional library for computing level- p -complexity of Boolean functions and applies it to two-level iterated majority. Boolean functions are simply functions from n bits to one bit, and they can describe digital circuits, voting systems, etc. An example of a Boolean function is majority, which returns the value that has majority among the n input bits for odd n . The complexity of a Boolean function f measures the cost of evaluating it: how many bits of the input are needed to be certain about the result of f . There are many competing complexity measures, but we focus on level- p -complexity — a function of the probability p that a bit is 1. The level- p -complexity $D_p(f)$ is the minimum expected cost when the input bits are independent and identically distributed with Bernoulli( p ) distribution. We specify the problem as choosing the minimum expected cost of all possible decision trees — which directly translates to a clearly correct, but very inefficient implementation. The library uses thinning and memoization for efficiency and type classes for separation of concerns. The complexity is represented using (sets of) polynomials, and the order relation used for thinning is implemented using polynomial factorization and root counting. Finally, we compute the complexity for two-level iterated majority and improve on an earlier result by J. Jansson.


title: Trace contracts

authors:
Cameron Moy
Matthias Felleisen

abstract: Abstract Behavioral software contracts allow programmers to strengthen the obligations and promises that they express with conventional types. They lack expressive power, though, when it comes to invariants that hold across several function calls. Trace contracts narrow this expressiveness gap. A trace contract is a predicate over the sequence of values that flow through function calls and returns. This paper presents a principled design, an implementation, and an evaluation of trace contracts.


title: A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go

authors:
Martin Sulzmann
Stefan Wehr

abstract: Abstract Featherweight Generic Go (FGG) is a minimal core calculus modeling the essential features of the programming language Go. It includes support for overloaded methods, interface types, structural subtyping, and generics. The most straightforward semantic description of the dynamic behavior of FGG programs is to resolve method calls based on runtime type information of the receiver. This article shows a different approach by defining a type-directed translation from ${\textrm{FGG}^{-}}$ to an untyped lambda-calculus. ${\textrm{FGG}^{-}}$ includes all features of FGG but type assertions. The translation of an ${\textrm{FGG}^{-}}$ program provides evidence for the availability of methods as additional dictionary parameters, similar to the dictionary-passing approach known from Haskell type classes. Then, method calls can be resolved by a simple lookup of the method definition in the dictionary. Every program in the image of the translation has the same dynamic semantics as its source ${\textrm{FGG}^{-}}$ program. The proof of this result is based on a syntactic, step-indexed logical relation. The step index ensures a well-founded definition of the relation in the presence of recursive interface types and recursive methods. Although being non-deterministic, the translation is coherent.


title: A correct-by-construction conversion from lambda calculus to combinatory logic

abstract: Abstract This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.


title: Contract lenses: Reasoning about bidirectional programs via calculation

authors:
Hanliang Zhang
Wenhao Tang
Ruifeng Xie
Meng Wang
Zhenjiang Hu

abstract: Abstract Bidirectional transformations (BXs) are a mechanism for maintaining consistency between multiple representations of related data. The lens framework, which usually constructs BXs from lens combinators, has become the mainstream approach to BX programming because of its modularity and correctness by construction. However, the involved bidirectional behaviors of lenses make the equational reasoning and optimization of them much harder than unidirectional programs. We propose a novel approach to deriving efficient lenses from clear specifications via program calculation, a correct-by-construction approach to reasoning about functional programs by algebraic laws. To support bidirectional program calculation, we propose contract lenses , which extend conventional lenses with a pair of predicates to enable safe and modular composition of partial lenses. We define several contract-lens combinators capturing common computation patterns including $\textit{fold}, \textit{filter},\textit{map}$ , and $\textit{scan}$ , and develop several bidirectional calculation laws to reason about and optimize contract lenses. We demonstrate the effectiveness of our new calculation framework based on contract lenses with nontrivial examples.


title: An example of goal-directed, calculational proof

authors:
Roland Carl Backhouse
Walter Guttmann
Michael Winter

abstract: Abstract An equivalence relation can be constructed from a given (homogeneous, binary) relation in two steps: first, construct the smallest reflexive and transitive relation containing the given relation (the “star” of the relation) and, second, construct the largest symmetric relation that is included in the result of the first step. The fact that the final result is also reflexive and transitive (as well as symmetric), and thus an equivalence relation, is not immediately obvious, although straightforward to prove. Rather than prove that the defining properties of reflexivity and transitivity are satisfied, we establish reflexivity and transitivity constructively by exhibiting a starth root—in a way that emphasises the creative process in its construction. The resulting construction is fundamental to algorithms that determine the strongly connected components of a graph as well as the decomposition of a graph into its strongly connected components together with an acyclic graph connecting such components.


title: Programming and reasoning about actors that share state

authors:
Samuel Caldwell
Tony Garnock-Jones
Matthias Felleisen

abstract: Abstract Actor languages realize concurrency via message passing, which most of the time is easy to use. Empirical code inspection provides evidence, however, that on occasion, programmers wish to have an actor share some of its state with others. The dataspace model adds a tightly controlled state-exchange mechanism, dubbed dataspace, to the actor model for just this purpose. Experience with dataspaces suggests that this form of sharing calls for linguistic constructs that allow programmers to state temporal aspects of actor conversations. In response, this paper presents the facet notation: its theory, its type system, its behavioral type system, and some first experiences with an implementation.


title: Alice or Bob?: Process polymorphism in choreographies

authors:
Eva Graversen
Andrew K. Hirsch
Fabrizio Montesi

abstract: Abstract We present PolyChor $\lambda$ , a language for higher-order functional choreographic programming —an emerging paradigm for concurrent programming. In choreographic programming, programmers write the desired cooperative behaviour of a system of processes and then compile it into an implementation for each process, a translation called endpoint projection . Unlike its predecessor, Chor $\lambda$ , PolyChor $\lambda$ has both type and process polymorphism inspired by System F $_\omega$ . That is, PolyChor $\lambda$ is the first (higher-order) functional choreographic language which gives programmers the ability to write generic choreographies and determine the participants at runtime. This novel combination of features also allows PolyChor $\lambda$ processes to communicate distributed values , leading to a new and intuitive way to write delegation. While some of the functional features of PolyChor $\lambda$ give it a weaker correspondence between the semantics of choreographies and their endpoint-projected concurrent systems than some other choreographic languages, we still get the hallmark end result of choreographic programming: projected programmes are deadlock-free by design.


title: Asymptotic speedup via effect handlers

authors:
Daniel Hillerström
Sam Lindley
John Longley

abstract: Abstract We study a fundamental efficiency benefit afforded by delimited control, showing that for certain higher-order functions, a language with advanced control features offers an asymptotic improvement in runtime over a language without them. Specifically, we consider the generic count problem in the context of a pure functional base language ${\lambda_{\textrm{b}}}$ and an extension ${\lambda_{\textrm{h}}}$ with general effect handlers . We prove that ${\lambda_{\textrm{h}}}$ admits an asymptotically more efficient implementation of generic count than any implementation in ${\lambda_{\textrm{b}}}$ . We also show that this gap remains even when ${\lambda_{\textrm{b}}}$ is extended to a language ${{{{{{\lambda_{\textrm{a}}}}}}}}$ with affine effect handlers , which is strong enough to encode exceptions, local state, coroutines and single-shot continuations. This locates the efficiency difference in the gap between ‘single-shot’ and ‘multi-shot’ versions of delimited control. To our knowledge, these results are the first of their kind for control operators.


title: PhD Abstracts

abstract: Although Abstracting Gradual Typing provides a systematic approach to design gradual languages, the original framework has limitations: first, it accepts design choices that lead to type inconsistencies sneaking through evaluation.Second, when a type inconsistency is identified at run time, evaluation halts without providing any feedback on the parts of the program related to the failure, a safe approach yet unhelpful for debugging.This dissertation addresses these two limitations of the Abstracting Gradual Typing framework.For the first limitation, I impose an extra constraint on the acceptable designs for gradual types: forward completeness of every type operation.This stricter constraint guarantees that, throughout evaluation, gradual types and runtime evidence objects cannot lose precision and will only represent information consistent with the original static type system.I introduce a new design for a gradual language with record subtyping that fulfills this restriction.For the second limitation, I provide a specification for runtime program slicing that can be systematically applied to languages designed using Abstracting Gradual Typing.Slicing can separate the portions of a program that are guaranteed to be uninvolved in a runtime failure.Unlike the standard blame approach, slicing does not assume that types are correct.The slicing semantics can be used to provide a debugging tool, and I apply empirical research methods to explore whether this runtime type slicing approach is useful to developers.


title: A simple blame calculus for explicit nulls

authors:
Ondrej Lhoták
Philip Wadler

abstract: Abstract Gradual typing provides a model for when a legacy language with less precise types interacts with a newer language with more precise types. Casts mediate between types of different precision, allocating blame when a value fails to conform to a type. The blame theorem asserts that blame always falls on the less-precisely typed side of a cast. One instance of interest is when a legacy language (such as Java) permits null values at every type, while a newer language (such as Scala or Kotlin) explicitly indicates which types permit null values. Nieto et al. in 2020 introduced a gradually typed calculus for just this purpose. The calculus requires three distinct constructors for function types and a non-standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (or vice versa) only when they are closed. Here, we define a simpler calculus that is more orthogonal, with one constructor for function types and one for possibly nullable types, and with an entirely standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (and vice versa) even if they are open. All results in the paper have been mechanized in Coq.


title: Sparcl: A language for partially invertible computation

authors:
Kazutaka Matsuda
Meng Wang

abstract: Abstract Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on partially invertible functions—functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible. We develop a language Sparcl for programming such functions in a natural way, where partial invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the “partially” part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the expressiveness of Sparcl with examples including tree rebuilding from preorder and inorder traversals, Huffman coding, arithmetic coding, and LZ77 compression.


title: Knuth-Morris-Pratt illustrated

abstract: Abstract The Knuth–Morris–Pratt (KMP) algorithm for string search is notoriously difficult to understand. Lost in a sea of index arithmetic, most explanations of KMP obscure its essence. This paper constructs KMP incrementally, using pictures to illustrate each step. The end result is easier to comprehend. Additionally, the derivation uses only elementary functional programming techniques.


title: Bottom-up computation using trees of sublists

abstract: Abstract Some top-down problem specifications, if executed, may compute sub-problems repeatedly. Instead, we may want a bottom-up algorithm that stores solutions of sub-problems in a table to be reused. How the table can be represented and efficiently maintained, however, can be tricky. We study a special case: computing a function ${\mathit{h}}$ taking lists as inputs such that ${\mathit{h}\;\mathit{xs}}$ is defined in terms of all immediate sublists of ${\mathit{xs}}$ . Richard Bird studied this problem in 2008 and presented a concise but cryptic algorithm without much explanation. We give this algorithm a proper derivation and discovered a key property that allows it to work. The algorithm builds trees that have certain shapes—the sizes along the left spine is a prefix of a diagonal in Pascal’s triangle. The crucial function we derive transforms one diagonal to the next.


title: Review of "Real World OCaml: Functional Programming for the Masses" Second Edition, by Yaron Minsky and Anil Madhavapeddy, 2023


title: Algebraic effects and handlers for arrows

abstract: Abstract We present an arrow calculus with operations and handlers and its operational and denotational semantics. The calculus is an extension of Lindley, Wadler and Yallop’s arrow calculus. The denotational semantics is given using a strong (pro)monad $\mathcal{A}$ in the bicategory of categories and profunctors. The construction of this strong monad $\mathcal{A}$ is not trivial because of a size problem. To build denotational semantics, we investigate what $\mathcal{A}$ -algebras are, and a handler is interpreted as an $\mathcal{A}$ -homomorphisms between $\mathcal{A}$ -algebras. The syntax and operational semantics are derived from the observations on $\mathcal{A}$ -algebras. We prove the soundness and adequacy theorem of the operational semantics for the denotational semantics.


title: Signature restriction for polymorphic algebraic effects

authors:
Taro Sekiyama
Takeshi Tsukada
Atsushi Igarashi

abstract: Abstract The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. In the literature, there are two kinds of approaches to this problem: one is to restrict how effects are triggered and the other is to restrict how they are implemented. This work explores a new approach to ensuring the safety of the use of polymorphic effects in polymorphic type assignment. A novelty of our work is to restrict effect interfaces . To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction , a new notion to restrict the type signatures of operations and show that signature restriction ensures type safety of a language equipped with polymorphic effects and unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both of the operations that satisfy and those that do not satisfy the signature restriction in a single program.


title: A review for the Journal of Functional Programming of Sandy Maguire, Algebra-Driven Design (Leanpub, 2020)

abstract: ContextCombinator libraries have been well studied in countless papers.Indeed, as Peyton Jones, Eber, and Seward wrote in 2000, At this point, any red-blooded functional programmer should start to foam at the mouth, yelling "build a combinator library."(Peyton Jones et al., 2000)


title: Static Blame for gradual typing

authors:
Chenghao Su
Lin Chen
Yanhui Li
Yuming Zhou

abstract: Abstract Gradual typing integrates static and dynamic typing by introducing a dynamic type and a consistency relation. A problem of gradual type systems is that dynamic types can easily hide erroneous data flows since consistency relations are not transitive. Therefore, a more rigorous static check is required to reveal these hidden data flows statically. However, in order to preserve the expressiveness of gradually typed languages, static checks for gradually typed languages cannot simply reject programs with potentially erroneous data flows. By contrast, a more reasonable request is to show how these data flows can affect the execution of the program. In this paper, we propose and formalize Static Blame , a framework that can reveal hidden data flows for gradually typed programs and establish the correspondence between static-time data flows and runtime behavior. With this correspondence, we build a classification of potential errors detected from hidden data flows and formally characterize the possible impact of potential errors in each category on program execution, without simply rejecting the whole program. We implemented Static Blame on Grift, an academic gradually typed language, and evaluated the effectiveness of Static Blame by mutation analysis to verify our theoretical results. Our findings revealed that Static Blame exhibits a notable level of precision and recall in detecting type-related bugs. Furthermore, we conducted a manual classification to elucidate the reasons behind instances of failure. We also evaluated the performance of Static Blame, showing a quadratic growth in run time as program size increases.


title: From high to low: Simulating nondeterminism and state with state

authors:
Wenhao Tang
Tom Schrijvers

abstract: Abstract Some effects are considered to be higher level than others. High-level effects provide expressive and succinct abstraction of programming concepts, while low-level effects allow more fine-grained control over program execution and resources. Yet, often it is desirable to write programs using the convenient abstraction offered by high-level effects, and meanwhile still benefit from the optimizations enabled by low-level effects. One solution is to translate high-level effects to low-level ones. This paper studies how algebraic effects and handlers allow us to simulate high-level effects in terms of low-level effects. In particular, we focus on the interaction between state and nondeterminism known as the local state, as provided by Prolog. We map this high-level semantics in successive steps onto a low-level composite state effect, similar to that managed by Prolog’s Warren Abstract Machine. We first give a translation from the high-level local-state semantics to the low-level global-state semantics, by explicitly restoring state updates on backtracking. Next, we eliminate nondeterminism altogether in favour of a lower-level state containing a choicepoint stack. Then we avoid copying the state by restricting ourselves to incremental, reversible state updates. We show how these updates can be stored on a trail stack with another state effect. We prove the correctness of all our steps using program calculation where the fusion laws of effect handlers play a central role.


title: Type-directed operational semantics for gradual typing

authors:
Wenjia Ye
Bruno C. d. S. Oliveira

abstract: Abstract The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In a TDOS, type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, type annotations are used to trigger type-based conversions on values. We illustrate how to employ a TDOS on gradually typed languages using two calculi. The first calculus, called $\lambda B^{g}$ , is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called $\lambda e$ , explores an eager semantics for gradually typed languages using a TDOS. For both calculi, type safety is proved. For the $\lambda B^{g}$ calculus, we also present a variant with blame labels and illustrate how the TDOS can also deal with such an important feature of gradually typed languages. We also show that the semantics of $\lambda B^{g}$ with blame labels is sound and complete with respect to the semantics of the blame calculus, and that both calculi come with a gradual guarantee . All the results have been formalized in the Coq theorem prover.


title: A practical formalization of monadic equational reasoning in dependent-type theory

authors:
Reynald Affeldt
Jacques Garrigue
Takafumi Saikawa

abstract: 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 maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes monadic equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws as interfaces like it is done when formalizing hierarchy of algebras in dependent-type theory. Thanks to this approach, we clearly separate equational laws from models. We can then take advantage of the sophisticated rewriting capabilities of Coq and build libraries of lemmas to achieve concise proofs of programs. We can also use the resulting framework to leverage on Coq’s mathematical theories and formalize models of monads. In this article, we explain how we formalize a rich hierarchy of effects (nondeterminism, state, probability, etc.), how we mechanize examples of monadic equational reasoning from the literature, and how we apply our framework to the design of equational laws for a subset of ML with references.


title: OCaml Blockly

abstract: 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 OCaml Blockly, its OCaml counterpart compiles: it is free from syntax errors, scoping errors, and type errors. OCaml Blockly supports introductory constructs of OCaml that are sufficient to write the shortest path problem for the Tokyo metro network. This paper describes the design of OCaml Blockly and how it is used in a CS-major course on functional programming.


title: Domain-specific tensor languages

authors:
Jean-Philippe Bernardy
Patrik Jansson

abstract: 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 either 1. array-oriented languages that do not enforce or take advantage of tensor properties and algebraic structure or 2. follow the categorical structure of tensors but require the programmer to manipulate tensors in an unwieldy point-free notation. A deeper issue is that for tensor calculus, the dominant pedagogical paradigm assumes an audience which is either comfortable with notational liberties which programmers cannot afford, or focus on the applied mathematics of tensors, largely leaving their linguistic aspects (behaviour of variable binding, syntax and semantics, etc.) for the reader to figure out by themselves. This state of affairs is hardly surprising, because, as we highlight, several properties of standard tensor notation are somewhat exotic from the perspective of lambda calculi. We bridge the gap by defining a dsl , embedded in Haskell, whose syntax closely captures the index notation for tensors in wide use in the literature. The semantics of this edsl is defined in terms of the algebraic structures which define tensors in their full generality. This way, we believe that our edsl can be used both as a tool for scientific computing, but also as a vehicle to express and present the theory and applications of tensors.


title: Call-by-value and call-by-name: A simple proof of a classic theorem

authors:
Dariusz Biernacki
James McKinna
Filip Sieczkowski

abstract: 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 form can always be simulated by a call-by-name evaluation. While the statement and intuition behind it are simple and clear, naive attempts at proof famously fail: the result is usually established as a consequence of the more complex standardisation theorem. In this work, we develop and formalise a novel and lightweight inductive approach to tackle the problem of simulation between two semantics for a single calculus, but with different evaluation orders. We exercise our method on the classic call-by-value and call-by-name example and report on methodological takeaways suggested by our approach, in particular what effect the flavour of semantics chosen has on the proof.


title: Experiences of early assessment to teach functional programming

abstract: 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 assessment instrument, in which students had to use code given to them, or slightly modify it, to achieve certain goals. The intended outcome was that the students would thus engage earlier with the functional language, enabling them to be better prepared for the second piece of assessment, where they create code to solve given problems. This intervention showed promise: the difference between a student’s score on the Create assignment improved by an average of 9% in the year after the intervention was implemented, a small effect.


title: Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq

authors:
Nicolas Chappe
Paul He
Ludovic Henrio
Eleftherios Ioannidis
Yannick Zakowski
Steve Zdancewic

abstract: 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 with three kinds of nodes: external events, internal steps, and delayed branching. This structure allows us to provide shallow embedding of denotational models with nondeterministic choice in the style of ccs , while recovering an inductive LTS view of the computation. CTrees leverage a vast collection of bisimulation and refinement tools well-studied on LTSs, with respect to which we establish a rich equational theory. We connect CTrees to the ITrees infrastructure by showing how a monad morphism embedding the former into the latter permits using CTrees to implement nondeterministic effects. We demonstrate the utility of CTrees by using them to model concurrency semantics in two case studies: ccs and cooperative multithreading.


title: Inductive synthesis of structurally recursive functional programs from non-recursive expressions

authors:
Hangyeol Cho
Woosuk Lee

abstract: 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 address this challenge by using a new technique we call block-based pruning. A block refers to a recursion- and conditional-free expression (i.e., straight-line code) that yields an output from a particular input. We first synthesize as many blocks as possible for each input–output example, and then we explore the space of recursive programs, pruning candidates that are inconsistent with the blocks. Our method is based on an efficient version space learning, thereby effectively dealing with a possibly enormous number of blocks. In addition, we present a method that uses sampled input–output behaviors of library functions to enable a goal-directed search for a recursive program using the library. We have implemented our approach in a system called Trio and evaluated it on synthesis tasks from prior work and on new tasks. Our experiments show that Trio significantly outperforms prior work.


title: Binary search - think positive

authors:
Alexander Dinges
Ralf Hinze

abstract: The setting is a tutorial on program verification in Agda. Please consult the programme for further details. [ See also Appendix A .]


title: A contextual formalization of structural coinduction

authors:
Paul Downen
Zena M. Ariola

abstract: 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 corecursive programs only in terms of the logical structure of their context. We illustrate this technique as an informal method of proofs which closely match the style of informal inductive proofs, where it is straightforward to check that all cases are covered and the coinductive hypotheses are used correctly. This intuitive idea is then formalized through a syntactic theory for deriving program equalities, which is justified purely in terms of the computational behavior of abstract machines and proved sound with respect to observational equivalence.


title: Turner, Bird, Eratosthenes: An eternal burning thread

abstract: 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 evaluation and of list comprehensions. As an illustration of these techniques, he popularized a one-line recursive “sieve” to generate the infinite list of prime numbers. Turner called this algorithm The Sieve of Eratosthenes. In a lovely paper called “The Genuine Sieve of Eratosthenes”, Melissa O’Neill argued that Turner’s program is not in fact a faithful implementation of the algorithm, and gave a detailed presentation using priority queues of the real thing. She included a variation by Richard Bird, which uses only lists but makes clever use of circular programming. Bird describes his circular program again in his textbook “Thinking Functionally with Haskell”, and sets its proof of correctness as an exercise. In particular, why is this circular program productive? Unfortunately, Bird’s hint for a solution is incorrect. So what should a proof look like? One of the last projects Turner worked on was the notion of “Total Functional Programming”. He observed that most programs are already structurally recursive or corecursive, therefore guaranteed respectively terminating or productive; he conjectured that “with more practice we will find this is always true”. We explore Bird’s circular Sieve of Eratosthenes as a challenge problem for Turner’s Total Functional Programming.


title: The graphical theory of monads

authors:
Ralf Hinze
Dan Marsden

abstract: 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 theory. Unfortunately, these results can be hard to reason about as they involve more abstract machinery. In this paper, we present the formal theory of monads in terms of string diagrams — a graphical language for 2-categorical calculations. Using this perspective, we show that many aspects of the theory of monads, such as the Eilenberg–Moore and Kleisli resolutions of monads, liftings, and distributive laws, can be understood in terms of systematic graphical calculational reasoning. This paper will serve as an introduction both to the formal theory of monads and to the use of string diagrams, in particular, their application to calculations in monad theory.


title: PhD Abstracts


title: PhD Abstracts

abstract: 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 interactive theorem prover and dependent type programming language Agda and prove the correctness of smart contracts in it.In the context of Bitcoin, our verification of Bitcoin scripts consists of non-conditional and conditional scripts.For Solidity, we refer to programs using object-oriented features of Solidity, such as calling of other contracts, full recursion, and the use of gas in order to guarantee termination while having a Turingcomplete language.We have developed a simulator for Solidity-style smart contracts.As a main example, we executed a reentrancy attack in our model.We have verified smart contracts in Bitcoin and Solidity using weakest precondition in Agda.Furthermore, Agda, combined with the fact that it is a theorem prover and programming language, allows the writing of verified programs, where the verification takes place in the same language in which the program is written, avoiding the problem of translation from one language to another (with possible translation mistakes).


title: JFP special issue on program calculation

authors:
Graham Hutton
Nicolas Wu


title: Checking equivalence in a non-strict language

authors:
John Charles Kolesar
Ruzica Piskac
William T. Hallahan

abstract: 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. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation, nebula , proves equivalences of programs written in Haskell. We demonstrate nebula ’s practical effectiveness at both proving equivalence and producing counterexamples automatically by applying nebula to existing benchmark properties.


title: Semantics of pattern unification

authors:
Ambroise Lafont
Neel Krishnaswami

abstract: 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 unification algorithm applies. To illustrate our semantic analysis, we implemented our generic unification algorithm in Agda. The syntax with metavariables given as input of the algorithm is specified by a notion of signature generalising binding signatures, covering a wide range of examples, including ordered $\lambda$ -calculus and (intrinsic) polymorphic syntax such as System F. Although we do not explicitly handle equations, we also tackle simply typed $\lambda$ -calculus modulo $\beta$ - and $\eta$ -equations (Miller’s original setting) by working on the syntax of normal forms.


title: Tail recursion modulo context: An equational approach (extended version)

authors:
Daan Leijen
Anton Lorenzen

abstract: 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 general TRMC algorithm from its specification. We can instantiate our general algorithm by providing an implementation of application and composition on abstract contexts and showing that our context laws hold. We provide some known instantiations of TRMC, namely modulo evaluation contexts (CPS), and associative operations , and further instantiations not so commonly associated with TRMC, such as defunctionalized evaluation contexts, monoids , semirings , exponents , and fields . We study the modulo cons instantiation in particular and prove that an instantiation using Minamide’s hole calculus is sound. We also calculate a second instantiation in terms of the Perceus heap semantics to precisely reason about the soundness of in-place update. While all previous approaches to TRMc fail in the presence of nonlinear control (e.g., induced by call/cc, shift/reset, or algebraic effect handlers), we can elegantly extend the heap semantics to a hybrid approach which dynamically adapts to nonlinear control flow. We have a full implementation of hybrid TRMc in the Koka language, and our benchmark shows the TRMc transformed functions are always as fast or faster than using manual alternatives.


title: Point-free calculational proofs and program derivation in linear algebra using a graphical syntax

authors:
Júlia Mota
João A. R. Paixão
Lucas Rufino Martelotte

abstract: 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 spaces and more generally linear relations. Linear algebra is usually seen as the study of vector spaces and linear transformations. However, to reason effectively with subspaces in a point-free and calculational manner, both can be generalized to an unifying concept: linear relations, much like relational algebra. While the semantics is relational, the syntax is graphical and uses string diagrams, 2-dimensional formal diagrams, which represent the linear relations. Most importantly, in a number of cases, the relational semantics allows algorithms and properties to be derived calculationally instead of just verified. Our approach is to proceed primarily by examples which involve finding inverses, switching from an implicit basis to an explicit basis (solving a homogeneous linear system), exploring both the exchange lemma and the Zassenhaus’ algorithm.


title: How much is in a square? Calculating functional programs with squares

abstract: Abstract Experience in teaching functional programming (FP) on a relational basis has led the author to focus on a graphical style of expression and reasoning in which a geometric construct shines: the (semi) commutative square. In the classroom this is termed the “magic square” (MS), since virtually everything that we do in logic, FP, database modeling, formal semantics and so on fits in some MS geometry. The sides of each magic square are binary relations and the square itself is a comparison of two paths, each involving two sides. MSs compose and have a number of useful properties. Among several examples given in the paper ranging over different application domains, free-theorem MSs are shown to be particularly elegant and productive. Helped by a little bit of Galois connections, a generic, induction-free theory for ${\mathsf{foldr}}$ and $\mathsf{foldl}$ is given, showing in particular that ${\mathsf{foldl} \, {{s}}{}\mathrel{=}\mathsf{foldr}{({flip} \unicode{x005F}{s})}{}}$ holds under conditions milder than usually advocated.


title: Hefty algebras: Modular elaboration of higher-order effects

authors:
Cas van der Rest
Casper Bach

abstract: Abstract 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.


title: Parallel dual-numbers reverse AD

authors:
Tom Smeding
Matthijs Vákár

abstract: Abstract Where dual-numbers forward-mode automatic differentiation (AD) pairs each scalar value with its tangent value, dual-numbers reverse-mode AD attempts to achieve reverse AD using a similarly simple idea: by pairing each scalar value with a backpropagator function. Its correctness and efficiency on higher-order input languages have been analysed by Brunel, Mazza and Pagani, but this analysis used a custom operational semantics for which it is unclear whether it can be implemented efficiently. We take inspiration from their use of linear factoring to optimise dual-numbers reverse-mode AD to an algorithm that has the correct complexity and enjoys an efficient implementation in a standard functional language with support for mutable arrays, such as Haskell. Aside from the linear factoring ingredient, our optimisation steps consist of well-known ideas from the functional programming community. We demonstrate the use of our technique by providing a practical implementation that differentiates most of Haskell98. Where previous work on dual numbers reverse AD has required sequentialisation to construct the reverse pass, we demonstrate that we can apply our technique to task-parallel source programs and generate a task-parallel derivative computation.


title: Towards type-directed compiler calculation

abstract: Abstract This paper explores a principled approach to calculating abstract machines and associated compilers, starting from an intrinsically typed interpreter. After deriving a compiler for a simple expression language in some detail, the first steps of this calculation are repeated to derive an optimizing evaluator for the simply typed lambda calculus.


title: Automatically testing console I/O behavior of student submissions in Haskell

authors:
Oliver Westphal
Janis Voigtländer

abstract: Abstract Good test-suites are an important tool to check the correctness of programs. They are also essential in unsupervised educational settings, like automatic grading or for students to check their solution to some programming task by themselves. For most Haskell programming tasks, one can easily provide high-quality test-suites using standard tools like QuickCheck. Unfortunately, this is no longer the case once we leave the purely functional world and enter the lands of console I/O. Nonetheless, understanding console I/O is an important part of learning Haskell, and we would like to provide students the same support as with other subject matters. The difficulty in testing console I/O programs arises from the standard tools’ lack of support for specifying intended console interactions as simple declarative properties. These interactions are however essential in order to determine whether a program behaves as desired. We describe the console interactions of a program by tracing its text input and output actions. In order to describe which traces match the intended behavior of the program under test, we present a formal specification language. The language is designed to capture interactive behavior found in commonly used textbook exercises and examples, or as much of it as possible, as well as in our own teaching, while at the same time retaining simplicity and clarity of specifications. We intentionally restrict the language, ensuring that expressed behavior is truly interactive and not simply a pure string-builder function in disguise. Based on this specification language, we build a testing framework that allows testing against specifications in an automated way. A central feature of the testing procedure is the use of a constraint solver in order to find meaningful input sequences for the program under test.


title: You could have invented Fenwick trees

abstract: Abstract Fenwick trees , also known as binary indexed trees are a clever solution to the problem of maintaining a sequence of values while allowing both updates and range queries in sublinear time. Their implementation is concise and efficient—but also somewhat baffling, consisting largely of nonobvious bitwise operations on indices. We begin with segment trees , a much more straightforward, easy-to-verify, purely functional solution to the problem, and use equational reasoning to explain the implementation of Fenwick trees as an optimized variant, making use of a Haskell EDSL for operations on infinite two’s complement binary numbers.


title: Review of "Haskell in Depth" by Vitaly Bragilevsky, Manning Publications, 2021

abstract: Review of "Haskell in Depth" by


title: Recursive subtyping for all

authors:
Litao Zhou
Yaoda Zhou
Qianyong Wan
Bruno C. d. S. Oliveira

abstract: Abstract Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala, or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification, and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability , transitivity of subtyping, conservativity , and a sound and complete algorithmic formulation, has been a long-time challenge. This paper shows how to extend $F_{\le}$ with iso-recursive types in a new calculus called $F_{\le}^{\mu}$ . $F_{\le}$ is a well-known polymorphic calculus with bounded quantification. In $F_{\le}^{\mu}$ , we add iso-recursive types and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. In addition, we use so-called structural folding/unfolding rules for typing iso-recursive expressions, inspired by the structural unfolding rule proposed by Abadi et al . (1996). The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity; the conservativity of $F_{\le}^{\mu}$ over $F_{\le}$ ; and a sound and complete algorithmic formulation of $F_{\le}^{\mu}$ . We study two variants of $F_{\le}^{\mu}$ . The first one uses an extension of the $\textrm{kernel}~F_{\le}$ (a well-known decidable variant of $F_{\le}$ ). This extension accepts equivalent rather than equal bounds and is shown to preserve decidable subtyping. The second variant employs the $\textrm{full}~F_{\le}$ rule for bounded quantification and has undecidable subtyping. Moreover, we also study an extension of the kernel version of $F_{\le}^{\mu}$ , called $F_{\le\ge}^{\mu\wedge}$ , with a form of intersection types and lower bounded quantification . All the properties from the kernel version of $F_{\le}^{\mu}$ are preserved in $F_{\le\ge}^{\mu\wedge}$ . All the results in this paper have been formalized in the Coq theorem prover.


title: Multi types and reasonable space

authors:
Beniamino Accattoli
Ugo Dal Lago
Gabriele Vanoni

abstract: Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system.


title: Mixing visual and textual code

authors:
Leif Andersen
Michael Ballantyne
Cameron Moy
Matthias Felleisen
Stephen Chang

abstract: The dominant programming languages support nothing but linear text to express domain-specific geometric ideas. What is needed are hybrid languages that allow developers to create visual syntactic constructs so that they can express their ideas with a mix of textual and visual syntax tailored to an application domain. This mix must put the two kinds of syntax on equal footing and, just as importantly, the extended language must not disrupt a programmer's typical workflow. This means that any new visual syntax should be a proper language extension that is composable with other language features. Furthermore, the extensions should also preserve static reasoning about the program. This paper presents Hybrid ClojureScript the first such hybrid programming language. Hybrid ClojureScript allows programmers to add visual interactive syntax and to embed instances of this syntax within a program's text. An enhanced hybrid IDE can then display these embedded instances as mini-GUIs that programmers interact with, while other IDEs will show a textual representation of the syntax. The paper argues the necessity of such an extensibility mechanism, demonstrates the adoptability of the design, and discusses what might be needed to use the design in other languages. to be published in JFP


title: Don't exhaust, don't waste: Resource-aware soundness for big-step semantics

authors:
Riccardo Bianchini
Francesco Dagnino
Paola Giannini
Elena Zucca

abstract: We extend the semantics and type system of a lambda calculus equipped with common constructs to be "resource-aware". That is, the semantics keeps track of the usage of resources, and is stuck, besides in case of type errors, if either a needed resource is exhausted, or a provided resource would be wasted. In such way, the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no resource gets either exhausted or wasted. The extension is parametric on an arbitrary "grade algebra", modeling an assortment of possible usages, and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning. Preprint submitted to JFP (Journal of Functional Programming)


title: A simple and efficient implementation of strong call by need by an abstract machine

authors:
Malgorzata Biernacka
Witold Charatonik
Tomasz Drab

abstract: Strong call-by-need combines full normalization with the sharing discipline of lazy evaluation, yet no prior implementation achieved both simplicity and efficiency. We introduce RKNL, an abstract machine that realizes strong call-by-need with bilinear overhead. The machine has been derived automatically from a higher-order evaluator that uses the technique of memothunks to implement laziness. By employing an off-the-shelf transformation tool implementing the ``functional correspondence'' between higher-order interpreters and abstract machines, we obtained a simple and concise description of the machine. We prove that the resulting machine conservatively extends the lazy version of Krivine machine for the weak call-by-need strategy, and that it simulates the normal-order strategy in a bilinear number of steps, i.e., linear in both the number of beta-reductions and the size of the input term.


title: Types, equations, dimensions and the Pi theorem

authors:
Nicola Botta
Patrik Jansson

abstract: The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to formalize basic notions of dimensional analysis: those of dimension function, physical quantity, homomorphic measurement, the covariance principle and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.


title: Adapting the MVVM pattern to C++ frontends and Agda-based backends

abstract: Using agda2hs and ad-hoc Haskell FFI bindings, writing Qt applications in C++ with Agda- or Haskell-based backends (possibly including correctness proofs) is already possible. However, there was no repeatable methodology to do so, nor to use arbitrary Haskell built-in libraries in Agda code. We present a well-documented, general methodology to address this, applying the ideas of the Model-View-ViewModel architecture to models implemented in functional languages. This is augmented by a software development kit providing easy installation and automated compilation. For obstacles arising, we provide solutions and ideas that are novel contributions by themselves. We describe and compare solutions for using arbitrary Haskell built-ins in Agda code, highlighting their advantages and disadvantages. Also, for user interruption, we present a new Haskell future design that, to the best of our knowledge, is the first to provide for arbitrary interruption and the first to provide for interruption via direct FFI calls from C and C++. Finally, we prove with benchmarks that the agda2hs compiler at the base of our methodology is viable when compared to other solutions, specifically to the OCaml extraction feature of Rocq and the default MAlonzo backend of Agda.


title: Longest r-chain: thinning by grouping

authors:
Alexander Dinges
Ralf Hinze

abstract: r ⊆ s⇒ length (longest-chain r xs) ⩽ length (longest-chain s xs).If we set the distance to, say, 13, then the poem is almost completely uncovered.> longest-chain (close 13) .unlines .take 2 .lines .


title: Proto-Quipper with dynamic lifting

authors:
Peng Fu
Kohei Kishida
Neil J. Ross
Peter Selinger

abstract: Quipper is a functional language for programming quantum circuits. Proto-Quipper is a family of languages aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a construct called dynamic lifting, which is present in Quipper. By virtue of being a circuit description language, Proto-Quipper has two separate runtimes: circuit generation time and circuit execution time. Values that are known at circuit generation time are called parameters, and values that are known at circuit execution time are called states. Dynamic lifting is an operation that enables a state, such as the result of a measurement, to be lifted to a parameter, where it can influence the generation of the next portion of the circuit. As a result, dynamic lifting enables Proto-Quipper programs to interleave classical and quantum computation. We describe the syntax of a language we call Proto-Quipper-Dyn. Its type system uses a system of modalities to keep track of the use of dynamic lifting. We then provide an operational semantics, as well as a notion of categorical model for dynamic lifting. We also construct a concrete instance of such a model based on biset-enrichment. We prove that both the type system and the operational semantics are sound with respect to our categorical semantics. Finally, we give some examples of Proto-Quipper-Dyn programs that make essential use of dynamic lifting.


title: Higher-order bialgebraic semantics

authors:
Sergey Goncharov
Stefan Milius
Lutz Schröder
Stelios Tsampas
Henning Urbat

abstract: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term (pointed) higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the lambda-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. Extended and updated version of arXiv:2210.13387


title: Etna: An evaluation platform for property-based testing

authors:
Alperen Keles
Jessica Shi
Nikhil Kamath
Tin Nam Liu
Ceren Mert
Harrison Goldstein
Benjamin C. Pierce
Leonidas Lampropoulos

abstract: Property-based testing is a mainstay of functional programming, boasting a rich literature, an enthusiastic user community, and an abundance of tools~ -- so many, indeed, that new users may have difficulty choosing. Moreover, any given framework may support a variety of strategies for generating test inputs; even experienced users may wonder which are better in any given situation. Sadly, the PBT literature, though long on creativity, is short on rigorous comparisons to help answer such questions. We present ETNA, a platform for empirical evaluation and comparison of PBT techniques. ETNA incorporates a number of popular PBT frameworks and testing workloads from the literature, and its extensible architecture makes adding new ones easy, while handling the technical drudgery of performance measurement. To illustrate its benefits, we use ETNA to carry out several experiments with popular PBT approaches in Rocq, Haskell, OCaml, Racket, and Rust, allowing users to more clearly understand best practices and tradeoffs.


title: Modular models of monoids with operations by lifting functors along fibrations

authors:
Zhixuan Yang
Nicolas Wu

abstract: Inspired by Plotkin and Power's algebraic treatment of computational effects and the principle of notions of computations as monoids, we propose a categorical framework for equational theories and models of monoids equipped with operations. This framework generalises Plotkin and Power's algebraic treatment of effectful operations taking or returning values as input or output to operations that may take or return computations as input or output. Additionally, to give semantic models of computational effects in a modular way, we introduce a formal theory of modular constructions of algebraic structures based on the framework of lifting functors along fibrations.


title: Polymorphic coverage types

authors:
Zhe Zhou
Ashish Mishra
Benjamin Delaware
Suresh Jagannathan

abstract: Test input generators are an important part of property-based testing (PBT) frameworks.Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by these generators can be complex data structures, constrained to satisfy properties the developer believes are most relevant to testing the function of interest.An important feature expected of these generators is that they be capable of producing all acceptable elements that satisfy the function's input type and generator-provided constraints.However, it is not readily apparent how we might validate whether a particular generator's output satisfies this coverage requirement.Typically, developers must rely on manual inspection and post-mortem analysis of test runs to determine if the generator is providing sufficient coverage; these approaches are error-prone and difficult to scale as generators become more complex.To address this important concern, we present a new refinement type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds "must-style" underapproximate reasoning principles as a fundamental part of the type system.The types associated with expressions now capture the set of values guaranteed to be produced by the expression, rather than the typical formulation that uses types to represent the set of values an expression may produce.We have formalized the notion of coverage types in a rich core language that supports higher-order functions and inductive datatypes.To better support checking coverage properties of real-world test generators, we extend this type system with type and qualifier polymorphism.These extensions enable our system to statically verify coverage guarantees of test input generators constructed using the sort of monadic combinators found in most PBT frameworks.We have implemented a coverage type checker for OCaml programs based on this core calculus, and present a detailed evaluation of the utility of our ideas using a corpus of benchmarks drawn from both the PBT literature and open-source projects.


venue: onward

title: On the language metaphor

abstract: There are many more similarities than distinctions between natural languages and the languages used in computer science. The term "language" has been used liberally as a metaphor in the discipline in terms of language creation, evolution and concept of elegance. Examples are presented to show that the language metaphor serves the discipline well.


title: The accessibility toolkit

authors:
Halimat I. Alabi
Bruce Gooch

abstract: We propose the creation of a repository of inclusive mobile application design tools and techniques. The repository will be based on existing and future research in the realm of accessibility and initially only available to academic researchers developing user studies. These developers may browse tool features based on operating system, ease of implementation, modality and range of user ability within each particular modality. To educate developers, the toolkit will utilize user personas for each modality that exemplify how users might use the features in the repository.


title: Evaluation and usability of programming languages and tools: (PLATEAU)

authors:
Craig Anslow
Shane Markstrum
Emerson R. Murphy-Hill

abstract: Programming languages exist to enable programmers to develop software effectively. But how efficiently programmers can write software depends on the usability of the languages and tools that they develop with. The aim of this workshop is to discuss methods, metrics and techniques for evaluating the usability of languages and language tools. The supposed benefits of such languages and tools cover a large space, including making programs easier to read, write, and maintain; allowing programmers to write more flexible and powerful programs; and restricting programs to make them more safe and secure. We plan to gather the intersection of researchers in the programming language, programming tool, and human-computer interaction communities to share their research and discuss the future of evaluation and usability of programming languages and tools. We are also interested in the input of other members of the programming research community working on related areas, such as refactoring, design patterns, program analysis, program comprehension, software visualization, end-user programming, and other programming language paradigms.


title: Example embedding

abstract: Using code examples in professional software development is like teenage sex. Those who say they do it all the time are probably lying. Although it is natural, those who do it feel guilty. Finally, once they start doing it, they are often not too concerned with safety, they discover that it is going to take a while to get really good at it, and they realize they will have to come up with a bunch of new ways of doing it before they really figure it all out.


title: Automated program verification made SYMPLAR: symbolic permissions for lightweight automated reasoning

abstract: Research in automated program verification against specifications written in first-order logic has come a long way. Ever-faster Satisfiability Modulo Theories (SMT) solvers [Barrett et al. 2010] promise to verify program instructions quickly against specifications. Unfortunately, aliasing still prevents automated program verification tools from easily and soundly verifying interesting programs. This paper introduces the use of symbolic permissions as the basis for sound automated program verification. Symbolic permissions provide a simple alias control mechanism with expressiveness similar to the well-known fractional permissions [Boyland 2003]. The paper shows that symbolic permissions can be enforced with a linear refinement typechecking procedure. Once permissions are checked, aliasing can essentially be ignored for the purposes of program verification, which allows taking full advantage of SMT solvers for doing the heavy verification lifting. The paper shows that a verification tool based on symbolic permissions can easily verify a design pattern with inherent aliasing challenges.


title: Ageing society

authors:
Roberto Bisiani
Davide Merico

abstract: This is a brief film describing the functionality and the inner behaviour of a system called Contexta-Care, a monitoring facility for independent-living elders. The first challenge for such a film is to give in a few minutes a fair idea of what the system can do in a real case. The target audience is first of all the geriatric health-care professionals but the system should be almost completely understandable by any person. The second challenge is that most of the "action" happens over many hours, days or even weeks and just showing the "real time" behaviour is not enough.


title: 2nd workshop on free composition (FREECO)

authors:
Christoph Bockisch
Lodewijk Bergmans
Dean Wampler

abstract: No abstract available.


title: Presenting a day in the life of video-based requirements engineering

authors:
Naoufel Boulila
Oliver Creighton
Georgi A. Markov
Steve Russell
Ronald Blechner

abstract: In today's global economy, innovation through technology is a key driver for a sustainable economic growth and competitiveness. Siemens as a global player possesses a tremendous portfolio of innovative technologies. In an effort to highlight some of these technologies, Siemens has organized an Internet-based event for selected industrial partners. The event comprised a virtual world showcasing five technological innovation areas, including video-based requirements engineering (VBRE). Attendees were connected to the virtual tradeshow and could visit manned booths, choose which technology presentation to attend, and even follow a guided tour.


title: Evolution of Mobile Software Development from Platform-Specific to Web-Based Multiplatform Paradigm

authors:
Luis Corral
Alberto Sillitti
Giancarlo Succi
Alessandro Garibbo
Paolo Ramella


title: The artist in the computer scientist: more humanity to our research

authors:
Daniel Cukier
Joseph W. Yoder

abstract: Art and Science are usually seen as quite distinct tasks and not supportive of each other or similar at all. Isn't art all about creativity and abstract beauty, while computer sci-ence is about logic, truths and problem solving? Can these two practices really be related in any way? Our primary objective is to show the benefits of arts to software development. First we reflect on the concept of how Art and Science are similar. Then we report our thoughts about the relation of different types of art to Computer Science such as theater, music, painting, and poetry.


title: The serious game: wemakewords

authors:
Ruth Barbara Demmel
Barbara Köhler
Stephan Krusche
Ludwig Schubert

abstract: We suggest digital serious games as a means to create individualized learning environments that train social skills in parallel to the content. In cooperation with a child psychology practice we developed the collaborative and adaptive serious game weMakeWords as a prove of concept. The game teaches children how to read in a fun and approachable way, while adjusting itself to the chidren's need. In first preliminary evaluations the concept has been highly successful concerning the leaning outcome as well as in fostering collaboration between children.


title: What makes a programming language popular?: an essay from a historical perspective

abstract: Among the thousands of programming languages available, some languages become extremely popular, while others, thought to be superior in many ways, languish. This essay explores this situation from a historical perspective.


title: Naturalistic types

authors:
Roman Knöll
Vaidas Gasiunas
Mira Mezini

abstract: The typical properties of natural language - redundancy avoidance, locality, and immediacy - support high semantic density and improve readability, and therefore, are also interesting for the design of programming languages. To achieve these properties, natural language heavily relies on types, which are used for referencing, generalization, and description of instances. With naturalistic types we conceptualize the idea of natural language types for use in programming. This article demonstrates possible applications of naturalistic types for programming and gives a detailed analysis of their constituents - concepts, properties, quantities, and conditions.


title: Mind your language: on novices' interactions with error messages

authors:
Guillaume Marceau
Kathi Fisler
Shriram Krishnamurthi

abstract: Error messages are one of the most important tools that a language offers its programmers. For novices, this feed-back is especially critical. Error messages typically contain both a textual description of the problem and an indication of where in the code the error occurred. This paper reports on a series of studies that explore beginning students' inter-actions with the vocabulary and source-expression high-lighting in DrRacket. Our findings demonstrate that the error message significantly fail to convey information accurately to students, while also suggesting alternative designs that might address these problems.


title: Coding at the speed of touch

abstract: Although programming is one of the most creative things that one can do with a computer, there is currently no way to make programs on an increasingly popular class of tablet computers. Tablets appear unable to support capable (proficient) programming experiences because of their small form factor and touch-centric input method. This paper demonstrates how co-design of a programming language, YinYang, and its environment can overcome these challenges to enable do-it-yourself game creation on tablets. YinYang's programming model is based on tile and behavior constructs that simplify program structure for effective display and input on tablets, and also supports the definition and safe reuse of new abstractions to be competitive with capable programming languages. This paper details YinYang's design and evaluates our initial experience through a prototype that runs on current tablet hardware.


title: Emerson: accessible scripting for applications in an extensible virtual world

authors:
Behram F. T. Mistree
Bhupesh Chandra
Ewen Cheslack-Postava
Philip Alexander Levis
David Gay

abstract: This paper presents Emerson, a new programming system for scripting objects in user-extensible virtual worlds such as Second Life, Active Worlds, and Open Wonderland. Emerson's primary goal is to make it easy for novice programmers to write and deploy interesting applications. Scripting applications for these worlds is difficult due to two characteristics: the worlds must scale to millions of users and are therefore distributed, and there is no central authority or design so interaction is mostly between mutually untrusting applications.


title: Language support for asynchronous event handling in the invocation call stack

authors:
Carlos Rafael Gimenes das Neves
Eduardo Martins Guerra
Clovis Torres Fernandes

abstract: There are times during the normal execution flow of programs, when an object of a class wishes to be notified about some special event which may take place in a method it calls. Some other times, this event might not happen in the directly called method, but in another one, deeper in the call stack, beyond the knowledge of the caller class. To overcome this, a common solution is to create structures close to the Observer design pattern, which ends up coupling the caller class with the called class and lacks asyn-chronous behavior. In order not to couple the classes, exception handling can be used, as long as the premature termination of the called method is not a concern. The present essay proposes a solution to fill this gap and describes the initial concept of a technique to asynchronously handle events triggered inside any method within the current call stack, without coupling classes.


abstract: Programming language design, The Four Rs, Domainspecific languages "I can learn the poor things reading, writing, and 'rithmetic, and counting as far as the rule of three, which is just as much as the likes of them require;" Lawrie Todd: Or the Settlers in the Woods, Galt (1832) [4]. ˜˜˜Many will be familiar with the old adage that at the core of any child's education should be the three Rs: reading, writing, and 'rithmetic.The phrase, which appeared first in print in 1825 [12] has been appropriated and parodied at length ("read, reason, recite", "reduce, reuse, recycle", etc.).Each permutation has the same purpose: to express succinctly the core tenets of an approach or philosophy.The four Rs of programming language design is another such parody of this old phrase, providing a rubric, or framework, for the design and evaluation of effective programming languages and language features.Since the very first programming language back in the 1940s [14] thousands of programming languages have been developed, representing a broad spectrum of paradigms, perspectives, and philosophies.And yet, there is no single language which is "all things to all people".The four Rs were born out of trying to answer a number of questions about the nature of programming languages and programming language design: what makes a programming language effective or ineffective?What should be the core aims of a language designer?How should programming languages and features be compared?Why is there no single "perfect" language?The four Rs go someway towards answering these questions.Before I reveal the four Rs, let's first consider some more foundational questions:Why programming languages?The development of programming languages has greatly aided software engineering.As hardware and software have grown increasingly complex, programming This is a minor revision of the published paper.Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page.To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.


title: The intuitive control of smart home and office environments

authors:
Sebastian Peters
Vivian Loftness
Volker Hartkopf

abstract: Along with the associated film, this paper presents an approach to individually controlling home and office fixtures such as lights, window blinds, cooling and ventilation units with an 'intuitive gesture-based controller' using a smart phone. The implementation of the gesture controls is based on the magnetometer, gyroscope and accelerometer built into the most recent smart phones. The user simply points to target objects and completes specific gestures. For example, pointing to the top of a window and completing a "down"-gesture is interpreted as a command to lower the blinds at the window. Pointing the device to a light fixture and doing an "up"-gesture raises the light levels. In combination with addressable fixtures and wireless infrastructures, this phone controller reveals how a wide variety of fixtures in a building can be intuitively controlled by pointing, using only a single button and gesturing.


title: Automatic performance programming

abstract: It has become extraordinarily difficult to write software that performs close to optimally on complex modern microarchitectures. Particularly plagued are domains that are data intensive and require complex mathematical computations such as information retrieval, scientific simulations, graphics, communication, control, and multimedia processing. In these domains, performance-critical components are usually written in C (with possible extensions) and often even in assembly, carefully "tuned" to the platform's architecture and microarchitecture. Specifically, the tuning includes optimization for the memory hierarchy and for different forms of parallelism. The result is usually long, rather unreadable code that needs to be re-written or re-tuned with every platform upgrade. On the other hand, the performance penalty for relying on straightforward, non-tuned, more elegant implementations is typically a factor of 10, 100, or even more. The reasons for this large gap are some (likely) inherent limitations of compilers including the lack of domain knowledge, and the lack of an efficient mechanism to explore the usually large set of transformation choices. The recent end of CPU frequency scaling, and thus the end of free software speed-up, and the advent of mainstream parallelism with its increasing diversity of platforms further aggravate the problem.


title: The tradeoffs of societal computing

authors:
Swapneel Sheth
Gail E. Kaiser

abstract: As Social Computing has increasingly captivated the general public, it has become a popular research area for computer scientists. Social Computing research focuses on online social behavior and using artifacts derived from it for providing recommendations and other useful community knowledge. Unfortunately, some of that behavior and knowledge incur societal costs, particularly with regards to Privacy, which is viewed quite differently by different populations as well as regulated differently in different locales. But clever technical solutions to those challenges may impose additional societal costs, e.g., by consuming substantial resources at odds with Green Computing, another major area of societal concern. We propose a new crosscutting research area, Societal Computing, that focuses on the technical tradeoffs among computational models and application domains that raise significant societal issues. We highlight some of the relevant research topics and open problems that we foresee in Societal Computing. We feel that these topics, and Societal Computing in general, need to gain prominence as they will provide useful avenues of research leading to increasing benefits for society as a whole.


title: A literate experimentation manifesto

abstract: This paper proposes a new approach to experimental computer systems research, which we call Literate Experimentation. Conventionally, experimental procedure and writeup are divided into distinct phases: i.e. setup (the method), data collection (the results) and analysis (the evaluation of the results). Our concept of a literate experiment is to have a single, rich, human-generated, text-based description of a particular experiment, from which can be automatically derived: (1) a summary of the experimental setup to include in the paper; (2) a sequence of executable commands to setup a computer platform ready to perform the actual experiment; (3) the experiment itself, executed on this appropriately configured platform; and, (4) a means of generating results tables and graphs from the experimental output, ready for inclusion in the paper.


title: Continuous demonstration


title: TouchDevelop: programming cloud-connected mobile devices via touchscreen

authors:
Nikolai Tillmann
Michal Moskal
Jonathan de Halleux
Manuel Fähndrich

abstract: The world is experiencing a technology shift. In 2011, more touchscreen-based mobile devices like smartphones and tablets will be sold than desktops, laptops, and netbooks combined. In fact, in many cases incredibly powerful and easy-to-use smart phones are going to be the first and, in less developed countries, possibly the only computing devices which virtually all people will own, and carry with them at all times. Furthermore, mobile devices do not only have touchscreens, but they are also equipped with a multitude of sensors, such as location information and acceleration, and they are always connected to the cloud. TouchDevelop is a novel application creation environment for anyone to script their smartphones anywhere -- you do not need a separate PC. TouchDevelop allows you to develop mobile device applications that can access your data, your media, your sensors and allows using cloud services including storage, computing, and social networks. TouchDevelop targets students, and hobbyists, not necessarily the professional developer. Typical TouchDevelop applications are written for fun, or for personalizing the phone.


title: Biological realms in computer science

abstract: In biology, evolution is usually seen as a tinkering process, different from what an engineer does when he plans the development of his systems. Recently, studies have shown that even in biology, there is a part of good engineering. As computer scientists, we have much more difficulty to admit that there is also a great deal of tinkering in what we do, and that our software systems behave more and more like biological realms every day. This essay relates my personal experience about this discovery.


title: Liberating the programmer with prorogued programming

authors:
Mehrdad Afshari
Earl T. Barr
Zhendong Su

abstract: Programming is the process of expressing and refining ideas in a programming language. Ideally, we want our programming language to flexibly fit our natural thought process. Language innovations, such as procedural abstraction, object and aspect orientation, have helped increase programming agility. However, they still lack important features that a programmer could exploit to quickly experiment with design and implementation choices.


title: Interruptible context-dependent executions: a fresh look at programming context-aware applications

authors:
Engineer Bainomugisha
Jorge Vallejos
Coen De Roover
Andoni Lombide Carreton
Wolfgang De Meuter

abstract: Context-aware applications provide end-users with enhanced experiences by continuously sensing their environment and adapting their behaviour to match the current context of use. However, developing true context-aware applications remains notoriously difficult due to the unpredictable nature of context changes. A context change may occur at any moment during a procedure execution, which may require an ongoing execution to be promptly interrupted in order to prevent the procedure from running in a wrong context. Currently, developers have to manually constrain a procedure execution to a particular context and take care of saving and restoring the execution state between context changes. Such manual approaches are error-prone and may lead to incorrect application behaviour.


title: Realising software development as a lived experience

abstract: This essay discusses software development from the perspective of Empirical Modelling (EM) [4], an approach to computing that draws on the construals of David Gooding [52], Bruno Latour's vexing notion of construction [70] and William James's radical empiricism [63]. It argues that effective software development must embrace semantic principles radically different from those endorsed by the traditional perspective on software that is based on computational thinking. Of paramount importance is the immediacy of the developer's experience of the relationship between software as an artefact on the computer and software as an agency in the world.