1,066 papers · page 8 of 54
Mahsa Varshosaz, Mohsen Ghaffari, Einar Broch Johnsen, Andrzej Wasowski
The development process for reinforcement learning applications is still exploratory rather than systematic. This exploratory nature reduces reuse of specifications between applications and increases the chances of introducing programming errors. This paper takes a step towards s…
Ningning Xie, Leo White, Olivier Nicole, Jeremy Yallop
We introduce MacoCaml, a new design and implementation of compile-time code generation for the OCaml language. MacoCaml features a novel combination of macros with phase separation and quotation-based staging, where macros are considered as compile-time bindings, expression cross…
Zhixuan Yang, Nicolas Wu
Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations. The framework covers not only algebraic operations but also scoped and variable-binding …
Beniamino Accattoli, Giulio Guerrieri
The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semanti…
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
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 λ-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provi…
Patrick Bahr, Graham Hutton
Bahr and Hutton recently developed a new approach to calculating correct compilers directly from specifications of their correctness. However, the methodology only considers converging behaviour of the source language, which means that the compiler could potentially produce arbit…
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
We study the nature of applicative bisimilarity in λ-calculi endowed with operators for sampling from contin- uous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with contextual equivalence when real numbers ca…
Malgorzata Biernacka, Witold Charatonik, Tomasz Drab
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 be…
Frank Emrich, Jan Stolarek, James Cheney, Sam Lindley
FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to Algori…
Joseph Eremondi, Ronald Garcia, Éric Tanter
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a central feature of type the…
Lucas Escot, Jesper Cockx
Datatype-generic programming makes it possible to define a construction once and apply it to a large class of datatypes. It is often used to avoid code duplication in languages that encourage the definition of custom datatypes, in particular state-of-the-art dependently typed lan…
Son Ho, Jonathan Protzenko
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to eliminate memory reasoning for a large class of Rust programs, as long as they do not rely on interior mutability o…
Tram Hoang, Anton Trunov, Leonidas Lampropoulos, Ilya Sergey
We describe our experience of using property-based testing---an approach for automatically generating random inputs to check executable program specifications---in a development of a higher-order smart contract language that powers a state-of-the-art blockchain with thousands of …
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
Session types have recently been integrated with functional languages, bringing message-passing concurrency to functional programming. Channel endpoints then become first-class and can be stored in data structures, captured in closures, and sent along channels. Representatives of…
Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, Nicolas Wu
A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads are a generalization of mona…
Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese
Verifying soundness of symbolic execution-based program verifiers is a significant challenge. This is especially true if the resulting tool needs to be usable outside of the proof assistant, in which case we cannot rely on shallowly embedded assertion logics and meta-programming.…
Hsiang-Shang Ko, Liang-Ting Chen, Tzu-Chi Lin
Datatype-generic programming is natural and useful in dependently typed languages such as Agda. However, datatype-generic libraries in Agda are not reused as much as they should be, because traditionally they work only on datatypes decoded from a library’s own version of datatype…
James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, Nadia Polikarpova
Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on building specialized data structures—version-space algebras, finite tree automata, or e-graphs—to compact…
James Koppel, Jackson Kearl, Armando Solar-Lezama
We develop the first theory of control-flow graphs from first principles, and use it to create an algorithm for automatically synthesizing many variants of control-flow graph generators from a language’s operational semantics. Our approach first introduces a new algorithm for con…
András Kovács
The aim of staged compilation is to enable metaprogramming in a way such that we have guarantees about the well-formedness of code output, and we can also mix together object-level and meta-level code in a concise and convenient manner. In this work, we observe that two-level typ…