CSci 5980/8980, Spring 2024
Software Foundations

News Flash: Online discussion using Piazza

New Information

03/25/2024

Reading assignment for March 27: Simple Imperative Programs and An Evaluation Function for Imp.
Homework 8, which was announced last Monday, is due on March 27; this has been delayed from March 25, due to some confusion about the due date that students indicated after class today.

01/22/2024

The slides used in the first lecture have been posted on the notes section of the course web page.

01/16/2024

This area will typically highlight content on this page that becomes available between classes and that has not been explicitly announced at a class meeting. Note that class attendance and keeping track of things going on there as well as on the course web page are required components of this course.
We will use Piazza extensively for discussions in this course. Please read the comments on etiquette for interactions that I have posted here and register on the Piazza page as soon as possible.
Lectures are only a small part of the learning process in a course, especially in one that is organized in seminar style like this one. Independent work, combined with discussions, are a much more valuable part. Please participate enthusiastically, especially via Piazza; I will be watching that space and will try to contribute as well as to learn from all of you!
Reading assignments: for 01/22/24, read the Preface and Functional Programming in Coq chapters, for 01/24/24 read Proofs by Induction.

Contact Information
Brief Course Description
Course Prerequisites
Books and Software
Required Work and Grading
Papers and Related Materials
Notes and Lecture Slides
Homeworks
Policies and Related Information
Links to Miscellaneous Online Resources

Contact Information

Lecture Times and Place: M, W 4:00 - 5:15 p.m., Amundson Hall 156
Instructor: Gopalan Nadathur
Email: (ngopalan atsign umn.edu)
Phone: 612-626-1354
Office: Keller Hall 6-215
Office Hours: T 10:00 - 11:00 a.m., by appointment

The penetration of computational artifacts into almost every aspect of modern society has placed a high premium on building software that is secure, free of bugs and generally reliable. Computer Science has responded to this challenge by developing techniques for managing projects, structuring programming teams and organizing libraries so as to enhance the reliability of the resulting software, by designing programming languages that possess strong formal properties and provide high degrees of abstraction, and by developing mathematical techniques for specifying and reasoning about properties of software and tools for applying these techniques in practical ways.

This course concerns the last of these lines of development. In particular, it will explore five interrelated conceptual threads related to the task of formally establishing properties of software:

the use of logic for making and justifying precise claims about programs;
the use of proof assistants for constructing rigorous arguments that verify such claims;
the use of functional programming as a bridge between programming and logic;
the use of formal techniques for reasoning about the properties of specific programs; and
the use of types as a means for stating deep properties of programs and the use of type checking as a means for ensuring such properties hold.

The focus will be on practical aspects: the course will be oriented around a hands-on use of the Coq system, a versatile and popular proof assistant, to construct actual programs and to state and prove properties about them. There will still be mathematical content to the discussion, but it will be oriented towards understanding logic, types and proofs so as to make effective use of them; the deeper properties of the logical systems that will be used will not be examined in the lectures, although they can be the topic of projects and class presentations for students taking the CSci 8980 version of the course.

Course Prerequisites

The course is appropriate for graduate and advanced undergraduate students in Computer Science interested in logic and programming languages. A previous course on these topics would be helpful, a good example of such a course being CSci 5106, but this is not essential. An indispensible quantity, though, is mathematical maturity: the student must be able to differentiate between a correct formal argument and an incomplete or incorrect one, they should know what induction is and she should be able to construct proofs of some complexity on their own.

Books and Software

This course will follow closely the online texts that are collectively labelled Software Foundations. We will begin by covering the material in Volume 1 entitled Logical Foundations. The plan then is to move on to Volume 2 entitled Programming Language Foundations or to Volume 3 entitled Verified Functional Algorithms; a decision on this will be made during the term based also on what the class itself wants.
You will need to download and install a recent version of Coq. The preface to Logical Foundations says the book has been tested with Coq 8.17, so I presume that or a later version would work well. I have version 8.18.0 installed on my laptop. From the the Coq page and the preface again, it seems that the recommended installation approach is to use Coq Platform. I have installed it on my laptop using opam; I think that this should work just as well, at least if one interacts with Coq through coqide (see below) or through emacs using the Proof General. (I believe that the installation sets up the Coq compiler coqc, the Coq read-eval-print loop coqtop, and the standard Coq libraries, and these are used by whatever IDE you set up to use for your interactions with Coq.)
You will also need some IDE within which you can develop your own Coq proofs. One reasonable alternative is coqide; I downloaded this package on my laptop using opam, and it looks like you may get this "for free" if you install Coq using Coq Platform. Another popular IDE is Proof General: you may prefer to get this one because it is a generic IDE for proof assistants that runs under emacs, i.e. you can use it for working with other proof assistants as well once you have learnt it. There are more suggestions in the preface of the Logical Foundations volume and I am hoping that people will share there experience and issues with downloading and setting up Coq via the relevant Piazza forum.
You will not really need anything more than the above, and readings available through the web for this course. However, there are a few other books that I should mention as being relevant to look at, should you want to pursue matters beyond what you see here:
- Types and Programming Languages, B.C. Pierce, MIT Press, ISBN 0-262-16209-1.
- Interactive Theorem Proving and Program Development, Yves Bertot and Pierre Castéran, Springer-Verlag, ISBN 3-540-20854-2.
- Certified Programming with Dependent Types, A. Chlipala, MIT Press, ISBN: 9780262026659.
- Program Logics for Certified Compilers , A. Appel et al, Cambridge University Press, ISBN-13: 9781107048010.

I provide links to useful electronic resources, such as manuals and papers, at a different location on this page.

Required Work and Grading

First, there are a core set of requirements for the CSci 5980 and the CSci 8980 versions of the course:

Reading Assignments. You will need to read about a chapter each week from the online text. Carrying out these reading assignments is essential. The class will not follow a standard lecture format. Instead we will spend time discussing and trying to address questions that may have arisen in the course of the reading. Thus, you will be out-of-place if you have not read the assigned material.
Class attendance and participation in discussions. The expectation is that you are taking this course because you are interested in the material and in the discussions about it, so you will be expected to be present in class for this to happen. You must also follow whatever happens on Piazza and participate enthusiastically in the discussions there as well.
Homework exercises. Homework problems, which typically will involve completing the exercises in each chapter of the online book, will be assigned periodically with a prescribed deadline. These deadlines will designed to ensure synchrony with what we will be doing in class and must be adhered to. You will be expected to turn in solutions by the deadlines. There is a builtin grace period of 7 days over all the homeworks that you may use in the way you choose with the proviso that no homework must be turned in more than two days late.

For CSci 8980, there is an additional requirement. Each student will have to take on some independent work, write a report on it and present the work in class. This work could be that of looking further in the six volume book, understanding the material there and demonstrating this understanding through the writeup and class presentation. It could also be that of picking up on a topic related to Coq (for example, the lambda calculus that Coq is based on), reading some papers on it and then demonstrating this understanding through a report and presentation.

In determining grades for CSci 5980, I will assign 10% weight to attendance and participation and 90% to the homeworks. For CSci 8980, class attendance and participation will carry 10% weight, homeworks will count for 60% and the independent work will count for 30%.

There are specific requirements and deadlines for the projects for the CSci 8980 version. You must discuss with me a possible topic by Feb 14, you should provide me about a one page description of what you plan to do for the project by March 13, you should be ready for a presentation in class on or after April 8, and the report should be turned in by April 29.

This being a topics course, I am assuming that everyone who has registered for it is doing so out of interest and a genuine desire to learn the material to be covered. I would therefore like to downplay the evaluative nature of the course and to focus on the more productive aspect of discovering new and interesting things together. Consequently, in assessing homeworks, I would be looking more to determine the effort and the level of intellectual involvement rather than to grade you for correctness. Note that you can test your solutions to problems from the book before turning them in, so "correctness" in the literal sense will already be known in most cases. This will be a little different for problems that I assign that do not appear in the text, but, even here, Coq will tell you if you have gotten a solution or not. The homeworks should also stimulate discussions and we can share information that helps us learn and to understand how to come up with more elegant solutions than the ones we might think of ourselves; the main requirement is that you must eventually do the work you turn in on your own, possibly after discussions, and you must not simply copy stuff from one of your classmates or from the web. For the projects for the CSci 8980 version, I will provide feedback on the presentations and writeups and may even "grade" them. However, for the purpose of determining a letter grade for the course, what I will be looking at is the involvement in the topic and the effort put into learning the material and organizing your thoughts to produce a cogent presentation and writeup.

To summarize my sentiments at the start of the semester, I am hoping that everyone will do the required work with application and enthusiasm, that we will have a fun semester and that I will not have to make distinctions between students when assigning a letter grade. The requirements and how I will be determing fulfillment are important to state so that you know what is expected of you during the term.

One final, important point. As I have indicated above, regular class attendance is required. If you have to miss a class, make sure to discuss this with me beforehand: absence is quite noticeable in a small class. Also, while you make miss a regular meeting based on circumstances, attendance during student presentations is mandatory; this is true for both the CSci 5980 and 8980 versions. Make sure to schedule any events that could potentially conflict with class attendance for before April 8 for this reason.

Policies and Related Information

Academic Honesty

I am going to assume that students in this class are familiar with the notion of academic honesty and are also aware what is expected of them in this regard. The department has a default set of policies related to this that you will find here.

There are perhaps two main things to stress in for this class. First, while discussions about assigned work and looking up material on the web is perfectly fine, any work that you turn in must represent your own understanding and effort; specifically, you must not have copied stuff from a colleague or what you have found on the web and you must be able to explain what you have done if you are asked. Second, you must include attributions in what you write or turn in if you have gotten substantial help from some other source. Not doing so is tantamount to trying to cheat and it is also makes you guilty of plagiarism, a particularly serious crime in academic circles.

Makeup Work for Legitimate Absences

Students will not be penalized for absence during the semester due to unavoidable or legitimate circumstances. Such circumstances include verified illness, participation in intercollegiate athletic events, subpoenas, jury duty, military service, bereavement, and religious observances. For information on what constitutes a legitimate absence and the attendant policies, please check out the Administrative Policy on Makeup Work for Legitimate Absences .

Equity, Diversity, Equal Opportunity, and Affirmative Action

The University is committed to providing equal access and opportunity to all in its programs and facilities, without regard to race, color, creed, religion, national origin, gender, age, marital status, disability, public assistance status, veteran status, sexual orientation, gender identity, or gender expression. For more information, please consult Board of Regents Policy on Equity, Diversity, Equal Opportunity, and Affirmative Action.

Disability Accommodations

The University of Minnesota views disability as an important aspect of diversity, and is committed to providing equitable access to learning opportunities for all students. The Disability Resource Center (DRC) is the campus office that collaborates with students who have disabilities to provide and/or arrange reasonable accommodations.

If you have, or think you have, a disability in any area such as, mental health, attention, learning, chronic health, sensory, or physical, please contact the DRC office on your campus (612.626.1333) to arrange a confidential discussion regarding equitable access and reasonable accommodations.
Students with short-term disabilities, such as a broken arm, can often work with instructors to minimize classroom barriers. In situations where additional assistance is needed, students should contact the DRC as noted above.
If you are registered with the DRC and have a disability accommodation letter dated for this semester or this year, please contact your instructor early in the semester to review how the accommodations will be applied in the course.
If you are registered with the DRC and have questions or concerns about your accommodations please contact your (access consultant/disability specialist).

Additional information is available on the DRC website. Students may also email drc@umn.edu with questions.

Mental Health and Stress Management

As a student you may experience a range of issues that can cause barriers to learning, such as strained relationships, increased anxiety, alcohol/drug problems, feeling down, difficulty concentrating and/or lack of motivation. These mental health concerns or stressful events may lead to diminished academic performance or reduce your ability to participate in daily activities. University of Minnesota services are available to assist you with addressing these and other concerns you may be experiencing. You can learn more about the broad range of confidential mental health services available on campus from the Student Mental Health website.

Sexual Harrassment

Sexual harassment means unwelcome sexual advances, requests for sexual favors, and/or other verbal or physical conduct of a sexual nature. Such conduct has the effect of unreasonably interfering with an individual's work or academic performance or creating an intimidating, hostile, or offensive working or academic environment in any University activity or program. Such behavior is not acceptable in the University setting. For additional information, please consult the Board of Regents Policy on this matter.

Academic Freedom

Academic freedom is a principle that is fundamental to intellectual inquiry. This notion includes the freedom to discuss relevant matters in the classroom, within the scope of the course as defined by the instructor. Students are encouraged to develop the capacity for critical judgment and to engage in a sustained and independent search for truth. Students are free to take reasoned exception to the views offered in any course of study and to reserve judgment about matters of opinion, even while they are responsible for learning the content of any course of study for which they are enrolled.

Links to Online Resources

Links to some of the resources that might be useful during the term:

Last modified on March 25, 2024 by ngopalan atsign umn dot edu.

The views and opinions expressed in this page are strictly those of the page author(s). The contents of this page have not been reviewed or approved by the University of Minnesota.

CSci 5980/8980, Spring 2024 Software Foundations