A continuation-based solution of the linearity challenge

DOI10.1007/S10817-026-09765-WMaRDI QIDQ7405773zbMATH OpenFDO

Authors Luca Padovani, Claudia Raffaelli

Publication date 2026

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-026-09765-W

zbMATH Keywords

Agdacontinuationsdeadlock freedomlinear logicsession types

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \( \pi\) with leftovers: a mechanisation in Agda
• A logical account of subtyping for session types
• A Semantics for Propositions as Sessions
• A simple library implementation of binary sessions
• An extensible approach to session polymorphism
• Computational interpretations of linear logic
• Everybody's got to be somewhere
• Formalized meta-theory of sequent calculi for linear logics
• Formalized meta-theory of sequent calculi for substructural logics
• Fundamentals of session types
• scientific article; zbMATH DE number 1863387 (Why is no real title available?)
• Linear logic propositions as session types
• Linear type theory for asynchronous session types
• Mechanizing focused linear logic in Coq
• On the \(\pi\)-calculus and linear logic
• Propositions as sessions
• Session types
• Session types as intuitionistic linear propositions
• Session types revisited
• Subtyping for session types in the pi calculus
• The Logic of Bunched Implications
• Type systems for concurrent programs.
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic

This page was built for publication: A continuation-based solution of the linearity challenge

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