[UMN logo]

CSci 5980/8980, Spring 2024
Software Foundations

News Flash: Online discussion using Piazza

New Information




Table of Contents

Contact Information

Brief Course Description

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 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

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: 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

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. 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.