One example of my work is the ReCaml language, a work done jointly with Fabien Dagnat. ReCaml is a strongly-typed programming language for DSU, with mechanized operational semantics, type system and Coq proof of type soundness. It is based on the execution-state paradigm, which is shared with other works on DSU such as UpStare and Hofmeister & Purtilo (1993). This paradigm is highly flexible as it does not need that the target application suspends in a specific state such as quiescence. Further details on ReCaml, including source code and proof script can be found here.
Currently, I participate to the supervision of Sébastien Martinez (ongoing PhD thesis at Télécom Bretagne). One of his early contributions is the PyMoult library, which is a DSU prototyping platform for Python.
- Dynamic software upgrading
- Dynamic reconfiguration
- Dynamic software architecture