[msp-interest] [MSP101] Emma Tye: Martin-Löf Type Theory (3pm Tue 20/10, LT619)

[Emma Tye]

Dear all,

We have another MSP101 seminar coming up. Hope to see you there!

Best wishes,
Emma

Date, time and place:
  Tuesday 20 October, 15:00, Livingstone Tower room LT619

Online attendance:
  https://www.youtube.com/@msp.strathclyde/streams

Speaker:
  Emma Tye (MSP)

Title:
  Martin-Löf Type Theory

Abstract:
  The simply-typed lambda calculus (STLC) gives us a nice Curry-Howard correspondence with propositional logic by treating the function arrow of STLC as implication. From this we can compute proofs as programs. But a natural question is then: what about predicate logics instead of propositional? Martin-Löf Type Theory (or Intuitionistic Type Theory) is a type theory based on predicate logic, with type constructions representing existentially quantified variables (Sigma) and universally quantified variables (Pi). We can also construct inductively defined families - W-types - as well-founded trees. Note that Martin-Löf's original paper was inconsistent due to having the type-in-type paradox, and that he later introduced a predicative version with universe hierarchies.
In this introduction, we assume knowledge of the STLC and natural-deduction-style sequents for introduction and elimination rules. We will go over the introduction and elimination of the Sigma-type, Pi-type and W-type, universe hierarchies, and equality reasoning.

MSP101 Feeds:
  Web: http://msp.cis.strath.ac.uk/msp101.html
  RSS: http://msp.cis.strath.ac.uk/msp101.rss
 iCal: http://msp.cis.strath.ac.uk/msp101.ics