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. The course sequence has been offered twice, so far, in two consecutive academic years. Certain improvements evolved in the second offering, and while this report focuses on that offering, it also offers reasons for the changes. The discussion outlines the topical coverage and required projects, suggests further improvements, and observes educational effects based on conversations with students and evaluations of their cou...
Rex L. Page