Refinement Type Systems and Martin Lof Type Theory

Explore a comprehensive lecture on refinement type systems and their connection to Martin-Löf type theory. Delve into Paul André Melliès' recent work with Noam Zeilberger, examining the concept of refinement type systems and their various notions of comprehension. Discover how these systems relate to Martin-Löf type theory, providing a deeper understanding of type theory and its applications. Learn about key concepts such as functors as type refinement systems, Isbell duality theorem for type refinement systems, and the bifibrational reconstruction of Lawvere's presheaf hyperdoctrine. Note that due to technical issues, blackboard recordings are presented in a slideshow format. This lecture is part of the Hausdorff Trimester Program: Types, Sets and Constructions, offering valuable insights for researchers and students in the field of mathematical logic and computer science.

Paul André Melliès: Refinement type systems and Martin Lof type theory