Rémi Douence

Sidney Congard, Guillaume Munch-Maccagnoni, Rémi Douence

We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad $T(- \oplus E)$ in a linear setting. We consider in particular for $T$ the allocation monad, which we introduce to model and study resource-safety properties. We apply these results to a series of two linear effectful calculi for which we establish their resource-safety properties. The first calculus is a linear (optionally ordered) call-by-push-value language with two allocation effects $\mathbf{new}$ and $\mathbf{delete}$. The resource-safety properties follow from the linear and ordered character of the typing rules. We then integrate exceptions with linearity and effects by adjoining default destruction actions to types, as inspired by C++/Rust destructors. We see destructors as objects $δ: A\rightarrow TI$ in the slice category over $TI$. This construction gives rise to a second calculus, the resource call-by-push-value, featuring exceptions and destructors, and whose weakening and exchange rules perform side-effects. It is therefore affine at the level of types but ordered at the level of derivations. As in C++ and Rust, a ``move'' operation -- the side-effecting exchange rule -- is necessary for releasing resources in random order, as opposed to LIFO order.

Jovial Cheukam-Ngouonou, Ramiz Gindullin, Nicolas Beldiceanu et al.

We present the proofs of the conjectures mentioned in the paper published in the proceedings of the 2024 AAAI conference [1], and discovered by the decomposition methods presented in the same paper.

Ekaterina Arafailova, Nicolas Beldiceanu, Rémi Douence et al.

First this report presents a restricted set of finite transducers used to synthesise structural time-series constraints described by means of a multi-layered function composition scheme. Second it provides the corresponding synthesised catalogue of structural time-series constraints where each constraint is explicitly described in terms of automata with registers.

Julien Cohen, Rémi Douence, Akram Ajouli

When one chooses a main axis of structural decompostion for a software, such as function- or data-oriented decompositions, the other axes become secondary, which can be harmful when one of these secondary axes becomes of main importance. This is called the tyranny of the dominant decomposition. In the context of modular extension, this problem is known as the Expression Problem and has found many solutions, but few solutions have been proposed in a larger context of modular maintenance. We solve the tyranny of the dominant decomposition in maintenance with invertible program transformations. We illustrate this on the typical Expression Problem example. We also report our experiments with Java and Haskell programs and discuss the open problems with our approach.