Master’s Thesis

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.