Master’s Thesis


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

It’s been some years now since this was produced, yet working with type systems recently I figured it was worth putting my master’s thesis online as well. It didn’t contain any break-through results, but I remember being content with its ridged formulations and proofs, and its self-containment — it even including a section in the appendix outlining the entire approach in the form of a tiny and easy-to-understand type system.

From the abstract:

In this paper we give a type inference algorithm for a type system for a pi calculus. The effect type system with dependent types guarantees that well-typed processes respect an authenticity property expressed as correspondences.

Given a process and a type context we generate constraints that are satisfiable if and only if the process can be made well-typed under the context. […] The output of the algorithm can be used to efficiently construct a proof of safety in the form of a derivation tree.

Experiments with a Caml implementation have shown that the algorithm performs well in praxis.

A small paper based on the thesis was presented at Nordic Workshop on Programming Theory 2008 (NWPT’08), and it also served as the basis for a later paper on a more advanced type system, presented at Workshop on Foundations of Security and Privacy 2010 (FCS-PrivMod’10).

 

Leave a Reply

Your email address will not be published.