Formal Semantics of DRMA-Style Programming in BSPlib. - Julien Tesson; Frédéric Loulergue (PPAM, 2007)

Program Calculation in Coq. - Julien Tesson; Hideki Hashimoto; Zhenjiang Hu; Frédéric Loulergue; Masato Takeichi (AMAST, 2010)

Systematic Development of Correct Bulk Synchronous Parallel Programs. - Louis Gesbert; Zhenjiang Hu; Frédéric Loulergue; Kiminori Matsuzaki; Julien Tesson (PDCAT, 2010)

AVerified Bulk Synchronous ParallelMLHeat Diffusion Simulation. - Julien Tesson; Frédéric Loulergue (ICCS, 2011)

Environnement pour le développement et la preuve de correction systèmatiques de programmes parallèles fonctionnels. (Environment for the systematic development and proof of correction of functional parallel programs). - Julien Tesson (2011)

A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays. - Wadoud Bousdira; Frédéric Loulergue; Julien Tesson (ICA3PP (1), 2012)

Programming with BSP Homomorphisms. - Joeffrey Legaux; Zhenjiang Hu; Frédéric Loulergue; Kiminori Matsuzaki; Julien Tesson (Euro-Par, 2013)

A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. - Kento Emoto; Frédéric Loulergue; Julien Tesson (ITP, 2014)

Formal derivation and extraction of a parallel program for the all nearest smaller values problem. - Frédéric Loulergue; Simon Robillard; Julien Tesson; Joeffrey Legaux; Zhenjiang Hu (SAC, 2014)

Implementing Powerlists with Bulk Synchronous Parallel ML. - Frédéric Loulergue; Virginia Niculescu; Julien Tesson (SYNASC, 2014)

Multi-ML: Programming Multi-BSP Algorithms in ML. - Victor Allombert; Frédéric Gava; Julien Tesson (Int. J. Parallel Program., 2017)

Calculating Parallel Programs in Coq Using List Homomorphisms. - Frédéric Loulergue; Wadoud Bousdira; Julien Tesson (Int. J. Parallel Program., 2017)

Toward Performance Prediction for Multi-BSP Programs in ML. - Victor Allombert; Frédéric Gava; Julien Tesson (ICA3PP (3), 2018)

A Formal Semantics of the MULTI-ML Language. - Victor Allombert; Frédéric Gava; Julien Tesson (ISPDC, 2018)

Interactive Bulk Synchronous Parallel Functional Programming in a Browser. - Julien Tesson; Frédéric Loulergue (SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI, 2018)

Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts. - Bruno Bernardo; Raphaël Cauderlier; Zhenlei Hu; Basile Pesin; Julien Tesson (FM Workshops (1), 2019)

Introduction to the Tezos Blockchain. - Victor Allombert; Mathias Bourgoin; Julien Tesson (HPCS, 2019)

Albert, An Intermediate Smart-Contract Language for the Tezos Blockchain. - Bruno Bernardo; Raphaël Cauderlier; Basile Pesin; Julien Tesson (Financial Cryptography Workshops, 2020)

Making Tezos Smart Contracts More Reliable with Coq. - Bruno Bernardo; Raphaël Cauderlier; Guillaume Claret; Arvid Jakobsson; Basile Pesin; Julien Tesson (ISoLA (3), 2020)

A type system to avoid runtime errors for Multi-ML. - Frédéric Gava; Victor Allombert; Julien Tesson (ISPDC, 2022)