Normalization for multimodal type theory

DOI10.1145/3531130.3532398MaRDI QIDQ6649430

Daniel Gratzer

Publication date: 6 December 2024

zbMATH Keywords

normalizationtype theorycategorical semanticsmodal type theorymodalitiesArtin gluing

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30) Type theory (03B38)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Fitch-style modal lambda calculi
• Sketches
• Canonicity and normalization for dependent type theory
• Type theory in type theory using quotient inductive types
• Natural models of homotopy type theory
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Connected limits, familial representability and Artin glueing
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Categorical reconstruction of a reduction free normalization proof
• Pointers in Recursion: Exploring the Tropics
• Modalities in homotopy type theory
• Modal dependent type theory and dependent right adjoints
• Normalisation by Evaluation for Dependent Types.
• Intensional interpretations of functionals of finite type I
• Types for Proofs and Programs
• Univalence for inverse diagrams and homotopy canonicity

This page was built for publication: Normalization for multimodal type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6649430)