This course of lectures is an introduction to logic and type theory as background material for formal methods.

- introducing transition system rules for a while programming language
- expanding to procedures and recursion (eager evaluation)
- syntax of LC, bound and free variables, currying, substitution
- beta reduction, lambda calculus rules
- church numerals, pairs, fixed points, while
- equivalence, eta reduction, normal forms
- Church-Rosser property

- introduction to propositional natural deduction
- truth tables, normal forms, satisfiability
- functions, relations, terms, satisfaction
- quantifiers and natural deduction inference
- states, assertions, invariants
- theories
- predicate transformers
- Hoare logic

- Zermelo-Fraenkel: ideas and axioms
- specification and first-order logic
- unions, products, equinumerousness
- function space, powerset, diagonal argument
- relations, reflexive transitive closure
- equivalences, partitions
- the axiom of choice and transfinite induction

- typed languages
- function types: simply typed lambda calculus
- product types and Currying
- natural numbers, recursive definitions including function valued (e.g. Ackermann functions)
- parametric types (poymorphism)
- inductive types
- dependent types
- propositions as types; integrated

- Ian chiswell and Wilfrid Hodges,
*Mathematical Logic* - Ebbinghaus, Flum and Thomas,
*Mathematical Logic*, Springer-Verlag. - David Gries,
*The science of programming* - Martin-Lof,
*Intutionist Type Theory.* - Hindley and Seldin
*Lambda-Calculus and Combinators: An Introduction*, Cambridge. - John Reynolds,
*Theories of programming languages.* - Halmos,
*Naive set theory*. -
*Homotopy Type Theory: Univalent Foundations of Mathematics*, Institute for Advanced Studies, Princeton 2013; available at http://homotopytypetheory.org/book/.

For the Type Theory segment, I recommend installing Idris.
Using Idris is pleasant, but installation can be painful. On Windows, I suggest using the binary on that page.
If you are using linux, you may find this answer
helpful (i.e., use `stack`

).

**Instructors:**Siddhartha Gadgil, Kamal Lodaya, T.V.H.Prathamesh, Anantha Padmanabha.**E-mail:**siddhartha.gadgil@gmail.com.**Timing:**Wednesday, Friday 9:30 am - 12:45 pm.**Lecture Venue:**LH-3, Department of Mathematics, IISc.-
**First Lecture:**Wednesday, July 31, 2019. **Google group:**TrainLogic

- Introduction and Set Theory (Wed, 31 Jul 2019).

- Partial and Total orders, due by Fri, 13 Sep 2019.
- Formulas for Sets, due by Tue, 20 Aug 2019.