Proof-Carrying Plans. - Christopher Schwaab; Ekaterina Komendantskaya; Alasdair Hill; Frantisek Farka; Ronald P. A. Petrick; Joe B. Wells; Kevin Hammond (PADL, 2019)

Proof-Carrying Plans: a Resource Logic for AI Planning. - Alasdair Hill; Ekaterina Komendantskaya; Ronald P. A. Petrick (PPDP, 2020)

Actions you can handle: dependent types for AI plans. - Alasdair Hill; Ekaterina Komendantskaya; Matthew L. Daggitt; Ronald P. A. Petrick (TyDe@ICFP, 2021)

Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. - Andre Knispel; Orestis Melkonian; James Chapman 001; Alasdair Hill; Joosep Jääger; William J. DeMeo; Ulf Norell (FMBC@CAV, 2024)

IntersectMBO/formal-ledger-specifications. - Andre Knispel; Orestis Melkonian; James Chapman 001; Alasdair Hill; Joosep Jääger; William J. DeMeo; Ulf Norell (DROPS Artifacts, 2024)