Types, Homotopy, Type Theory, and Verification Workshop

Explore advanced topics in type theory, homotopy theory, and formal verification through this comprehensive workshop featuring leading researchers in the field. Delve into cutting-edge developments including cubical type theory investigations, modal dependent type theories, and cohesive homotopy type theory (HoTT). Master fibrational frameworks for both simple and dependent modal type theories while examining discrete and codiscrete modalities in cohesive settings. Investigate the shape modality in real cohesive HoTT and its applications to covering spaces, alongside differential cohesive HoTT concepts. Study cubical models and their relationship to homotopy types, including cartesian cubical computational type theory and the yacctt system. Examine theoretical foundations through initiality theorems for general type theories, univalent polymorphism, and W types in setoid models. Address practical challenges such as free groups in homotopy type theory and explore assemblies as elementary quotient completions. Connect type theory to broader mathematical concepts through refinement type systems and their relationship to Martin-Löf type theory, providing a thorough grounding in both theoretical foundations and computational applications.