Modular Abstractions of Reactive Nodes Using Disjunctive Invariants. - David Monniaux; Martin Bodin (APLAS, 2011)

Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. - Jörg Endrullis; Dimitri Hendriks; Martin Bodin (ITP, 2013)

Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version). - Martin Bodin; Thomas P. Jensen; Alan Schmitt (Festschrift for Dave Schmidt, 2013)

Pretty-big-step-semantics-based Certified Abstract Interpretation. - Martin Bodin; Thomas P. Jensen; Alan Schmitt (JFLA, 2014)

A trusted mechanised JavaScript specification. - Martin Bodin; Arthur Charguéraud; Daniele Filaretti; Philippa Gardner; Sergio Maffeis; Daiva Naudziuniene; Alan Schmitt; Gareth Smith (POPL, 2014)

Certified Abstract Interpretation with Pretty-Big-Step Semantics. - Martin Bodin; Thomas P. Jensen; Alan Schmitt (CPP, 2015)

Certified semantics and analysis of JavaScript. (Sémantique et analyse certifiée de JavaScript). - Martin Bodin (2016)

A trustworthy mechanized formalization of R. - Martin Bodin; Tomás Diaz; Éric Tanter (DLS, 2018)

Skeletal semantics and their interpretations. - Martin Bodin; Philippa Gardner; Thomas P. Jensen; Alan Schmitt (Proc. ACM Program. Lang., 2019)

Two Mechanisations of WebAssembly 1.0. - Conrad Watt; Xiaojia Rao; Jean Pichon-Pharabod; Martin Bodin; Philippa Gardner (FM, 2021)