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.

1. Clone the Repository:

   You can make a local copy of the repository by cloning it:

   git clone https://github.com/SyntakticSugar/proofgrams.git
   cd proofgrams

   Or simply downloading the repository.

2. 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.

3. 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.

4. 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.