Skip to content

Commit

Permalink
Add Stanford's CS 99 to course list (#595)
Browse files Browse the repository at this point in the history
We have a new course this year
  • Loading branch information
lenianiva authored Feb 19, 2025
1 parent 5875307 commit 72cd7d7
Showing 1 changed file with 17 additions and 0 deletions.
17 changes: 17 additions & 0 deletions data/courses.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -624,3 +624,20 @@
This course really works well, and it will probably continue for a long time.
The idea to use controlled natural language tactics seems a lot more efficient than the native syntax to ensure students improve at pen and paper proofs.
year: 2025
- name: Functional Programming and Theorem Proving in Lean 4
instructor: Leni Aniva, Abdalrhman Mohamed
institution: Stanford University
website: https://web.stanford.edu/class/cs99/
tags: ['English', 'computer science', 'mathematics', 'functional programming', 'theorem proving', 'metaprogramming']
year: 2025
lean_version: 4
summary: >
This course gives a systematic introduction to Lean 4, first as a functional
programming language, and then a theorem prover. We explain the type
theoretic foundations of Lean and show examples of theorem proving and
tactics. The last part of the course covers Lean's compiler and
metaprogramming system. The course is intended for both mathematicians and
computer scientists. The contents covered include: Type Polymorphism,
Monads, CIC, Subtyping, Tactics, Logic, Sets, Computability, Termination,
Metaprogramming, Macros, Elaboration, Type Unification, and relevant works
in other proof assistants.

0 comments on commit 72cd7d7

Please sign in to comment.