We present a binary session type system using context-free session types to a version of the applied pi-calculus of Abadi et. al. where only base terms, constants and channels can
Concrete artefacts are produced and used for dissemination. These include scientific publications, a repository of use-cases, tutorials, a non-technical article presenting the main achievements of the project, material for tutorials and recorded tutorials. These artefacts will remain available to the general public beyond the duration of the project and promote a continuative and long-term dissemination.
If you are unable to view these files, please log in or register.
This work exploits the logical foundation of session types to determine what kind of type discipline for the pi-calculus can exactly capture, and is captured by, lambda-calculus behaviours. Leveraging the proof theoretic
This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed lambda-calculus. The proposed framework, by
In the simply-typed lambda-calculus we can recover the full range of expressiveness of the untyped lambda-calculus solely by adding a single recursive type U = U -> U. In contrast,
The adoption of formal models by process specialists has faced two challenges: First, it requires process specialists to get training in formal modeling. Second, the resulting specifications bear little resemblance
(a) Situation faced: Exformatics, a Danish adaptive case-management vendor, wanted to leverage declarative process tools to support the flexible processes found at BRFkredit. However, switching from the more common flow-based
Process modelling notations fall in two broad categories: declarative notations, which specify the rules governing a process; and imperative notations, which specify the flows admitted by a process. We outline an empirical approach to