Linearity, control effects, and behavioral types

DOI10.1007/978-3-662-54434-1_9zbMATH Open1485.68055DBLPconf/esop/CairesP17OpenAlexW2594993942WikidataQ57652340 ScholiaQ57652340MaRDI QIDQ2988641FDOQ2988641

Authors: Luís Caires, Jorge A. Pérez 

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/25748

Recommendations

• A type and effect system for determinism in multithreaded programs
• Lolliproc: to concurrency from classical linear logic via Curry-Howard and control
• Session types as intuitionistic linear propositions
• CONCUR 2005 – Concurrency Theory
• Linearity, session types and the pi calculus

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• Practical affine types
• Title not available (Why is that?)
• Differential interaction nets
• A Powerdomain Construction
• The \(\pi\)-calculus: A theory of mobile processes
• Logic Programming with Focusing Proofs in Linear Logic
• Session types as intuitionistic linear propositions
• Linear type theory for asynchronous session types
• Title not available (Why is that?)
• Structured Interactional Exceptions in Session Types
• Computational types from a logical perspective
• On the expressiveness of internal mobility in name-passing calculi
• Linear logical relations for session-based concurrency
• Proof-carrying code in a session-typed process calculus
• Propositions as sessions
• Behavioral polymorphism and parametricity in session-based communication
• Title not available (Why is that?)
• Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python
• Linear logic propositions as session types
• Title not available (Why is that?)
• Multiparty Session Types Within a Canonical Binary Theory, and Beyond
• Title not available (Why is that?)
• Linear forwarders
• Stateful contracts for affine types
• Title not available (Why is that?)
• Higher-order processes, functions, and sessions: a monadic integration
• Title not available (Why is that?)
• Effects as sessions, sessions as effects
• Functions as session-typed processes
• Global escape in multiparty sessions
• Conflation confers concurrency
• Superficially substructural types

Cited In (9)

• An interpretation of CCS into ludics
• Comparing type systems for deadlock freedom
• Safe session-based concurrency with shared linear state
• A message-passing interpretation of adjoint logic
• Deadlock freedom for asynchronous and cyclic process networks
• Comparing session type systems derived from linear logic
• A subexponential view of domains in session types
• A type and effect system for determinism in multithreaded programs
• Resource sharing via capability-based multiparty session types

Uses Software

• Alms

This page was built for publication: Linearity, control effects, and behavioral types

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