Circular proofs as session-typed processes: a local validity condition

MaRDI QIDQ5094136FDO

Authors Farzaneh Derakhshan, Frank Pfenning

Publication date 2 August 2022

Full work available at URL https://arxiv.org/abs/1908.01909

zbMATH Keywords

progresssubstructural logicfixed pointslinear logicsession typesterminationcircular proofssubsingleton logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Local validity for circular proofs in linear logic with fixed points
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• Session types as intuitionistic linear propositions
• A new linear logic for deadlock-free session-typed processes
• scientific article; zbMATH DE number 6774227

Cites work

• scientific article; zbMATH DE number 6680140 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1956528 (Why is no real title available?)
• scientific article; zbMATH DE number 2087442 (Why is no real title available?)
• scientific article; zbMATH DE number 1398002 (Why is no real title available?)
• scientific article; zbMATH DE number 7533344 (Why is no real title available?)
• μ-Bicomplete Categories and Parity Games
• Around classical and intuitionistic linear logics
• Constructive completeness for the linear-time \(\mu \)-calculus
• Cut reduction in linear logic as asynchronous session-typed communication
• Free \(\mu\)-lattices
• From parity games to circular proofs
• Higher-order processes, functions, and sessions: a monadic integration
• Infinitary proof theory: the multiplicative additive case
• Intensional type theory with guarded recursive types qua fixed points on universes
• Linear logic propositions as session types
• Linear type theory for asynchronous session types
• Local validity for circular proofs in linear logic with fixed points
• Polarized Substructural Session Types
• Propositions as sessions
• Realizability in cyclic proof: extracting ordering information for infinite descent
• Session types as intuitionistic linear propositions
• Substructural proofs as automata
• Talking bananas: structural recursion for session types
• Well-founded recursion with copatterns and sized types

Cited in

(3)

• Local validity for circular proofs in linear logic with fixed points
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
• A logical account of subtyping for session types

This page was built for publication: Circular proofs as session-typed processes: a local validity condition

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