Lambda the Ultimate

Rex Page, Engineering software correctness, Proceedings of the ACMS,PLAN 2005 Workshop on Functional and Declarative Programming in Education, September 25, 2005.

Software engineering courses offer one of many opportunities for
providing students with a significant experience in declarative
programming. This report discusses some results from taking
advantage of this opportunity in a two-semester sequence of
software engineering courses for students in their final year of
baccalaureate studies in computer science. The sequence is based
on functional programming using ACL2, a purely functional
subset of Common Lisp with a built-in, computational logic
developed by J Strother Moore and his colleagues over the past
three decades...

A JFP educational pearl with the same title and a similar abstract appears in Journal of Functional Programming (2007), 17: 675-68, but I haven't managed to access it yet.

I am still in the process of finding furniture etc. But at least I have an apartment now... Thanks for all the help and tips, guys!