System F^_ with context-free session types

DOI10.1007/978-3-031-30044-8_15zbMATH Open1541.68258MaRDI QIDQ6535246FDOQ6535246

Authors: Diogo Poças, Diana Costa, Andreia Mordido, Vasco T. Vasconcelos 

Publication date: 24 November 2023

Recommendations

• Polymorphic lambda calculus with context-free session types
• Deciding the bisimilarity of context-free session types
• Context-free session types for applied pi-calculus
• Context-free session type inference
• Nested session types

zbMATH Keywords

System Fhigher-order kindscontext-free session types

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Functions as processes
• Title not available (Why is that?)
• Linear logic
• Combinatory logic. With two sections by William Craig.
• Decidability of DPDA equivalence
• Title not available (Why is that?)
• Subtyping for session types in the pi calculus
• Types and programing languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear type theory for asynchronous session types
• Comparing object encodings.
• Bisimulation equivalence is decidable for all context-free processes
• Proof-carrying code in a session-typed process calculus
• Behavioral polymorphism and parametricity in session-based communication
• Title not available (Why is that?)
• Title not available (Why is that?)
• Decidability of bisimulation equivalence for process generating context-free languages
• Title not available (Why is that?)
• Polytypic values possess polykinded types
• An elementary bisimulation decision procedure for arbitrary context-free processes
• Title not available (Why is that?)
• Session types revisited
• Fundamentals of session types
• Title not available (Why is that?)
• Numbering matters
• Bounded polymorphism in session types
• The equivalence problem for deterministic pushdown automata is decidable
• Title not available (Why is that?)
• Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)
• Polymorphic lambda calculus with context-free session types
• Talking bananas: structural recursion for session types
• Higher-order processes, functions, and sessions: a monadic integration
• Recursive subtyping revealed (functional pearl)
• BPA bisimilarity is EXPTIME-hard
• Practical coinduction
• Polarized Substructural Session Types
• Context-free session types
• Deciding the bisimilarity of context-free session types
• Nested session types
• Characteristic formulae for session types
• Context-free session type inference
• On polymorphic sessions and functions. A tale of two (fully abstract) encodings
• Session coalgebras: a coalgebraic view on session types and communication protocols
• Title not available (Why is that?)
• System F-omega with equirecursive types for datatype-generic programming
• Title not available (Why is that?)
• Contractive signatures with recursive types, type parameters, and abstract types
• The different shades of infinite session types

Cited In (1)

• The different shades of infinite session types

This page was built for publication: System \(F^\mu_\omega\) with context-free session types

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