Modular Type-Safety Proofs using Dependant Types - Christopher Schwaab; Jeremy G. Siek (CoRR, 2012)

Modular type-safety proofs in Agda. - Christopher Schwaab; Jeremy G. Siek (PLPV, 2013)

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

Verified programming with explicit coercions. - Christopher Schwaab (2019)