A unified view of modalities in type systems
Andreas Abel, Jean-Philippe Bernardy
Abstract
We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose.
Topics & Concepts
ModalitiesGeneralityMetatheoryComputer scienceType (biology)Range (aeronautics)Theoretical computer scienceCognitive scienceProgramming languagePsychologySociologyEngineeringSocial scienceEcologyPsychotherapistBiologyAerospace engineeringLogic, programming, and type systemsLogic, Reasoning, and KnowledgeSemantic Web and Ontologies