CS 720: Logical Foundations of Computer Science
- Lecture 1 [PDF], Sept 4 (Tue): Introduction (
- Lecture 2 [PDF], Sept 6 (Thu): Induction (
- Lecture 3 [PDF], Sept 11 (Tue): Data structures (
- Sept 12 (Wed): Homework 1 due:
- Lecture 4 [PDF], Sept 13 (Thu): Lists, Polymorphism (
- Lecture 5 [PDF], Sept 18 (Tue): Tactics (
Tactics.v). Homework 2 due:
- Lecture 6 [PDF], Sept 20 (Thu): More tactics (
- Lecture 7 [PDF], Sept 25 (Tue): Logic in Coq (
Logic.v). Homework 3 due:
- Lecture 8 [PDF], Sept 27 (Thu): Logic in Coq (
Logic.v). Homework 4 due:
- Lecture 9 [PDF], Oct 2 (Tue): Inductively defined propositions (
- Lecture 10 [PDF], Oct 4 (Thu): Inductively defined propositions and proof objects (
ProofObjects.v) Homework 5 due:
- Lecture 11 [PDF], Oct 9 (Tue): Total and partial maps, modeling an imperative programming language (
- Lecture 12 [PDF], Oct 11 (Thu): More automation (
Auto.v) Homework 6 due:
- Lecture 13 [PDF], Oct 16 (Tue): Program equivalence (
- Lecture 14 [PDF], Oct 18 (Thu): Hoare Logic (
Hoare.v). Homework 7 due:
- Lecture 15 [PDF], Oct 23 (Tue): Hoare Logic (
- Lecture 16 [PDF], Oct 25 (Thu): Hoare Logic (
HoareLogic.v). Homework 8:
- Lecture 17 [PDF], Oct 30 (Tue): Small-step operational semantics (
- Lecture 18 [PDF], Nov 1 (Thu): Small-step operational semantics (
Smallstep.v). Homework 9:
- Lecture 19 [PDF], Nov 6 (Tue): Type systems (
- Lecture 20 [PDF], Nov 8 (Thu): Simply typed lambda calculus (STLC) (
Stlc.v). Homework 10:
- Lecture 21 [PDF], Nov 13 (Tue): Properties of the STLC (
- Lecture 22, Nov 15 (Thu): Project [PDF](. Homework 11:
- Lecture 23, Nov 20 (Tue): Project [PDF]
- Lecture 24, Nov 22 (Thu): (No class. Thanksgiving recess.)
- Lecture 25, Nov 27 (Tue): Presentations Homework 12:
- Lecture 26, Nov 29 (Thu): Presentations Homework 13: Project.
- Lecture 27, Dec 4 (Tue): Presentations
- Lecture 28, Dec 6 (Thu): Presentations
- Lecture 29, Dec 11 (Tue): Presentations
- Lecture 30, Dec 13 (Thu): Presentations, Course review.
- Room: M-1-0208
- Schedule: Tuesdays & Thursdays 12:30noon to 1:45pm
- Office hours: Tuesdays & Thursdays 2:30pm to 4:00pm
- Email: Tiago.Cogumbreiro@umb.edu
- Office: S-3-088
- Phone #: 617.287.6479
- Software Foundations. Volume 1 and 2. Benjamin Pierce et al. 2018.
What makes a functional language functional? What makes an imperative language imperative? Can we prove that all program executions are absent of undefined behavior? Can we prove that a compiler preserves the intent of the source program?
This course will introduce the formalization of the semantics of a programming language. We will use a rigorous mathematical formalism to describe a computation model (eg, a programming language) and its properties (eg, avoiding undefined behavior).
The objective of this course is to specify a functional and imperative language with pre- and post-conditions. We will use the Coq Proof Assistant to specify the language, and prove the properties of the the programming language we are specifying.
One of the underlying goals of the class is to appeal to practitioners (software engineers) as well as researcher. To this end, we will learn a lightweight testing technique, called property testing, that leverages properties of a computation model (eg, a data structure or a component) to improve the quality of our software.
- basic concepts of logic
- computer-assisted theorem proving (Coq)
- functional programming
- logic programming
- operational semantics
- static type systems
- Hoare logic
The course is taught “from the ground up,” so it does not assume a specific background in logic or programming. However, familiarity with functional programming and rigorous mathematical proofs is advantageous.
If you are unsure about meeting the requirements for this course, I recommend
doing the Coq exercises in the
Basics.v chapter of the Software Foundations
book, Volume 1.
Course work and grades
- Homework: 75%
- Presentation: 15%
- Participation: 10%
Students are expected to have access to CoqIDE 8.7.2.
Homework assignments consist of Coq programs that will be submitted to the instructor unless stated otherwise.
Attendance is required. All students are responsible for knowing everything that is covered during class meetings, including announcements. If you must be absent from a class meeting, make arrangements with another student to find out what you missed.
No late homework will be accepted.
Any homework may be revised and resubmitted once, up to one week after the original deadline. (If you didn’t submit on time, your original score will be 0.) The grade for that homework will be the average of the two submissions.
All homework will be weighted equally. Your lowest homework score will be dropped.
You may not collaborate with anyone else on any homework. Each homework represents your own, individual work.
It is acceptable to discuss the concept in general terms, but unacceptable to discuss specific solutions to any homework assignment.
On auto grading
Grading of Coq exercises is done automatically. Thus, in order for a homework to
be graded, it needs to be accepted by Coq. Use
Admitted to allow incomplete
proofs and definitions.
Every student must present one of two:
- One chapter of the textbook to the class (60 minutes). The instructor will still publish the slides of that chapter.
- One paper on the subject of formalizing the semantics of a programming language or system (20 minutes presentation). The student may suggest a paper (or request one suggestion).
- 60% instructor’s grade
- 25% peers’ grade
- 15% grading peer participation (submit at least 10 sheets)
The participation component in the evaluation corresponds to student participation in classes and in the online forum. Participation does not just mean just answering questions correctly. Discussion and questions, either posed online or in class, are encouraged and counted toward participation.
Each reasonable student intervention (in the class or online) yields 1 point. If the student reaches 14 points, they are graded the full mark of participation.
This class seeks ways to become a working and evolving model of inclusion and
universal design for all participants. Individuals with disabilities of
any kind (including learning disabilities, ADHD, depression, health
conditions), who require instructional, curricular, or test
accommodations are responsible for make such needs known to the instructor as
early as possible. Every effort will be made to accommodate students in a
timely and confidential manner. Individuals who request accommodations must be
registered with the Ross Center for Disability Services, which authorizes
accommodations for students with disabilities. If applicable, students may
obtain adaptation recommendations from the Ross Center for Disability Services,
www.rosscenter.umb.edu. The student must
present these recommendations and discuss them with each professor within a
reasonable period, preferably by the end of Drop/Add period.
Students are required to adhere to the University Policy on Academic Standards
and Cheating, to the University Statement on Plagiarism and the Documentation of
Written Work, and to the Code of Student Conduct as delineated in the catalog of
Undergraduate Programs, pp. 44-45, and 48-52. The Code is available online at: