COL832: Difference between revisions
| [checked revision] | [checked revision] |
Prashantt492 (talk | contribs) Creating course page via bot |
Bot: wrap bare course codes in wikilinks |
||
| Line 4: | Line 4: | ||
| credits = 3 | | credits = 3 | ||
| credit_structure = 3-0-0 | | credit_structure = 3-0-0 | ||
| pre_requisites = COL226, COL352 | | pre_requisites = [[COL226]], [[COL352]] | ||
| overlaps = | | overlaps = | ||
}} | }} | ||
Latest revision as of 16:26, 14 April 2026
| COL832 | |
|---|---|
| proofs and Types | |
| Credits | 3 |
| Structure | 3-0-0 |
| Pre-requisites | COL226, COL352 |
| Overlaps | |
COL832 : proofs and Types
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.