Skip to content

Commit

Permalink
add BU courses to course list (#581)
Browse files Browse the repository at this point in the history
  • Loading branch information
robertylewis authored Jan 20, 2025
1 parent 261b48a commit 4c89f57
Showing 1 changed file with 29 additions and 1 deletion.
30 changes: 29 additions & 1 deletion data/courses.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -582,4 +582,32 @@
(2) partially ordered sets, complete lattices, pre/pos/fixpoints, Knaster-Tarski theorem
(3) Kleene fixpoint theorem, induction and co-induction
(4) concatenating lists, reversing lists, sorting lists (formally verify mergesort)
- name: Combinatoric Structures
instructor: Assaf Kfoury
institution: Boston University
material: https://hrmacbeth.github.io/math2001/
tags: ['computer science', 'beginner']
year: 2025
lean_version: 4
summary: >
This course will be taught in the Spring 2025 semester for the first time. It will cover topics in a standard discrete-math course at entry undergraduate level (freshman and sophomore in the US).
(The course name is therefore a bit of a misnomer, chosen in order to avoid a few turf issues at Boston University.)
The reference textbook is Heather Macbeth's "The Mechanics of Proof".
Most of the enrolled students are majoring in computer science, with the remaining few majoring in mathematics or computer engineering.
The course is intended to teach the rigor of mathematical proofs as well as various proof methods commonly encountered in the mathematical sciences.
Students are assigned weekly homework exercises which they have to solve in one of two ways, or in both ways:
(a) with Lean 4 and (b) in longhand "paper-and-pen" style.
Lean 4 will also be used as a functional programming language, in particular, in homework exercises involving the implementation of standard algorithms and some of their variations on finite graphs.
- name: Formal Methods for High-Assurance Software Engineering
instructor: Assaf Kfoury
institution: Boston University
website: https://sites.google.com/bu.edu/cs511-fall-2024/home
material: https://lean-lang.org/theorem_proving_in_lean4/
tags: ['computer science', 'mathematics']
year: 2025
lean_version: 4
summary: >
This course will be taught in the Fall 2025 semester, a slight modification of the same title taught in the Fall 2024 semester.
About half of the course will cover standard material of mathematical logic, with an emphasis on model theory, as taught in a first-year graduate course.
The course will be limited to graduate students in computer science and mathematics.
The material for the course will combine sections in the book "Theorem Proving in Lean 4" and the book "The Hitchhiker's Guide to Logical Verification", in addition to lecture notes by the instructor on model theory.

0 comments on commit 4c89f57

Please sign in to comment.