Skip to content

Abstracts.2020.ModTySys

Jump to bottom
Carlos Tomé edited this page Mar 10, 2021 · 2 revisions

A Unified View of Modalities in Type Systems

by 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.

References

  1. Andreas Abel, Jean-Philippe Bernardy. A unified view of modalities in type systems. ICFP 2020. [video]
Clone this wiki locally