Verifying message-passing programs using decompositions

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

Preview	Text BSc_Thesis___Verifying_message_passing_programs_using_decompositions.pdf Download (444kB) | Preview
	Text toestemming.pdf Restricted to Registered users only Download (142kB)

Abstract

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
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/21095

Actions (login required)

View Item