HOπ in Coq. - Guillaume Ambal; Sergueï Lenglet; Alan Schmitt (J. Autom. Reason., 2021)

Certified abstract machines for skeletal semantics. - Guillaume Ambal; Sergueï Lenglet; Alan Schmitt (CPP, 2022)

Certified Derivation of Small-Step From Big-Step Skeletal Semantics. - Guillaume Ambal; Sergueï Lenglet; Alan Schmitt; Camille Noûs (PPDP, 2022)

Skeletal semantics transformations. (Transformations de sémantiques squelettiques). - Guillaume Ambal (2022)

Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures. - Guillaume Ambal; Brijesh Dongol; Haggai Eran; Vasileios Klimis; Ori Lahav 001; Azalea Raad (Proc. ACM Program. Lang., 2024)

Sufficient Conditions for Robustness of RDMA Programs. - Guillaume Ambal; Ori Lahav 001; Azalea Raad (ESOP (1), 2025)