Javascript must be enabled for the correct page display

Verifying message-passing programs using decompositions

Vokač, Jakob (2019) Verifying message-passing programs using decompositions. Bachelor's Thesis, Computing Science.


Download (444kB) | Preview
[img] Text
Restricted to Registered users only

Download (142kB)


This bachelor project concerns the implementation of session types through the process calculus called HO [Kouzapas et al., 2016b]. In particular, it explores the framework for Haskell called Cloud Haskell [Epstein et al., 2011] to simulate decomposed HO processes, that can be typed using minimal session types. This serves as an illustration of how typing systems could be implemented in languages with minimal support for session types. In the course of the project, many important properties regarding HO and Cloud Haskell are identified and taken into consideration when translating the decomposed processes. The outcome of the project is an extension of the Haskell implementation of the decomposition function, called MISTY [Arslanagic et al., 2019], which takes the output of this implementation and gives executable Cloud Haskell programs that simulate the output.

Item Type: Thesis (Bachelor's Thesis)
Supervisor name: Perez Parra, J.A. and Arslanagic, A.
Degree programme: Computing Science
Thesis type: Bachelor's Thesis
Language: English
Date Deposited: 11 Oct 2019
Last Modified: 11 Oct 2019 14:26

Actions (login required)

View Item View Item