- Lambda-calculus and functional programming
- Strategies for full reduction
- Strategies for weak reduction

- Formal proofs for mobile robot swarms protocols
- Concurrency
- Semantics of atomics in C
- Separation logic
- Geometric interpretation

## Lambda-calculus and functional programming

### Strategies for full reduction

#### 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*

## Formal proofs for mobile robot swarms protocols [ 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*

## Concurrency

### 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*