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 the 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 off-reductions and the size of the input term.
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. This, 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.
Over the past fifteen years, several languages for functionalreactive programming (FRP) have been suggested that use modaltypes to ensure properties like causality, productivity, and lack ofspace leaks. So far, almost all of these languages have included amodal operator for delay on a global clock. For some applications,however, a global clock is unnatural and leads to leakyabstractions as well as inefficient implementations. While modallanguages without a global clock have been proposed, no operationalproperties have been proved about them yet.This paper proposes Async RaTT, a new modal language for asynchronousFRP, equipped with an operational semantics mapping completeprograms to machines that take asynchronous input signals andproduce output signals. The main novelty of Async RaTT is a new modalityfor asynchronous delay, allowing each output channel to beassociated at runtime with the set of input channels it depends on,thus causing the machine to only compute new output when necessary.We prove a series of operational properties including causality,productivity, and lack of space leaks. We also show that, althoughthe set of input channels associated with an output channel canchange dynamically during execution, upper bounds on these can bedetermined statically by the type system.
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)
