We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic operations over a monad. We introduce operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant under the reduction and expansion of term and state configurations. Finally, we characterize convergent terms via their typings.

A well-formed global type describes the interaction protocol of multiple end-points via the projection to local specifications. Typed sessions of processes enjoy good communication properties and their overall behaviour is the one described by the global type. We show that a projectable global type is bounded (also said “balanced” in the literature) but also that projectability is not necessary for a global type to be a sound description of well-behaved systems. By revising the semantics of global types via a coinductively defined LTS, we obtain a conservative extension of previous type systems in case of simple sessions without channels and local types, which we call Simple MultiParty Sessions, accommodating unbounded and hence un-projectable global types. Such a system is sound and encompasses infinite sessions that do not type-check for any bounded and/or projectable global type.

We study the logical semantics of an untyped λ-calculus equipped with operators representing read and write operations from and to a global store. Such a logic consists of an intersection type assignment system, which we derive from the denotational semantics of the calculus, based on the monadic approach to model computational λ-calculi. The system is obtained by constructing a filter model in the category of ω-algebraic lattices, such that the typing rules can be recovered out of the term interpretation. By construction, the so-obtained type system satisfies the “type-semantics” property and completeness.

We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, which are sufficient conditions that guarantee a protocol to be implementable. We introduce a typing discipline that enforces well-formedness of typed choreographies. Then we unveil the relation among refinable choreographies and their admissible refinements in terms of an axiom scheme.

Abstract We study the reduction in a $\lambda$ -calculus derived from Moggi’s computational one, which we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form and address the question of normalizing strategies. Our analysis relies on factorization results.

We study the semantics of an untyped λ-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side effects and treat read and write as algebraic operations over a monad. We introduce an operational semantics and a type assignment system of intersection types, and prove that types are invariant under reduction and expansion of term and state configurations, and characterize convergent terms via their typings.

invited-talk Two notions of sub-behaviour for session-based client/server systems: 10 Years Later Share on Authors: Franco Barbanera Universita di Catania, Italy Universita di Catania, ItalyView Profile , Ugo de'Liguoro Universita di Torino, Italy Universita di Torino, ItalyView Profile Authors Info & Claims PPDP '20: Proceedings of the 22nd International Symposium on Principles and Practice of Declarative ProgrammingSeptember 2020 Article No.: 2Pages 1–3https://doi.org/10.1145/3414080.3414082Published:08 September 2020 0citation17DownloadsMetricsTotal Citations0Total Downloads17Last 12 Months9Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous pi-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.

We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebraic lattices via Abramsky's domain-logic approach. This provides at the same time an interpretation of the type system and a proof of the completeness of the system with respect to the continuation models by means of a filter model construction. We then define a restriction of our system, such that a lambda-mu term is typeable if and only if it is strongly normalising. We also show that Parigot's typing of lambda-mu terms with classically valid propositional formulas can be translated into the restricted system, which then provides an alternative proof of strong normalisability for the typed lambda-mu calculus.

We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records. Intersection types with records and record-merge are used to assign meaningful types to these terms without resorting to recursive types. Second, typed terms are translated to a repository of typed combinators. We show a relation between record types with record-merge and intersection types with constructors. This relation is used to prove soundness and partial completeness of the translation with respect to mixin composition synthesis. Furthermore, we demonstrate how a translated repository and goal type can be used as input to an existing framework for composition synthesis in bounded combinatory logic via type inhabitation. The computed result is a class typed by the goal type and generated by a mixin composition applied to an existing class.

We consider the problem of finding pre-fix points of interactive realizers over arbitrary knowledge spaces, obtaining a relative recursive procedure. Knowledge spaces and interactive realizers are an abstract setting to represent learning processes, that can interpret non-constructive proofs. Atomi c pieces of information of a knowledge space are stratified into levels, and evaluated into truth values depending on knowledge states. Realizers are then used to define operators that extend a given state by adding answers and possibly forcing us to remove some: in the learning process states of knowledge change non-monotonically. Existence of a pre-fix point of a realizer is equivalent to the termination of the learning process with some state of knowledge which is free of patent contradictions and such that there is nothing to add. In this paper we generalize our previous results in the case of level 2 knowledge spaces and deterministic operators to the case of ω-level knowledge spaces and of non-deterministic operators.

We consider a notion of approximation for terms of de Groote–Saurin Λμ-calculus. Then, we introduce an intersection type assignment system for that calculus which is invariant under subject conversion. The type assignment system also induces a filter model, which is an extensional Λμ-model in the sense of Nakazawa and Katsumata. We then establish the approximation theorem, stating that a type can be assigned to a term in the system if and only if it can be assigned to same of its approximations.

Abstract In the setting of session behaviours , we study an extension of the concept of compliance when a disciplined form of backtracking and of output skipping is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via an LTS, and define natural notions of checkpoint compliance and sub-behaviour , which we prove to be both decidable. Then we extend the operational semantics with skips and we show the decidability of the obtained compliance.

We propose a refinement and a simplification of the behavioural semantics of session types, based on the concepts of compliance and sub-behaviour from the theory of web contracts. We introduce three relations on a suitable class of behaviours with higher-order input/output, called ‘session behaviours’. Such relations, depending on each other, represent the idea of sub-behaviour from the point of view of a client, a server or a peer, respectively. A restriction of the intersection of the first two relations characterizes the ‘usual’ sub-behaviour relation from the literature. We then device an algorithmic formal system for three subtyping relations (dubbed CSP-subtyping) for session types that takes into account the role played by a user of a channel during an interaction, so extending Gay and Hole subtyping theory. We show that our session behaviours and sub-behaviour relations provide sound and complete semantics for CSP-subtyping, and for Gay and Hole subtyping as a by-product.

We propose a realizability interpretation of a system for quantier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, called here EM 1 -arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the “nature,” represented by the standard interpretation of closed atomic formulas, and with each other. We obtain in this way a program extraction method by proof interpretation, which is faithful with respect to proofs, in the sense that it is compositional and that it does not need any translation.

We propose a refinement and a simplification of the behavioural semantics of types, based on the concepts of compliance and sub-behaviour from the theory of web contracts. We introduce two relations, representing the idea of sub-behaviour from the point of view of the client and the server, respectively, and characterize the sub-behaviour relation (from the literature) as the intersection of the other two. We show that a proper subclass of behaviours, called session behaviors, and the sub-behaviour relations model types and subtyping, clarifying the otherwise problematic extension of type subtyping with concepts from the theory of contracts.

Type-free lazy $\lambda$-calculus is enriched with angelic parallelism and demonic nondeterminism. Call-by-name and call-by-value abstractions are considered and the operational semantics is stated in terms of a must convergence predicate. We introduce a type assignment system with intersection and union types, and we prove that the induced logical semantics is fully abstract.

To model at the same time parallel and nondeterministic functional calculi we define a powerdomain functor Ρ such that it is an endofunctor over the category of algebraic lattices. Ρ is locally continuous and we study the initial solution D ∞ of the domain equation D = Ρ([D → D] ⊥ ). We derive from the algebras of Ρ the logic of D ∞ , that is the axiomatic description of its compact elements. We then define a λ-calculus and a type assignment system using the logic of D ∞ as the related type theory. We prove that the filter model of this calculus, which is isomorphic to D ∞ , is fully abstract with respect to the observational Preorder of the λ-calculus.

Retractions existing in all models of simply typed lambda -calculus are studied and related to other relations among types, such as isomorphisms, surjections, and injections. A formal system to deduce the existence of such retractions is shown to be sound and complete with respect to retractions definable by linear lambda -terms. Results aiming at a system complete with respect to the provable retractions tout court are established.>