Formalization of a Type and Effect System using Coq and Ott

Abstract

Papers from the field of programming language theory, especially those related to concurrent programming languages, often contain languages and definitions with many rules, and proofs about these are therefore often long and tedious. The need for both formalization and automation is sought after, as indicated by the POPLMark-challenge. This thesis presents a formalization of two type and effect systems, and a formalized proof relating one of the systems to the other. The formalization is realized with the tools Coq and Ott, which give a rigorous and machine checkable formalization.