[The talk will take place in amphi A, 3rd & 4th floors, at the other end of the corridor w.r.t. amphi B, if you know where this is.]

Martin-Löf Type Theory is a sweet spot in the correspondence between proofs and programs: dependent types and inductive types allow for remarkably expressive program specifications, and adding a universe hierarchy results in a theory with enough logical power to encode most day-to-day mathematical constructions -- an all-around foundational tool for proof assistants.

However the inductive equality supplied by MLTT is not quite suitable for mathematical reasoning, because it encodes program equality ("intensionality") instead of behavioral equality ("extensionality"). This has unfortunate consequences: one cannot prove that the functions n -> n+2 and n -> 2+n are equal, there is no way to quotient a type by an equivalence relation, etc.

Observational Type Theory was designed to remediate to this very state of affairs. A complete implementation of OTT would feature these desired extensionality principles, while preserving the philosophy of the correspondence between proofs and programs and the nice properties that come with it (normalization, canonicity, decidability of typing...).

In my talk, after some preliminary exposition about dependent types, I will introduce TT^obs, a conceptually simple extension of Martin-Löf Type Theory that turns it into a fully observational type theory. I will illustrate with some use cases, and if time allows I will go over its meta-theory.