scholarly journals Session Type Systems based on Linear Logic: Classical versus Intuitionistic

2020 ◽  
Vol 314 ◽  
pp. 1-11 ◽  
Author(s):  
Bas van den Heuvel ◽  
Jorge A. Pérez
Keyword(s):  
Linear Logic ◽  
Type Systems ◽  
Session Type

Linear logic propositions as session types

2014 ◽  
Vol 26 (3) ◽  
pp. 367-423 ◽  
Author(s):  
LUÍS CAIRES ◽  
FRANK PFENNING ◽  
BERNARDO TONINHO
Keyword(s):  
Sequent Calculus ◽  
Linear Logic ◽  
Type System ◽  
Type Systems ◽  
Cut Elimination ◽  
Session Types ◽  
Deadlock Freedom ◽  
Session Type ◽  
Π Calculus ◽  
Intuitionistic Linear Logic

Throughout the years, several typing disciplines for the π-calculus have been proposed. Arguably, the most widespread of these typing disciplines consists of session types. Session types describe the input/output behaviour of processes and traditionally provide strong guarantees about this behaviour (i.e. deadlock-freedom and fidelity). While these systems exploit a fundamental notion of linearity, the precise connection between linear logic and session types has not been well understood.This paper proposes a type system for the π-calculus that corresponds to a standard sequent calculus presentation of intuitionistic linear logic, interpreting linear propositions as session types and thus providing a purely logical account of all key features and properties of session types. We show the deep correspondence between linear logic and session types by exhibiting a tight operational correspondence between cut-elimination steps and process reductions. We also discuss an alternative presentation of linear session types based on classical linear logic, and compare our development with other more traditional session type systems.

scholarly journals Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols

2021 ◽  
pp. 375-403
Author(s):  
Alex C. Keizer ◽  
Henning Basold ◽  
Jorge A. Pérez
Keyword(s):  
Communication Protocols ◽  
Type System ◽  
Type Systems ◽  
Software Systems ◽  
Compositional Techniques ◽  
Behavioural Type ◽  
Session Types ◽  
Session Type ◽  
Coalgebra Structure ◽  
Large Systems

AbstractCompositional methods are central to the development and verification of software systems. They allow breaking down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that programs interact with channels according to a certain protocol, whether the intended messages are exchanged in a certain order. In this paper, we put on our coalgebraic spectacles to investigate session types, a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation makes it possible to elegantly derive a decidable type system with subtyping for $$\pi $$ π -calculus processes, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective agree with the existing ones.

scholarly journals Propositions-as-types and shared state

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Pedro Rocha ◽  
Luís Caires
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Linear Logic ◽  
Natural Extension ◽  
Concurrent Programming ◽  
Type Systems ◽  
Liveness Properties ◽  
Mutable State ◽  
Shared State ◽  
Logical Rules

We develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.

scholarly journals Gradual session types

2019 ◽  
Vol 29 ◽  
Author(s):  
ATSUSHI IGARASHI ◽  
PETER THIEMANN ◽  
YUYA TSUDA ◽  
VASCO T. VASCONCELOS ◽  
PHILIP WADLER
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Type Systems ◽  
Session Types ◽  
Novel Approach ◽  
Seamless Transition ◽  
Linear Types ◽  
Gradual Typing ◽  
Session Type ◽  
Dynamic Typing

Abstract Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types; an internal language with casts, for which operational semantics is given; and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.

Program equivalence in a linear functional language

2000 ◽  
Vol 10 (2) ◽  
pp. 167-190 ◽  
Author(s):  
G. M. BIERMAN
Keyword(s):  
Linear Functional ◽  
Linear Logic ◽  
Type Systems ◽  
Functional Languages ◽  
Functional Language ◽  
Program Equivalence ◽  
Principal Theorem ◽  
Contextual Equivalence

Researchers have recently proposed that for certain applications it is advantageous to use functional languages whose type systems are based upon linear logic: so-called linear functional languages. In this paper we develop reasoning techniques for programs in a linear functional language, linPCF, based on their operational behaviour. The principal theorem of this paper is to show that contextual equivalence of linPCF programs can be characterised coinductively. This characterisation provides a tractable method for reasoning about contextual equivalence, and is used in three ways:[bull ] A number of useful contextual equivalences between linPCF programs is given.[bull ] A notion of type isomorphism with respect to contextual equivalence, called operational isomorphism, is given. In particular the types !ϕ[otimes ]!ψ and !(ϕ&ψ) are proved to be operationally isomorphic.[bull ] A translation of non-strict PCF into linPCF is shown to be adequate, but not fully abstract, with respect to contextual equivalence.

Effects of activated carbon on treatment of photo-processing waste by sulfur-oxidizing bacteria

1997 ◽  
Vol 35 (7) ◽  
pp. 187-195 ◽  
Author(s):  
Binle Lin ◽  
K. Futono ◽  
A. Yokoi ◽  
M. Hosomi ◽  
A. Murakami
Keyword(s):  
Activated Carbon ◽  
Treatment Effectiveness ◽  
Environmental Concern ◽  
Type Systems ◽  
Continuous Treatment ◽  
Processing Waste ◽  
Treatment Technology ◽  
Adsorption Effect ◽  
Sulfur Oxidizing ◽  
Sulfur Oxidizing Bacteria

Establishing economic treatment technology for safe disposal of photo-processing waste (PW) has most recently become an urgent environmental concern. This paper describes a new biological treatment process for PW using sulfur-oxidizing bacteria (SOB) in conjunction with activated carbon (AC). Batch-type acclimation and adsorption experiments using SOB/PAC, SOB/PNAC, and SOB reactor type systems demonstrated that AC effectively adsorbs the toxic/refractory compounds which inhibit thiosulfate oxidization of SOB in PW. Thus, to further clarify the effect of AC, we performed a long-term (≈ 160 d) continuous-treatment experiment on 4- to 8-times dilution of PW using a SOB/GAC system which simulated a typical wastewater treatment system based on an aerobic activated sludge process that primarily uses acclimated SOB. The thiosulfate load and hydraulic retention time (HRT) were fixed during treatment such that they ranged from 0.8-3.7 kg S2O32-/l/d and 7.7-1.9 d, respectively. As expected, continuous treatment led to breakthrough of the adsorption effect of GAC. Renewing the GAC and continuing treatment for about 10 d demonstrated good treatment effectiveness.

Sign in / Sign up

Export Citation Format

Share Document