Daniel J. Singer

Here are my publically available papers and work on computer science topics:

Proving Type Soundness of Simple Languages in ACL2

The paper is here: Proving Type Soundness of Simple Languages in ACL2
The source code of the Lisp list language is here: Ps.lisp
The source code of the string language is here: Ps as Strings.lisp
Both of the source codes are formatted as ACL2 books but can be read and used just like any Lisp code.


If you'd like more information about any projects listed here, please contact me.

• Philosophy at the University of Michigan
• Go Grue!
• Me on Facebook
• The Leiter Reports
• Thoughts Arguments and Rants
• The University of Michigan
• The Philomathean Society
• Nobody
• Sympose