Practical affine types

Jesse A. Tov, Riccardo Pucella

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

Abstract

Alms is a general-purpose programming language that supports practical affine types. To offer the expressiveness of Girard's linear logic while keeping the type system light and convenient, Alms uses expressive kinds that minimize notation while maximizing polymorphism between affine and unlimited types. A key feature of Alms is the ability to introduce abstract affine types via ML-style signature ascription. In Alms, an interface can impose stiffer resource usage restrictions than the principal usage restrictions of its implementation. This form of sealing allows the type system to naturally and directly express a variety of resource management protocols from special-purpose type systems. We present two pieces of evidence to demonstrate the validity of our design goals. First, we introduce a prototype implementation of Alms and discuss our experience programming in the language. Second, we establish the soundness of the core language. We also use the core model to prove a principal kinding theorem.

Original languageEnglish (US)
Title of host publicationPOPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages447-458
Number of pages12
DOIs
StatePublished - Dec 1 2010
Event38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11 - Austin, TX, United States
Duration: Jan 26 2011Jan 28 2011

Other

Other38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
CountryUnited States
CityAustin, TX
Period1/26/111/28/11

Keywords

  • Affine types
  • Linear logic
  • Modules
  • Polymorphism
  • Type systems

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Practical affine types'. Together they form a unique fingerprint.

Cite this