Polarized Substructural Session Types

DOI10.1007/978-3-662-46678-0_1MaRDI QIDQ2948548zbMATH OpenOpenAlexFDO

Authors Dennis Griffith, Frank Pfenning

Publication date 1 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2142/90544

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Polarized subtyping
• Polarized Subtyping for Sized Types
• Polarised subtyping for sized types
• Session types and subtyping for orchestrated interactions
• Fair subtyping for multi-party session types
• Mixed polarized constructions
• Linearly refined session types
• Sublattices Generated by Polars
• Polarization and isogenies

Cited in

(21)

• A message-passing interpretation of adjoint logic
• Polymorphic lambda calculus with context-free session types
• Nested session types
• Fairness and communication-based semantics for session-typed languages
• Linear is CP (more or less)
• A linear/producer/consumer model of classical linear logic
• A universal session type for untyped asynchronous communication
• Non-blocking concurrent imperative programming with session types
• scientific article; zbMATH DE number 7441269 (Why is no real title available?)
• Gradual type theory
• scientific article; zbMATH DE number 7453964 (Why is no real title available?)
• Rast: a language for resource-aware session types
• Back to futures
• Session Types with Arithmetic Refinements
• Circular proofs as session-typed processes: a local validity condition
• Two decades of automatic amortized resource analysis
• Session-typed concurrent contracts
• System \(F^\mu_\omega\) with context-free session types
• Around classical and intuitionistic linear processes
• Worst-case input generation for concurrent programs under non-monotone resource metrics
• A mixed linear and graded logic: proofs, terms, and models

This page was built for publication: Polarized Substructural Session Types

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