Plays as resource terms via non-idempotent intersection types

Conference item

A program is interpreted as a collection of resource terms by the Taylor expansion, as a collection of plays by game semantics, and as a collection of types by a non-idempotent intersection type assignment system. This paper investigates the connection between these models and aims to show that they are essentially the same in a certain sense. Technically we study the relational interpretations of resource terms and of plays, which can be seen as nonidempotent intersection type assignment systems for resource terms and plays, respectively.We show that both relational interpretations are injective, have the same image, and respect composition. This result allows us to study a property of the game model by using the syntax of a resource calculus and vice versa.

Authors: Tsukada, T; Ong, C

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Association for Computing Machinery
• Host title: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
• Journal: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
• Pages: 237-246
• Publication date: 2016-07-01
• Acceptance date: 2016-04-04
• DOI: 10.1145/2933575.2934553
• ISSN: 1043-6871
• ISBN: 9781450343916
• Keywords: intersection types; relational models; Game semantics; resource calculus