Propositions as sessions

DOI10.1145/2364527.2364568MaRDI QIDQ5168904zbMATH OpenOpenAlexFDO

Authors Philip Wadler

Publication date 21 July 2014

Published in Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2364527.2364568

zbMATH Keywords

lambda calculuslinear logicpi calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Propositions as sessions
• A Semantics for Propositions as Sessions
• scientific article; zbMATH DE number 2048506
• Propositions
• scientific article; zbMATH DE number 5521993
• Assembling Sessions
• scientific article; zbMATH DE number 1897911
• Propositions as cognitive acts
• Anatomy of a proposition

Cited in

(59)

• Multiparty session types, beyond duality
• A core model for choreographic programming
• A message-passing interpretation of adjoint logic
• Mixed sessions
• Polymorphic lambda calculus with context-free session types
• Nested session types
• Multiparty session types as coherence proofs
• On concurrent behaviors and focusing in linear logic
• Session types revisited
• Comparing type systems for deadlock freedom
• On the hardness of proving CCA-security of Signed ElGamal
• A Semantics for Propositions as Sessions
• Session Types with Gradual Typing
• Corecursion and non-divergence in session-typed processes
• Type-Based Analysis for Session Inference (Extended Abstract)
• Effects as sessions, sessions as effects
• Propositions as sessions
• Observed Communication Semantics for Classical Processes
• Linearity, control effects, and behavioral types
• Assembling Sessions
• I got plenty o' nuttin'
• Linear is CP (more or less)
• Certifying data in multiparty session types
• Session types as intuitionistic linear propositions
• Affine sessions
• Propositions
• A linear/producer/consumer model of classical linear logic
• Linear logical relations and observational equivalences for session-based concurrency
• COCHIS: stable and coherent implicits
• Comparing deadlock-free session typed processes
• Taking linear logic apart
• Rast: a language for resource-aware session types
• Mixed sessions
• Session Types with Arithmetic Refinements
• Circular proofs as session-typed processes: a local validity condition
• Towards races in linear logic
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Asynchronous functional sessions: cyclic and concurrent
• Polymorphic higher-order context-free session types
• Safe session-based concurrency with shared linear state
• Resource sharing via capability-based multiparty session types
• Linear resources in Isabelle/HOL
• Towards logical foundations for probabilistic computation
• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Comparing session type systems derived from linear logic
• Curry and Howard meet Borel
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Deadlock freedom for asynchronous and cyclic process networks
• Typed non-determinism in concurrent calculi: the eager way
• Rast: resource-aware session types with arithmetic refinements (system description)
• Semi-axiomatic sequent calculus
• Around classical and intuitionistic linear processes
• Adjoint natural deduction
• A gentle overview of asynchronous session-based concurrency: deadlock freedom by typing
• EXPRESSing session types
• A sound and complete projection for global types
• Worst-case input generation for concurrent programs under non-monotone resource metrics
• Less is more revisited: association with global protocols and multiparty sessions
• Policies for fair exchanges of resources

This page was built for publication: Propositions as sessions

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