Mine is in Python with several usual and some less usual influences: John McCarthy "Recursive Functions of..." by way of Paul Graham "The Roots of Lisp"; Peter Norvig "(How to Write..." and tail recursion from his "(An ((Even Better)..."; quoted-printable encoding of characters; Wikipedia & Knuth's enthusiasm for the balanced ternary number base. I have gone a very short way to start translating Lisp programs to Python code. Also I have gone a very short way to do relevant proofs in Coq in the manner of Benjamin C. Pierce, et al. "Software Foundations". My notions are to implement the Calculus of Constructions in the simplified form found in Claudio S. Coen, "Mathematical Libraries as Proof Assistant Environments", and natural deduction on top of that. And a TR SECD machine. Oh, and algorithms from Artificial Intelligence: A Modern Approach. And a pony... http://github.com/minopret/minopret-lisp