Uniqueness Typing in Natural Deduction Style

Abstract

We present two type systems for graph rewriting: conventional typing and (polymorphic) uniqueness typing. The latter is introduced as a natural extension of simple algebraic and higher-order uniqueness typing. The systems are given in natural deduction style using an inductive syntax of graph denotations with familiar constructs such as let and case.

The conventional system resembles traditional Curry-style typing systems in functional programming languages. Uniqueness typing extends this with reference count information. In both type systems, typing is preserved during evaluation, and types can be determined effectively.

Due to the present formalization, the system can easily be compared with other proposals based on linear and affine logic.

Contributors

Erik Barendsen

Sjaak Smetsers

Conference

Publication date: July 1995

Publication date (Print): July 1995

Pages: 1-10

Affiliations

University of Nijmegen, Computing Science Institute

Toernooiveld 1, 6525 ED Nijmegen, The Netherlands

Article

DOI: 10.14236/ewic/FP1995.1

Copyright statement: © Erik Barendsen et al. Published by BCS Learning and Development Ltd. Proceedings of the 1995 Glasgow Workshop on Functional Programming, Ullapool, Scotland

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Proceedings of the 1995 Glasgow Workshop on Functional Programming

Conference acronym: FP

Conference number:

Conference location: Ullapool, Scotland

Conference date: 10-12 July 1995

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Functional Programming

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/FP1995.1

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing