Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

DOI10.46298/lmcs-19(4:1)2023arXiv2104.14759MaRDI QIDQ6076174

Daniele Nantes-Sobrinho, Unnamed Author, Jorge A. Pérez

Publication date: 23 October 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

linear logicconcurrency\(\pi\)-calculusintersection typesprocess calculilambda-calculussession typesresource calculi

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx) Computer science (68-XX)

Related Items (1)

Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A prismoid framework for languages with resources
• Resource operators for \(\lambda\)-calculus
• A calculus of mobile processes. I
• Intersection type assignment systems
• Coherence for sharing proof-nets
• A general theory of sharing graphs
• The differential lambda-calculus
• Principality and type inference for intersection types using expansion variables
• The discriminating power of multiplicities in the \(\lambda\)-calculus
• Towards a unified approach to encodability and separation results for process calculi
• On phase semantics and denotational semantics in multiplicative-additive linear logic
• Non-idempotent intersection types in logical form
• On the relative expressiveness of higher-order session processes
• On polymorphic sessions and functions. A tale of two (fully abstract) encodings
• Effects as sessions, sessions as effects
• Expressiveness of Process Algebras
• Functions as Session-Typed Processes
• Linearity, Control Effects, and Behavioral Types
• Intersection Types for the Resource Control Lambda Calculi
• A new type assignment for λ-terms
• Solvability in Resource Lambda-Calculus
• Session Types as Intuitionistic Linear Propositions
• Functions as processes
• A linearization of the Lambda-calculus and consequences
• Execution time of λ-terms via denotational semantics and intersection types
• Non-idempotent intersection types for the Lambda-Calculus
• From λ to π; or, Rediscovering continuations
• A tale of intersection types
• Propositions as sessions
• Process Types as a Descriptive Tool for Interaction
• Types, potency, and idempotency
• Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing
• Full abstraction for expressiveness: history, myths and facts
• On phase semantics and denotational semantics: The exponentials
• Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

This page was built for publication: Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)