CMSC 15300-1: Foundations of Software

---

Index

Announcements
Instructor Contact Info
Course Description
Course Textbook
Course Policies
Course Mailing List
Course Schedule
Homework Assignments
Handouts
Programming in SML
SML/NJ FAQ

---

Announcements/Updates

There will be a special SML programming clinic in Ryerson 251 at 4pm on Monday, 11/27/06.

Instructor Contact Info

Name	Role	Office	Office hours	Phone	Email
David MacQueen	Professor	Hinds 045	By appointment	2-4980	dbm@cs.uchicago.edu
Henry Wu	TA	Ryerson 177	Monday 4:00-7:00	4-4416	xyzw2307 [at] yahoo [dot] com
Irina Matveeva	TA	Ryerson 177	Thursday 3:00-6:00	(773)702-6614	matveeva [at] cs [dot] uchicago [dot] edu

Course Description

This course is concerned with the mathematical foundations of computer software. It will introduce the student to a number of mathematical areas used in the modelling of programming languages and software, including propositional and predicate logic, basic set theory, relations, orderings, and finite state automata. Inductive definitions and proofs play a central role in formalizing and reasoning about programs, and will form a central theme of the course. The connection between mathematics and software will be made via examples and small programming assignments.

Students should have some programming experience. Programming examples and exercises will use the Standard ML (SML) programming language, which will be introduced in the class.

Course Textbook

The textbook for the course is Discrete Structures, Logic, and Computability by James Hein. A student study guide is also available from the publisher.

Programming Exercises

This is not a course centered on programming projects, but programming examples and exercises that show how to implement the ideas explored in the lectures and textbook will be given using the language Standard ML. There are several good sources of documentation and tutorials for SML/NJ available online, and some of these are given in the course SML/NJ page.

Course Policies

• Grading will be based on the following weightings:
• Homework exercises: 50%
• Midterm exam: 20%
• Final exam: 30%
• Assigments: Homework assignments will normally be given on Wednesdays and will be due at the beginning of class the following Wednesday. Late homework can be handed in the class following the due date with a 30% penalty. The default is to hand in hard copy, but if necessary homework can be submitted by email to dbm@cs.uchicago.edu. Neatness and clarity are important in submitted homework.
• Collaboration: We encourage students to discuss course material among themselves. Discussions of assignment problems is also permitted to some extent, but submitted assignments must be your own work, and collaborative discussions should be acknowledged in your homework write-up.
• Final Examination: The final examination will be a two hour in-class exam.

Course Mailing List

A mailing list has been created for the course. The address is cmsc15300@cs.uchicago.edu. The web page for the mailing list is at http://mailman.cs.uchicago.edu/mailman/listinfo/cmsc15300.

Course Schedule

Here is a tenative schedule of the lectures. This is subject to midcourse adjustment, of course.

Date	Topic	Reading
9/25	Introduction and admin
9/27	Sets	1.1-1.3
9/29	Relations	4.1
10/2	Functions	2.1-2.3
10/4	Equivalence Relations	4.2
10/6	Order Relations	4.3
10/9	Recursion and Induction
10/11	Fixed Points
10/13	Inductive structures
10/16
10/18
10/20
10/23
10/25	Midterm review
10/27	Midterm exam
10/30	Propositional Calculus	6.1-6.2
11/1	Propositional Calculus	6.3
11/3	Propositional Calculus
11/6	Predicate Calculus	7.1
11/8	Predicate Calculus	7.2-7.3
11/10	Predicate Calculus	7.2-7.3
11/13		Lambda Calculus
11/15
11/17
11/20
11/22
11/27
11/29
12/1	Reading Period

Homework Assignments

Here are links to PDF files of the homework assignments.
Homework 1 (due Oct 4)

• Solution 1.
• Grades Statistics Homework 1.

Homework 2 (due Oct 13)

• Solution 2.
• Grades Statistics Homework 2.

Homework 3 (due Oct 20);

• Solution 3.
• Grades Statistics Homework 3.

Homework 4 (due Oct 27).

• Solution 4.
• Grades Statistics Homework 4.

Homework 5 (due Nov 6).

• Solution 5
• Solution for problem 8 in SML (set.sml,wff.sml); set.sml; wff-mod.sml (modularized, updated).
• Grades Statistics Homework 5.

Homework 6 (due Nov 13)

• Solution 6
• Solution for Problem 6: quine.sml.
• Grades Statistics Homework 6.

Homework 7 (due Nov 20).

• Template code for Problem 11: pc.sml.
  You will also need the updated files wff-mod.sml and set.sml.
• Solution 7
• Solution for Problem 6: pc.sml.

Homework 8 (due Nov 29).

• Template code for Problem 2: proof.sml.

Midterm Solutions

Midterm Solutions

Grades Statistics Midterm.

Handouts

Here are links to PDF files of the handouts.
Outline of concepts
Sequent-style rules for Natural Deduction
Loading Source Files in SML

SML Code

Here are links to sample code.

set.sml A general set module (functor SetFn).
wff-mod.sml Wffs of propositional calculus.
quine.sml Quine's method of testing for tautologies.
lambda-EV.sml Lambda calculus evaluator.

Additional Useful Links

The book "Naive Set Theory" by Paul Halmos (published by Springer and available from Amazon for $39) is a slim and very readable account of what every mathematician (and I would add most computer scientists) should know about elementary set theory.