Under construction. This area is a framework being built: most courses have no teaching material yet, and things may change or break. Private self-study. Not an official programme and not recognised by any ministry or school. No qualification, mark or document is issued, and “years 1 to 3” and “advanced” are names of study paths only.
E08 Type theory and formal verification
Years 1 to 3 pathE: Proposed extensionsplannedproposed, not in any programmeabout 120 h (planning estimate)
Planned: syllabus only, no teaching material yet. Nothing on this page can be studied; it describes what the course would cover.
In no programme. This is a proposed extension course; the owner has not approved it into a programme.
Proposed by the assistant to fill a gap in the owner's catalogue. It is in no programme until the owner approves it.
Why this course
Formal methods and proof assistants link logic to computer science; also supports the brief's "formal verification" evidence type.
Prerequisites
Concept-level units
Units follow the syllabus order, as a recommended sequence rather than a gate.
- Lambda calculus
- Simple types
- The Curry–Howard correspondence
- Dependent types first look
- Proving in an assistant (Lean or Coq)
- Verifying small programs
Assessable outcome
Write and check a formal proof and explain what the checker guarantees.
Assessment design
- topic exercises
- mixed problem sets
- unseen proof or derivation problems
- cumulative examination
cumulative; uses spaced retrieval
Resources
Every title here is candidate, unverified unless marked verified. Titles were suggested while planning. Nobody has checked that they exist, what they cost or how they are licensed.
- Software Foundations (free)
- Avigad · Logic and Proof (free)
- Pierce · Types and Programming Languages
Content record
- Version
- 0.0.0
- Review
- no review of any kind
- Provenance
- PROPOSED by the assistant on 30 Oct 2026 to fill gaps in the brief's catalogue; not in the owner's brief; needs the owner's approval and a curriculum reviewer
- Known issues
- Proposed course: not counted by any programme audit until the owner approves adding it to an elective pool.
- Type
- course
Bridges and laboratories
No bridge or laboratory is attached to this course yet.
You and this course
Reading your plan on this device…