See DBLP for a full record.

Lambda-calculus and functional programming

Complexity and programming patterns

An abstract, log-sensitive space-cost measure for the weak lambda-calculus (2025) [ HAL | talk ]

A "reasonable" space-cost model for the weak lambda-calculus, equivalent to Turing cost for any logarithmic or higher space complexity. Main insight: the notion of descendant (from rewriting theory) can be used to characterize subterms that can simply be described by a pointer in the input. Corollary: weak lambda-calculus equipped with this measure defines the same space complexity classes than the standard Turing model, from L (logspace) upward.

T. Balabonski

How to fold a tree: programming exercises on Calder's mobiles (OlivierFest'25) [ EE ]

Exploring several ways of folding over a binary tree, with solutions to various problems on Calder's mobiles, focusing on algorithms that perform a single tree traversal.

T. Balabonski

Strategies for full reduction

A strong call-by-need calculus (LMCS, 2023) [ EE ]

Definition of a family of strong reduction strategies inspired from call-by-need, which actually benefit from strongness to reduce the number of reduction steps to normal form. Partially formalized with the proof assistant Abella.

T. Balabonski, A. Lanco, G. Melquiond

Foundations of strong call-by-need (ICFP'17) [ DOI | .pdf ]

Definition of a call-by-need strategy, extended to compute strong normal forms. The strategy is complete: whenever their exists a reduction path to a normal form, the strategy will find it.

T. Balabonski, P. Barenbaum, E. Bonelli, D. Kesner

Strategies for weak reduction

Weak optimality, and the meaning of sharing (ICFP'13) [ DOI | .pdf ]

The usual call-by-need strategy achieves Levy-optimality in the weak lambda-calculus. Without the sharing of subterms (a.k.a. memoization) used in call-by-need, such an optimal strategy could not be computable.

T. Balabonski

A unified approach to fully lazy sharing (POPL'12) [ DOI | .pdf ]

Usual presentations of full laziness are mostly equivalent. Fully lazy lambda-lifting establishes a bisimulation between the weak lambda-calculus and a first order orthogonal rewriting system.

T. Balabonski

Axiomatic sharing-via-labelling (RTA'12) [ DOI | .pdf ]

Adding labels to terms to represent sharing of subterms. Using such labels, some forms of graph rewriting can be expressed using only simple term rewriting.

T. Balabonski

La pleine paresse, une certaine optimalité (thèse) [ .pdf ]

Partage de sous-termes et stratégies de réduction en réécriture d'ordre supérieur.

T. Balabonski, sous la direction de D. Kesner

Semantics of concurrent programs

Semantics of atomics in C [ project page ]

Common Compiler Optimisations are Invalid in the C11 Memory Model, and what we can do about it (POPL'15) [ DOI | .pdf ]

The weak memory model of C11 forbids some program transformations that we would expect to be admissible. Some of these can be fixed by weakening or strengthening the semantics while respecting its spirit (and some remain open). Coq formalization included.

V. Vafeiadis, T. Balabonski, S. Chakraborty, R. Morisset, F. Zappa Nardelli

Separation logic [ project page ]

The Design and Formalization of Mezzo, a Permission-Based Programming Language (TOPLAS, 2016) [ EE | .pdf ]

Presentation of a programming language in the ML tradition, with a type system inspired by separation logic. Well-typed programs are guaranteed to be data-race free. Type-checker and Coq formalization of the type system included.

T. Balabonski, F. Pottier, J. Protzenko

Geometric interpretation

A geometric approach to the problem of unique decomposition of processes (CONCUR'10) [ DOI | .pdf ]

A solution to the problem of prime decomposability of a set of concurrent processes, based on a geometric semantics of concurrent programs.

T. Balabonski, E. Haucourt

Formalization of distributed computing [ project page ]

Synchronous Gathering without Multiplicity Detection: a Certified Algorithm (Theory of Computing Systems, 2019) [ DOI ]

A gathering algorithm for oblivious mobile robots that operate synchronously. In contrast to previous work, the algorithm does not assume the robots are capable of multiplicity detection. Coq formalization in the Pactole framework included.

T. Balabonski, A. Delga, L. Rieg, S. Tixeuil, X. Urbain

Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots on Graphs (NETYS'19)

Formalization of asynchronous operation of mobile robots swarms. In this context, proof of equivalence of two graph-based models: instantaneous moves from vertex to vertex, vs continuous moves along edges with discrete observations. Coq formalization in the Pactole framework included.

T. Balabonski, P. Courtieu, R. Pelle, L. Rieg, S. Tixeuil, X. Urbain

A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs (ICDCN'18) [ DOI | .pdf ]

Formalization of the model of swarms of oblivious robots moving in a discrete space. Proof of impossibility of the problem of exploration with stop of a ring-shaped graph when the number of robots divides the size of the ring. Coq formalization in the Pactole framework included.

T. Balabonski, R. Pelle, L. Rieg, S. Tixeuil