James McDonald & John Anton (2001):
SPECWARE - Producing Software Correct by Construction.
Sol Swords & William R. Cook (2006):
Soundness of the Simply Typed Lambda Calculus in ACL2.
In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications,
ACL2 '06.
ACM,
New York, NY, USA,
pp. 35–39,
doi:10.1145/1217975.1217982.