From fdcad8922da84d44f0c643d62117f85cbe9a518d Mon Sep 17 00:00:00 2001 From: Kevin Sullivan Date: Wed, 27 Dec 2023 15:28:42 -0500 Subject: [PATCH] Add section for Kevin Sullivan UVa ugrad course in discrete math --- data/courses.yaml | 57 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/data/courses.yaml b/data/courses.yaml index eb126df960..3bbdb63ac2 100644 --- a/data/courses.yaml +++ b/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: sullivan@virginia.edu + 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