Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add BU courses to course list #581

Merged
merged 1 commit into from
Jan 20, 2025
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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.
Loading