CSC 579 Spring 2026 (R 9:40am to 10:55 Douglass 307)
The language of intelligence is logic. The course teaches proof systems, with a focus on Coq. You will learn to use Coq to formalize logic, which is the fundamental language of rational thought and problem-solving, and construct sound and verifiable proofs. A similar system, Lean 4, was used by generative AI, Alpha Proof, to solve Olympiad-level math problems. By learning the fundamentals of modern proof systems, you acquire a complete foundation for logical thinking and the knowledge and skill to use or build automated reasoning systems.
Pre-requisites: Students enrolling in the course are expected to have advanced knowledge in either programming languages (CSC 253, 254 or 255), math, or logic.
Syllabus
The Need for Training Thought: The Values of Thought. Tendencies Needing Constant Regulation. Regulation Transforms Inference into Proof.
Type Systems. Operational Semantics. Progress. Type Preservation. Type Soundness.
Functional Programming in Coq: Data and Functions. Proof by Simplification, Rewriting and Case Analysis.
Proof by Induction. Proofs Within Proofs. Formal vs. Informal Proof.
Logic in Coq. Logical Connectives: Conjunction, Disjunction, Falsehood and Negation, Truth, Logical Equivalence, Logical Equivalence, Existential Quantification. Programming with Propositions. Applying Theorems to Arguments. Coq vs. Set Theory: Functional Extensionality, Propositions vs. Booleans, Classical vs. Constructive Logic.
Inductively Defined Propositions. Induction Principles for Propositions. Induction Over an Inductively Defined Set and an Inductively Defined Proposition.
The Curry-Howard Correspondence. Natural Deduction. Typed Lambda Calculus. Proof Scripts. Quantifiers, Implications, Functions. Logical Connectives as Inductive Types.
Anonymous inputs were collected by the university before the final exam. 17 out of 24 students (71%) submitted the evaluation.The overall Instructor Rating is 4.53, and the overall Course Rating 4.44.
Two anonymous comments:
Professor Ding is a great professor and a strong proponent of Rust. Taking his class has introduced me to many benefits of Rust and broadened my horizon on collaborative programming, software design, and software testing. I believe acquiring these knowledge is beneficial for me and my teammates (it goes both ways) on the long run.
The final DVCS group project workload is very imbalanced and hard to control. Some group members even disappeared during the last half of the project.
This is a course required for the Bachelor of Science degree in Computer Science at the University of Rochester. A graduate must understand in depth the underlying physical reality which the virtual world including AI is built and depends on, i.e. the fundamentals of modern computer organization, including software and hardware interfaces, assembly language and C programming, memory hierarchy and program optimization, parallelism and operating systems. The textbooks are listed here.
There are two aspects for such a course in an elite research department like mine. First, the teaching focuses on fundamentals and goes in depth, which sets a high standard but this requirement is necessary for students to learn advanced subject courses later. Second, the material is updated often and part of it even experimental. In prior semesters, my colleagues Prof. John Criswell has emphasized on assembly and operating systems, Prof. Yuhao Zhu on gates and circuits, and Prof. Sree Pai on automatic (bit operation) correctness checking. My main change is the ISA.
RISC-V Instead of x86
Instruction Set Architecture (ISA) is essential in a BS CS degree and must be learned in this course which may be most hated material by a good number of students especially who have no prior knowledge of computer hardware. In my ancient PKU years, I learned Zilog Z80 (a microcontroller) and taught MIPS (classic RISC) and x86 (Intel/AMD) last time in this course in 2012. For the 2024 course, I evaluated Arm (Apple silicons) and the newest RISC-V. RISC-V is “open-source hardware” which means free for anyone to use. The course has the room to teach just one ISA; otherwise students will rebel.
I had a year to prepare for the course and tested this idea first before deciding on this significant change — This year’s students were the first (in Rochester) to learn RISC-V.
My NSF project with RIT has synthesized a RISC-V processor (papers here and here). I consulted my RIT collaborators who told me “x86 is too complex”, Arm is better but has “a lot of corner cases”, and for RISC-V, “I like it enough.” I learned about RISC-V over the years from computer architects to know the ISA is a good design, e.g., the first time in ASPLOS PC in 2019, but the RIT feedback made me think that the ISA is practical and learnable. The next question is whether it is teachable in a required undergrad class.
I purchased five or six single-board computers in both Arm and RISC-V and have them installed. Department staff Ian Ward installed Linux on Lichee-Pi 4A which has a quad-core processor, a GPU, and 8GB RAM for $130. The Arm processor (Raspberry Pi 4A) is weaker and does not run Linux.
My graduate TA Yifan Zhu (SchrodingerZhu on GitHub) installed the complete tool chain to compile and run RISC-V programs (in QEMU) on undergrad server (Intel) machines.
I found the 2024 textbook on RISC-V as recommended by the RISC-V foundation. The book reads well and covers the core knowledge: data representation, binary file and assembly, registers, data movement and control flow, application binary interface (ABI), all in 100 pages.
Here is the result. I summerized four changes in the following question (I created) in the Course Evaluation. Here are the question and the 15 responses:
RISC-V is newer and better designed, first with a core and then a series of extensions. The book covers RV32I, the core ISA. It is challenging to learn but learnable, unlike x86 which is too unwieldy, but it is 100 pages of material. Many students read the book and learned. They crossed a threshold of knowing the complete core, which they cannot do from learning x86.
Reading Books instead of Studying for Exams
At last semester’s CS Undergrad Town Hall where most CS faculty sat to listen to students’ feedback. One is that the department changes instructors of a course, and the exams are completely different from past years. I responded that a course teaches a subject, not a subject taught in a particular way and definitely not just exams. Exams are not the goal of learning or teaching, they are the feedback for both students and their teacher.
For this course, Prof. Zhu has made available past exams, problem sets, and their solutions (which I linked to in my course page). One can learn by studying these but shouldn’t use them as the primary source. Instead, students should learn by reading the textbooks. An important use of my lectures is to motivate students to read, show organization so they have mental map going in, and explain tricky/difficult examples and parts. When I find students don’t read textbooks, I use the lecture to read the book with them. My goal is for students to read the book and read it multiple times. The RISC-V book has the full content, updated, and readily accessible online.
The next and last 25 pages of the RISC-V book covers system-level programming (not covered in the course) but reading them (if/when they need to) would be a breeze once a student reads the first 100 pages.
In-person instead of Off-line Grading
The class has 64 students. 89 students registered, 21 dropped, and 5 withdrawn. Multiple students told me that they liked the course but felt not sufficiently prepared and will take the course next semester.
I myself cannot give every student the time and attention they deserve. There is no self deception/illusion/delusion here. I hired seven undergrad TAs. To maintain consistency, they must be primarily responsible for grading. The last thing I should do is to cherry pick and over rule their work.
There are two challenges to project grading. Computer organization is standard material, and the solutions of pass assignments and projects are abundant on the Web. One may say that students who choose to copy solutions waste their time and learning opportunity so who cares, but these are young minds that are often immature, so I do care to at least make it hard for them to fall. Using RISC-V reduces the severity of the problem.
The new problem is ChatGPT and other AI tools which could program in RISC-V. My TAs solved the problem with in-person grading. Students are divided into four groups and come to a TA session each week. They were required to explain their solution. In home work, students wrote and ran RISC-V programs using an emulator. At grading time, TAs set up an actual RISC-V machine so students saw their programs running native and for real.
In one project, the binary bomb, Yifan created the setup that students had practice bombs but when they came to grading, they were given a new bomb to defuse in 15 minutes.
The Result
The end test of a course is how well students have learned after a full semester. There were a total of 869 points across all assignments and exams. The final score is the ratio of student’s points over this total number. Here is the distribution:
50 students scored 80% and above, and all but 7 students were 70% or higher. I had the most fun problem which was deciding between a B+ and an A- for the 8 students who were between 88.94% and 90.2%. This is much better than what I expected from such a difficult course. I remember telling my colleagues who were duly impressed by my students. I am still immensely proud of what they have done.
Parting Thoughts
“One might as well say he has sold when no one has bought as to say he has taught when no one has learned.” — John Dewey in Logic The Theory of Inquiry
The course has its problems that can and should be improved. One that’s difficult to fix is that students learned RISC-V and then read the CS:APP textbook which uses x86. Right now, they have to map the book examples to RISC-V themselves. The evaluation score is 3.53 for overall instructor and 3.4 for the course, lower than my typical scores (here and here). Seven respondents gave the highest rating, and two the lowest. I appreciate students wrote in the evaluation and in public (here). What’s online is anecdotally true but not complete or comprehensive. My blog is partly to tell the part of the extensive learning that computer science students have accomplished in one of their courses in their four-year journey at Rochester.
Acknowledgements: including but not limited to CS staff Ian Ward and Dave Costello; my TAs Yifan, Boyang, Leo, Jacob, Kestor, Yekai, Zack, and Zachary; and my colleague John Criswell (for suggesting the xargs project).
CSC 253/453 Collaborative Programming and Software Design
Fall 2023 Student Evaluation
Anonymous inputs were collected by the university before the final exam. 9 out of 25 students (36%) submitted the evaluation.
The overall Instructor Rating is 4.89, same as the overall Course Rating.
All nine students gave highest or next highest score to the questions:
Teaching Skills
Rapport with Students
Academic Honesty
Value of the Course
Some of the comments include:
I particularly relished the final big project, which was both challenging and immensely rewarding. Working collaboratively with my team was a highlight, fostering a sense of friendship and shared purpose that made the learning process especially enjoyable. However, I do wish we had more time allocated for this final project. The complexity and scale of the project made it engaging, and having additional time would have allowed us to delve deeper into the coding challenges and explore more creative solutions as a team.
hard course
This course has a strong emphasis on collaboration, which is very helpful for my future work. Project is a little bit hard and it takes a lot of time.
Chen Ding, Professor of Computer Science WFs 3:25pm to 4:40 Gavett 206
CSC 252 teaches the fundamentals of modern computer organization, including software and hardware interfaces, assembly languages and C, memory hierarchy and program optimization, data parallelism and GPUs. It shows the underlying physical reality which the virtual world including AI is built and depends on.
Logic in Coq. Logical Connectives: Conjunction, Disjunction, Falsehood and Negation, Truth, Logical Equivalence, Logical Equivalence, Existential Quantification. Programming with Propositions. Applying Theorems to Arguments. Coq vs. Set Theory: Functional Extensionality, Propositions vs. Booleans, Classical vs. Constructive Logic.
Inductively Defined Propositions. Induction Principles for Propositions. Induction Over an Inductively Defined Set and an Inductively Defined Proposition.
The Curry-Howard Correspondence. Natural Deduction. Typed Lambda Calculus. Proof Scripts. Quantifiers, Implications, Functions. Logical Connectives as Inductive Types.
CSC 253/453 and TCS 453 Collaborative Programming and Software Design
Modern software is complex and more than a single person can fully comprehend. This course teaches collaborative programming which is multi-person construction of software where each person’s contribution is non-trivial and clearly defined and documented. The material to study includes design principles, safe and modular programming in modern programming languages, software teams and development processes, design patterns, and productivity tools. The assignments include collaborative programming and software design and development in teams. The primary programming language taught and used in the assignments is Rust. Students in CSC 453 have additional reading and requirements.
Prerequisites: CSC 172 or equivalent for CSC 253 and TCS 453. CSC 172 and CSC 252 or equivalent for CSC 453.
Fall 2020 Student Evaluation
Anonymous inputs were collected by the university before the final exam. 14 out of 33 students (44%) submitted the evaluation.
The overall Instructor Rating is 4.21 and Course Rating 4.00.
Among the individual questions, the highest are 4.79 (The instructor was willing to listen to student questions and/or opinions), 4.71 (The instructor demonstrated sincere respect for students), and two COVID related questions both are 4.54 (the instructor clearly articulated course expectations to students, and the instructor noticed when students did not understand course material and adjusted accordingly). The lowest are 3.71 (The exams/assignments were clearly worded) and 3.93 (The instructor used examples that helped with understanding the material).
Prerequisites: CSC 252 and CSC 254 are required for CSC 453 and recommended for CSC 253. CSC 161, CSC 172 or equivalent is required for CSC 253. Crosslisted: TCS 453 (same requirement as CSC 253)
Modern software is complex and more than a single person can fully comprehend. This course teaches the principles and techniques of writing modular and composable code and collaborating with others in software design. The topics include advanced concepts and techniques in modern programming languages, principles of modularity, software architecture, design patterns, software development processes, and other examples of software design. A significant portion of the assignment is a group project to develop a groupware system. Students enrolled in the class are expected to already have significant programming experience in some languages. The programming languages used in lectures are mainly Ruby, Haskell and Rust.
Teaching Staff and office hours: Prof. Chen Ding, Fridays 11am to 12pm in Wegmans Hall (WH) 3407, x51373. Wesley Smith, Tuesdays 11am to noon WH 2215. Michael Chavrimootoo, 10am to 11 WH 2215.
Policies for grading, attendance, and academic honesty (updated 8/18)
The workload will be heavy. Be sure to read instructions for each assignment and exam carefully, start the assignment early, know where/when to seek help, and work with peers. (read more)
Grading:
3 exams, roughly 30%
attendance and written homework, about 10%
assignments and projects, approximately 60%
Assignments are typically handed out before Monday and due Friday midnight.
Preparation (before first class):
“No Silver Bullet — Essence and Accidents of Software Engineering” is a classic paper on software engineering written by Turing Award winner Fred Brooks in 1986. Read the paper (available here) pages 3 to 5 on the “essential difficulties” of software development and skim the rest of the paper.
“A former member of the SD10 Panel on Computing in Support of Battle Management explains why he believes the ‘star wars’ effort will not achieve its stated goals.” Read the paper (available here if accessed inside the UR network) pages 2 to 4 the section titled “Why software is unreliable.” Which of the “essential difficulties” was Parnas discussing?
You can read this and other articles by borrowing the book “Software Fundamentals” from the textbook reserve for CSC 253/453 at the Carlson Library. The lease is two hours.
Further material will be distributed through the Blackboard web site for students who have registered. Contact the instructor if you have problem accessing the site.
Textbooks (online access at learn.rochester.edu > CSC 253 > Reserves > Materials on Reserve in the Library):
Object-oriented Software Engineering
Author: Schach, Stephen R.
Imprint: New York : McGraw-Hill, c2008.
Available at school book store. On Reserve at: Carlson Library Reserve Desk 2nd Floor
Fundamentals of software engineering
Author: Ghezzi, Carlo.
Imprint: Upper Saddle River, N.J. : Prentice Hall, c2003.
On Reserve at: Carlson Library Reserve Desk 2nd Floor
Call Number: QA76.758 .G47 2003
Structure and Interpretation of Computer Programs
Authors: Hal Abelson and Jerry Sussman and Julie Sussman
Imprint: MIT Press, 1984
Policies for CSC 2/453
The workload will be heavy. Be sure to read instructions for each assignment and exam carefully, start the assignment early, know where/when to seek help, and work with peers.
Grades will be released periodically to Blackboard, the University’s on-line course management system.
Attendance and Class Participation
Class attendance is mandatory. Please arrive on time. I expect to start at 3:25 sharp, and late arrivals disturb the people who are already there. You are encouraged to ask or answer questions in class. I may call on you just to know what you think. As a general rule, if there’s something you don’t understand, make me stop and explain it. Other people sitting around you probably didn’t understand it either, but don’t have the nerve to say so. Likewise, let me know if I’m belaboring something that you already know.
For most lectures, I will assign reading before and after. Reading is mandatory It includes all lecture slides released to Blackboard, and textbook chapters/sections listed on the first slide of each lecture. The exams include topics covered in class and in the required reading.
Late Submission Policy
A student may have a total of two extra days in all individual assignments. They can be used as either a one-day extension for two assignments, or a two-day extension for one assignment. Additional extensions are given to students who attend research/education conferences. The length of extension is roughly equal to the days of the conference plus travel. A student must inform the TA about the extension before the due time. No other late submission is permitted.
Academic Honesty
Student conduct in CSC 2/453 is governed by the College Academic Honesty Policy, the Undergraduate Laboratory Policies of the Computer Science Department, and the University’s Acceptable Use Policy for Information Technology. I worked in the academic honesty education committee in the past. I believe in these policies strongly, and will enforce them aggressively.
The following are details specific to CSC 2/453.
Exams in CSC 2/453 must be strictly individual work.
Collaboration on programming assignments among team members is of course expected. Collaboration on assignments across teams is encouraged at the level of ideas. Feel free to ask each other questions, brainstorm on algorithms, or work together at a whiteboard. You may not claim work as your own, however, unless you transform the ideas into substance by yourself. Among other things, this means that you must leave any brainstorming sessions with no written or electronic notes—only what you carry in your head.
If you use the work of others (e.g., you download a function from the web at the last minute so that you can get the rest of your project working), then (1) either you must have the author’s explicit permission or the material must be publicly available, and (2) you must label what you copied, clearly and prominently, when you hand it in. You will of course get points only for the parts of your assignment that you wrote yourself.
To minimize the temptation to steal code, all students are expected to protect any directories or on-line repositories in which they do their work.
For purposes of this class, academic dishonesty is defined as
Any attempt to pass off work on an exam or quiz that didn’t come straight out of your own head.
Any collaboration on assignments beyond the sharing of ideas, unless the collaborating parties clearly and prominently explain exactly who did what, at turn-in time.
Any activity that has the effect of significantly impairing the ability of another student to learn. Examples here might include destroying the work of others, interfering with their access to resources, or deliberately providing them with misleading information.
Note that grades in CSC 2/453 are assigned on the basis of individual merit rather than relative standing, so there is no benefit—even a dishonest one—to be gained by sabotaging the work of others.
I work under the assumption that students are honest. I will not go looking for exceptions. If I discover one, however, I will come down on it very hard. Over the past few years, the department has submitted violation cases to the College Board on Academic Honesty. Many resulted in major penalties for the students involved.
Prerequisites: CSC 252 and CSC 254 are required for CSC 453 and recommended for CSC 253. Familiarity with a dynamic programming language such as Python is required for CSC 253. Crosslisted: TCS 453 (same requirement as CSC 253)
This course studies dynamically-typed programming languages and modular software development. Topics include principles and practice of modular design, functional and object-oriented programming techniques, software engineering concepts, software correctness and reliability, programming tools, and design examples. Ruby is used as the main instruction language. The lessons complement those in traditional compilers and programming languages courses, which focus mainly on statically-typed languages and individual algorithms rather than system design. A significant portion of the assignment is a group project.
Teaching Staff and office hours: Prof. Chen Ding, Fridays 11am to 12pm in Wegmans Hall 3407, x51373. Yu Feng, 5pm to 6pm, Mondays and Wednesdays, Wegmans Hall 3407. Patrick Ferner, 2:30pm to 3:30pm, Tuesdays, Wegmans 2215 (updated 9/11).
Assignments are typically handed out on Wednesday and due the following Tuesday midnight.
Preparation (before first class):
“No Silver Bullet — Essence and Accidents of Software Engineering” is a classic paper on software engineering written by Turing Award winner Fred Brooks in 1986. Read the paper (available here if accessed inside the UR network) pages 3 to 5 on the “essential difficulties” of software development and skim the rest of the paper.
“A former member of the SD10 Panel on Computing in Support of Battle Management explains why he believes the ‘star wars’ effort will not achieve its stated goals.” Read the paper (available here if accessed inside the UR network) pages 2 to 4 the section titled “Why software is unreliable.” Which of the “essential difficulties” was Parnas discussing?
More background of this debate, detailed rationales and an illuminating discussion of the ethical issues can be found in another article of Parnas: “SDI: A Violation of Professional Responsibility”. The article does not seem to have a free version online, but you can read it by borrowing the book “Software Fundamentals” (included as Chapter 27) from the textbook reserve for CSC 253/453 at the Carlson Library. The lease is two hours.
Further material will be distributed through the Blackboard web site for students who have registered. Contact the instructor if you have problem accessing the site.
Textbooks (online access at learn.rochester.edu > CSC 253 > Reserves > Materials on Reserve in the Library):
Object-oriented Software Engineering
Author: Schach, Stephen R.
Imprint: New York : McGraw-Hill, c2008.
Available at school book store. On Reserve at: Carlson Library Reserve Desk 2nd Floor
The workload will be heavy. Be sure to read instructions for each assignment and exam carefully, start the assignment early, know where/when to seek help, and work with peers.
Grades will be released periodically to Blackboard, the University’s on-line course management system.
Attendance and Class Participation
Class attendance is mandatory. Please arrive on time. I expect to start at 3:25 sharp, and late arrivals disturb the folks who are already there. You are encourage to ask or answer questions in class. I may call on you just to know what you think. As a general rule, if there’s something you don’t understand, make me stop and explain it. There are probably a dozen people sitting around you who didn’t understand it either, but don’t have the nerve to say so. Likewise, if I’m belaboring something that everyone understands, prod me to move on.
I will assign reading before and after lectures. Reading is mandatory It includes all lecture slides released to Blackboard, and textbook chapters/sections listed on the first slide of each lecture. Keep in mind that the exams include topics covered in class and in the required reading.
Late Submission Policy
A student may have a total of two extra days in all assignments. They can be used as either a one-day extension for two assignments, or a two-day extension for one assignment. A student must inform the TA about the extension before the due time. No other late submission is permitted.
Exams in CSC 2/453 must be strictly individual work.
Collaboration on programming assignments among team members is of course expected. Collaboration on assignments acrossteams is encouraged at the level of ideas. Feel free to ask each other questions, brainstorm on algorithms, or work together at a whiteboard. You may not claim work as your own, however, unless you transform the ideas into substance by yourself. Among other things, this means that you must leave any brainstorming sessions with no written or electronic notes—only what you carry in your head.
If you use the work of others (e.g., you download a function from the web at the last minute so that you can get the rest of your project working), then (1) either you must have the author’s explicit permission or the material must be publicly available, and (2) you must label what you copied, clearly and prominently, when you hand it in. You will of course get points only for the parts of your assignment that you wrote yourself.
To minimize the temptation to steal code, all students are expected to protect any directories or on-line repositories in which they do their work.
For purposes of this class, academic dishonesty is defined as
Any attempt to pass off work on an exam or quiz that didn’t come straight out of your own head.
Any collaboration on assignments beyond the sharing of ideas, unless the collaborating parties clearly and prominently explain exactly who did what, at turn-in time.
Any activity that has the effect of significantly impairing the ability of another student to learn. Examples here might include destroying the work of others, interfering with their access to resources, or deliberately providing them with misleading information.
Note that grades in CSC 2/453 are assigned on the basis of individual merit rather than relative standing, so there is no benefit—even a dishonest one—to be gained by sabotaging the work of others.
I work under the assumption that students are honest. I will not go looking for exceptions. If I discover one, however, I will come down on it very hard. Over the past few years, I have submitted about a dozen cases to the College Board on Academic Honesty. All resulted in major penalties for the students involved.