85 citations · 103 across the 13 of their papers we have counts for
15 papers
Linear Constraints
Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy +2
Linear constraints are the linear counterpart of Haskell's class constraints. Linearly typed parameters allow the programmer to control resources such as file handles and manually…
Refinement-Types Driven Development: A study
Facundo Domínguez, Arnaud Spiwack
This paper advocates for the broader application of SMT solvers in everyday programming, challenging the conventional wisdom that these tools are solely for formal methods and veri…
Invertible Syntax without the Tuples (Functional Pearl)
Mathieu Boespflug, Arnaud Spiwack
In the seminal paper Functional unparsing, Olivier Danvy used continuation passing to reanalyse printf-like format strings as combinators. In the intervening decades, the conversat…
Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes
Thomas Bagrel, Arnaud Spiwack
Destination passing -- aka. out parameters -- is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination pas…
Union and intersection contracts are hard, actually
Teodoro Freund, Yann Hamdaoui, Arnaud Spiwack
Union and intersection types are a staple of gradually typed language such as TypeScript. While it's long been recognized that union and intersection types are difficult to verify…
Evaluating Linear Functions to Symmetric Monoidal Categories
Jean-Philippe Bernardy, Arnaud Spiwack
A number of domain specific languages, such as circuits or data-science workflows, are best expressed as diagrams of boxes connected by wires. Unfortunately, functional languages h…