20/08/2020

A Unified View of Modalities in Type Systems

Andreas Abel, Jean-Philippe Bernardy

Keywords: subtyping, linear types, modal logic

Abstract Paper Similar Papers

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.

 0
 0
 0
 0
  Share    
This is an embedded video. Talk and the respective paper are published at ICFP 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd Characters remaining: 140

Similar Papers

 0
 0
 0
 0
 17:16 
 0
 0
 0
 0
 15:50 
 0
 0
 0
 0
 15:00 
 0
 0
 0
 0
 21:13 
 0
 0
 0
 0
 15:05 
 0
 0
 0
 0
 14:33 
 0
 0
 0
 0
 13:45 
 0
 0
 0
 0
 13:09 
 0
 0
 0
 0
 14:39 
 0
 0
 0
 0
 25:54 
 0
 0
 0
 0
 16:10 
 0
 0
 0
 0
 14:13 
 0
 0
 0
 0
 15:04 
 0
 0
 0
 0
 24:21 
 0
 0
 0
 0
 11:16 
 0
 0
 0
 0
 15:07 
 0
 0
 0
 0
 2:57 
 0
 0
 0
 0
 24:54 
 0
 0
 0
 0
 11:29 
 0
 0
 0
 0
 21:37 
 0
 0
 0
 0
 14:45 
 0
 0
 0
 0
 12:55 
 0
 0
 0
 0
 25:33 
 0
 0
 0
 0
 13:32 
 0
 0
 0
 0
 18:30 
 0
 0
 0
 0
 4:45 
 0
 0
 0
 0
 14:27 
 0
 0
 0
 0
 14:59 
 0
 0
 0
 0
 16:06 
 0
 0
 0
 0
 19:19 
 0
 0
 0
 0
 12:47 
 0
 0
 0
 0
 30:20 
 0
 0
 0
 0
 4:57 
 0
 0
 0
 0
 10:40 
 0
 0
 0
 0
 15:20 
 0
 0
 0
 0
 23:41 
 0
 0
 0
 0
 25:23 
 0
 0
 0
 0
 10:02 
 0
 0
 0
 0
 12:26 
 0
 0
 0
 0
 20:31