We present an extension of polymorphic context-free session types that allows passing channels on channels, commonly known as higher-order session types. The mixture of functional types and session types has proven to be a challenge for type equivalence formulation: whereas functional type equivalence is often inductive and presented as a system of derivation rules, session type equivalence is often coinductive and usually presented as a bisimulation. We propose a unifying approach that handles the equivalence of functional and higher-order context-free session types together in the form of a system of rules generating a coinductively defined relation. Decidability of type equivalence is obtained via reduction to bisimulation for simple grammars, for which practical algorithms are known. To bridge the gap between types and simple grammars, we introduce a language of types with canonical names instead of bindings (which we call c-types), and propose a notion of canonical renaming to translate types to c-types.

Abstract We study increasingly expressive type systems, from $$F^\mu $$ Fμ —an extension of the polymorphic lambda calculus with equirecursive types—to $$F^{\mu ;}_\omega $$ Fωμ; —the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contractive fragment of $$F^\mu _\omega $$ Fωμ as studied in the literature. Decidability results for type equivalence of the various type languages are obtained from the translation of types into objects of an appropriate computational model: finite-state automata, simple grammars and deterministic pushdown automata. We show that type equivalence is decidable for a significant fragment of the type language. We further propose a message-passing, concurrent functional language equipped with the expressive type language and show that it enjoys preservation and absence of runtime errors for typable processes.

Switch graphs are graph-like structures characterized by embedding higher-level edges (edges that link to other edges) to describe reactive phenomena. When an edge of such structure is traversed, the accessibility relation of this graph can be changed by adding/removing edges. Relation-changing models have been used to represent phenomena in diverse fields (from Biology to Computer Science) and some modal languages were introduced recently. In this paper we introduce four-valued local information in switch graphs, and propose a paraconsistent logic to study these systems.

We propose an extension of separation logic with fractional permissions, aimed at reasoning about concurrent programs that share arbitrary regions or data structures in memory. In existing formalisms, such reasoning typically either fails or is subject to stringent side conditions on formulas (notably precision ) that significantly impair automation. We suggest two formal syntactic additions that collectively remove the need for such side conditions: first, the use of both “weak” and “strong” forms of separating conjunction, and second, the use of nominal labels from hybrid logic. We contend that our suggested alterations bring formal reasoning with fractional permissions in separation logic considerably closer to common pen-and-paper intuition, while imposing only a modest bureaucratic overhead.

When visiting a hospital and seeking for answers for their symptoms, many people face contradictory diagnoses given by different physicians. This may happen either because they exhibit symptoms that are common to several diseases or because the symptoms are themselves misleading. In some cases, complementary methods of diagnostic are needed for further discussion. However, sometimes, not even those are the solution for an infallible diagnosis. By resorting to multimodal hybrid logic in a setting where inconsistencies are allowed, we introduce an informal example about the path of a patient in a hospital, where we keep information about his symptoms and diagnoses until being discharged. Our goal is the establishment of a measure of inconsistency, so that one can get a sense on the quality of the treatment given to the patient. By gathering a sufficient amount of information about patients in a hospital, those measures could be of help in determining the efficiency of the hospital. This is a critical issue, as it is well-known that early diagnoses are superbly desirable and can be life-changing.

As in standard knowledge bases, hybrid knowledge bases (i.e. sets of information specified by hybrid formulas) may contain inconsistencies arising from different sources, namely from the many mechanisms used to collect relevant information. Being a fact, rather than a queer anomaly, inconsistency also needs to be addressed in the context of hybrid logic applications. This article introduces a paraconsistent version of hybrid logic which is able to accommodate inconsistencies at local points without implying global failure. A main feature of the resulting logic, crucial to our approach, is the fact that every hybrid formula has an equivalent formula in negation normal form. The article also provides a measure to quantify the inconsistency of a hybrid knowledge base, useful as a possible basis for comparing knowledge bases. Finally, the concepts of extrinsic and intrinsic inconsistency of a theory are discussed.

In this paper we focus in health care knowledge, specified by hybrid formulas, representing flows of medical assistance in the care delivery process in a hospital. As in standard knowledgebases inconsistencies may arise. In fact, Medical Informatics is one field where the ability to reason with inconsistent information is crucial. Patients can receive different, and moreover contradictory, diagnoses from different physicians, and the same can happen with medical treatments: they can exhibit contradictory symptoms. We introduce a paraconsistent version of multimodal hybrid logic to help with this medical issue, specially through the diagnosis.