Type classes for lightweight substructural types

MaRDI QIDQ5015212zbMATH OpenFDO

Authors Edward Gan, Jesse A. Tov, Greg Morrisett

Publication date 6 December 2021

Full work available at URL https://arxiv.org/abs/1502.04772, http://eptcs.web.cse.unsw.edu.au/paper.cgi?LINEARITY2014.4

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• Static typing for a substructural lambda calculus
• Substructural Type Systems for Program Analysis
• Type Reconstruction for Type Classes
• Modular type classes
• Programming Languages and Systems

Cites work

• A step-indexed model of substructural state
• Computational interpretations of linear logic
• scientific article; zbMATH DE number 969070 (Why is no real title available?)
• scientific article; zbMATH DE number 2238212 (Why is no real title available?)
• Linear logic
• Linear type theory for asynchronous session types
• Lolliproc: to concurrency from classical linear logic via Curry-Howard and control
• Practical affine types
• Qualified Types
• Reference counting as a computational interpretation of linear logic

Cited in

(8)

• Static typing for a substructural lambda calculus
• Modular inference of linear types for multiplicity-annotated arrows
• Superficially substructural types
• Practical affine types
• Substructural Type Systems for Program Analysis
• Additive types in quantitative type theory
• Linearity and uniqueness: an entente cordiale
• A framework for substructural type systems

Describes a project that uses

Uses Software

• Alms

This page was built for publication: Type classes for lightweight substructural types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5015212)