On Polymorphic Sessions and Functions

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Verification of Knowledge Obtained in the Study of Business Process Models

The paper focuses on the method of formal verification of knowledge obtained in the study of business process models. As a formal language for the presentation and verification of business processes, a certain version of π-calculus was chosen, and linear temporal modal logic was chosen as a language for formulating test assignments, i.e., questions, to be checked. The paper gives the rationale for such choice, and considers the principles of developing the test assignments in the language of modal logic and their usage for knowledge verification. The study proposes to automate knowledge testing with logic programs obtained as a result of the transition from a description of business processes to a verification program in the logical programming language Visual Prolog. The formal knowledge verification technique is illustrated by examples of knowledge verification. Findings of research show how the transition from the description of business processes to the procedures of formal verification of knowledge is carried out. The prospects for the development of the proposed method are discussed