A right-to-left type system for mutually-recursive value definitions. - Alban Reynaud; Gabriel Scherer; Jeremy Yallop (CoRR, 2018)

Linear Inequalities. - Ralph Bottesch; Alban Reynaud; René Thiemann (Arch. Formal Proofs, 2019)

Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. - Ralph Bottesch; Max W. Haslbeck; Alban Reynaud; René Thiemann (NFM, 2020)

A practical mode system for recursive definitions. - Alban Reynaud; Gabriel Scherer; Jeremy Yallop (Proc. ACM Program. Lang., 2021)

Modular verification of op-based CRDTs in separation logic. - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2022)

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Zenodo, 2022)

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Zenodo, 2022)