Course on a Mathematical Presentation of Functional Programming

We present the motivations, syllabus and teaching method of Foundations of Computing, a course of Mathematics whose objects are given by a functional programming language. 1 Motivation We teach within a Software Engineering program which is 10 semesters long, with each semester com- prising 16 weeks of lessons including examinations. We are in charge of the design and teaching of the courses of the Theoretical Computing Science area. The first course belonging to this area that students used to encounter was, until the beginning of the school year of 2013, (Mathematical) Logic, placed in the Second Semester of the program. It comprised the classical Propositional and First-Order material plus an initial part on Induction and Recursion. This part was necessary for the students to learn to define sets (notably, languages) inductively, and to compose recursive functions and proofs by induction on such sets, all of them methods to be used in the rest of the course and not taught elsewhere. Besides, ours was the only serious introduction to such matters prior to the Algorithms and Data Structures courses, which also belong to our area. As a consequence, the Logic course was divided into three parts of almost the same size, all of them a little bit too much compressed for the students to be able to fully incorporate the relevant material. In particular, we had become unsatisfied with the degree of understanding and mastery that the students were able to reach of the methods of recursive definitions of functions and their close connection to proof by induction. Reflection on the matter, together with the emergence of a timely reformulation of the entire program of studies, led us to realize that we were actually in the presence of an opportunity to address a combination of significant issues, which we would like now to expose in detail. The prime observation is that Induction and Recursion is of course a mathematical subject but, as such, it is possibly the one lying closest to Programming, so much so that it can be thought of being introduced as a mathematical presentation of Programming. This is possible by letting programs be functions, generally recursive and acting on inductive data types, i.e. by considering some form of functional programming. These functional programs would become the relevant mathematical objects, which means that their properties were to be investigated and proven, generally by induction. Going this way, we could then just take the path of promoting our Induction and Recursion material into a (first) course on Functional Programming, one that included the appropriate techniques of program proof. Sample courses and textbooks fairly meeting such description abound, so that setting up the syllabus and plan ought not to be a problem. On the other hand, we would need a full semester slot to actually teach it, but that was fortunately put at our disposal, as a new course was created in the Second Semester, displacing our previous Logic to the Third. It is important here to mention that the new program of studies includes initial courses on Programming in the first two semesters, in which the Java language is