ACL2 is a mathematical logic, programming language, and mechanical theorem prover based on the applicative subset of Common Lisp. It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.
CL-BibTeX is a replacement for the BibTeX program, written in Common Lisp. The aim is to enable the user to format bibliographic entries using Common Lisp programs, rather than using the stack language of BibTeX style files. A compiler that transforms BibTeX style files into comprehensible Common Lisp programs is included.
Charlemagne is a versatile genetic programming application. It includes a commandline client and an interactive console mode. It is written in Python and Lisp, and is user extensible to some degree in both languages. It features built-in input-output mapping support and provides the ability to define complex fitness calculations in Lisp or Python.
Common Lisp Quick Reference is a booklet with short descriptions of the thousand or so symbols defined in the ANSI standard. It comes with a comprehensive index. It is written in LaTeX and formatted for printing on both A4 and letter paper. After folding the sheets lengthwise, they can easily be turned into a handy booklet.
IPA-CXS/X-Sampa Converter is a selection of modules for various programming languages (C, Perl, Lisp, and Python) for translating between IPA (International Phonetic Alphabet) and ASCII versions, in particular CXS, which is a close relative to X-Sampa. The project homepage contains a demo for using the Perl script as an online converter.