COL832 Proofs and Types

Credits: 3 (3-0-0)

Prerequisites: COL226, COL352

Description

Syntax and semantic foundations: Ranked algebras, homomorphisms, initial algebras, congruences. First-order logic review: Soundness, completeness, compactness. Herbrand models and Herbrand’s theorem, Horn-clauses and resolution. Natural deduction and the Sequent calculus. Normalization and cut elimination. Lambda-calculus and Combinatory Logic: syntax and operational semantics (beta-eta equivalence), confluence and Church-Rosser property. Introduction to Type theory: The simply-typed lambda-calculus, Intuitionistic type theory. Curry-Howard correspondence. Polymorphism, algorithms for polymorphic type inference, Girard and Reynolds’ System F. Applications: type-systems for programming languages; modules and functors; theorem proving, executable specifications.

Prerequisite Tree

flowchart TD
COL832-239[COL832]
COL352-239 --> COL202-239[COL202]
COL832-239 --> COL226-239[COL226]
COL226-239 --> COL106-239[COL106]
COL106-239 --> COL100-239[COL100]
COL832-239 --> COL352-239[COL352]

classDef empty height:17px, fill:transparent, stroke:transparent;
classDef trueEmpty height:0px, width:0px;