https://wiki.devclub.in/index.php?action=history&feed=atom&title=COL832 2026-04-09T07:50:04Z Revision history for this page on the wiki MediaWiki 1.45.1 https://wiki.devclub.in/index.php?title=COL832&diff=625&oldid=prev 2026-03-04T10:00:39Z

<p>Creating course page via bot</p> <p><b>New page</b></p><div>{{Infobox Course<br /> | code = COL832<br /> | name = proofs and Types<br /> | credits = 3<br /> | credit_structure = 3-0-0<br /> | pre_requisites = COL226, COL352<br /> | overlaps = <br /> }}<br /> <br /> == COL832 : proofs and Types ==<br /> Syntax and semantic foundations: Ranked algebras, homomorphisms, initial algebras, congruences. First-order logic review: Soundness, completeness, compactness. Herbrand models and Herbrand&#039;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&#039; System F. Applications: type-systems for programming languages; modules and functors; theorem proving, executable specifications.</div>

Prashantt492