Soundness of the simply typed lambda calculus in ACL2

Sol Swords, William R. Cook. Soundness of the simply typed lambda calculus in ACL2. In Panagiotis Manolios, Matthew Wilding, editors, Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006. pages 35-39, ACM, 2006. [doi]

@inproceedings{SwordsC06,
  title = {Soundness of the simply typed lambda calculus in ACL2},
  author = {Sol Swords and William R. Cook},
  year = {2006},
  doi = {10.1145/1217975.1217982},
  url = {http://doi.acm.org/10.1145/1217975.1217982},
  tags = {type soundness},
  researchr = {https://researchr.org/publication/SwordsC06},
  cites = {0},
  citedby = {0},
  pages = {35-39},
  booktitle = {Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006},
  editor = {Panagiotis Manolios and Matthew Wilding},
  publisher = {ACM},
  isbn = {0-9788493-0-2},
}