Add section for Kevin Sullivan UVa ugrad course in discrete math

data/courses.yaml

@@ -18,6 +18,24 @@
 # 
 # This list is not ordered. Add new entries wherever you want.
 
+# Entries in this file should have the following fields:
+# 
+# `name`: the title of the course
+# `instructor`: the name of the person or people who taught the course
+# `institution`: the name of the institution at which the course was taught
+# `year`: the most recent year the course was taught
+# `lean_version`: 3 or 4, the Lean version of the most recent iteration of the course
+# `summary`: a description of what was covered and done in the course
+# `tags`: a list of tags (see below)
+# `website` (optional): the course's home page
+# `material` (optional): a link to a textbook, course notes, etc
+# `repo` (optional): a link to the course's project repository, e.g. on GitHub
+# `experiences` (optional): a reflection about how the course went, things that could be done differently, etc
+# `language` (optional): if the instruction language was not English, what language was it?
+#
+# Please use tags that are shown on the website. In particular, each entry should have
+# a general subject (`mathematics`, `logic`, `computer science`).
+
 - name: Introduction to formal verification of mathematics
   instructor: Philip Matchett Wood
   institution: Harvard University
@@ -56,6 +74,45 @@
   summary: >
     The goal of the course is to teach the basics of Lean to first year undergraduate students in a double major program in mathematics and computer science.
   year: 2023
+- name: Discrete Mathematics for Computer Science and Engineering
+  instructor: Kevin Sullivan
+  contact: [email protected]
+  institution: University of Virginia, Dept. of Computer Science
+  website: https://computingfoundations.org
+  environment: Coursework is supported by a VS-Code+Docker remote container.
+  lean_version: 4
+  tags: ['mathematics','computer science', 'programming-first', 'discrete']
+  summary: >
+    The course is intended to replace the broad, shallow, paper-and-pencil, usually
+    set-theory based courses in discrete mathematics, almost universally taught to 
+    early undergraduate students. Distinguishing features of this course include the
+    folowing: (1) based on Lean, it offers a type-theory-unified, rigorously formal 
+    introduction to the topics typically covered in undergraduate discrete mathematics
+    as well as providing a strong foundation in elementary type theory and functional
+    programming. (2) Based on numerous years of experience, the course materials in Lean 
+    use a carefully selected subset of Lean features, to keep the focus on the concepts
+    and their formal expression using standard mathematical notations. (3) This course 
+    is based on the hypothesis that engaging CS students' interests in advancing their 
+    understanding not of logic and abstract mathematics but of computation will lead to
+    better learning outcomes and student satisfaction. The trick it employs is to first 
+    work up to programming with product, sum, and *function-to-Empty* types, and encoding 
+    logical propositions and proofs as function types and implementations; and only when
+    students have learned this programming skill do we cross the Curry-Howard bridge to 
+    formal logic, in Prop. With these computing and logical foundations laid, the course 
+    then presents topics typically covered in discrete mathematics courses, including
+    induction axioms, their use in constructing both recursive functions and proofs by 
+    induction, and well-ordered relations as capstone idea. (The last bits of the course
+    remain in the publication pipeline and will appear online shortly).
+experiences: >
+    This course has evolved over a period of about five years, through repeated annual
+    offerings in the Department of Computer Science at the University of Virginia. In 
+    the Fall of 2023 it was taught to *160 UVa undergraduate students*, as their second 
+    course in our BA and BS programs Computer Science. In comparison with its previous 
+    offerings, this year's restructuring to employ a programming-first on-ramp strategy
+    appears to have worked very well, both in learning outcomes and student satisfaction. 
+    We have not yet conducted IRB-approved studies of these parameters. The course will
+    be offered again in the Fall of 2024.
+  year: 2023,
 - name: Some high-school mathematics in Lean
   instructor: Peter Pfaffelhuber
   institution: University of Freiburg, Germany