This repository houses course materials for learning Logic, lambda calculus, and Lean. Including slides, lecture notes, and exercises.
- Propositional Logic: Basic grammar of logical connectives and natural deduction.
- First-Order Logic: Introduction to quantifiers, predicates, and more natural deductions.
- Un-typed Lambda Calculus: Write programs in Alonso Church's lambda calculus.
- Simply Typed Lambda Calculus: Adding typed structure to the lambda calculus. Write typing derivations to ensure programs are well-typed.
- Dependent Type Theory: Learn how simple type theory is extended to allow for a much more expressive language.
- Lean Theorem Prover: Instructions on how to get started with Lean, a proof assistant.
- Interactive Proofs: Writing and verifying proofs using Lean's type theory.
-
Clone the Repository:
You can make a local copy of the repository by cloning it:
git clone https://github.com/SyntakticSugar/proofgrams.git cd proofgramsOr simply downloading the repository.
-
Course Materials 📚 (Incomplete drafts)
- Lecture Slides: These are skeletal slides, to be filled during class.
- Lecture Notes: Detailed notes on logic, lambda calculus, and Lean.
- Tutorials: Practice problems to test your understanding.
- Projects: Larger assignments to apply your knowledge.
-
Getting Started with Lean:
To get a feel for how working in Lean, both of the introductory games Natural Number Game and A Lean Introduction to Logic are particularly relevant to this course. You can follow this Quickstart Guide to begin working with Lean on your personal computer.
-
Recommended Resources: 🔗
My course materials were developed while studying these excellent resources:
- Theorem Proving in Lean 4 by Avigad, de Moura, Kong, and Ullrich.
- Programming Language Foundations in Agda by Philip Wadler.
- Verified Functional Programming in Agda by Aaron Stump.
- Type Theory and Functional Programming by Simon Thompson.
- Stanford Encyclopaedia of Philosophy.