Piergiorgio Bertoli & Paolo Traverso (2000):
Design Verification of a Safety-Critical Embedded Verifier,
pp. 233–245.
Springer US,
Boston, MA,
doi:10.1007/978-1-4757-3188-0_14.
Ruben Gamboa, John Cowles & JV Baalen (2003):
Using ACL2 Arrays to Formalize Matrix Algebra.
In: Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL203) 1.
Thomas J Jech (2008):
The Axiom of Choice.
Courier Corporation.