Reusable Programming Language Components
C.R. van der Rest (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. van Deursen – Promotor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
N. Yorke-Smith – Promotor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
C. Bach – Promotor (Syddansk Universitet)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Type systems are a tool for preventing software errors, by classifying (sub)terms according to how they are evaluated. This way, mistakes can be caught at compile-time, ruling out the existence of entire classes of mistakes altogether. Using a programming language with a strong type system to develop critical software can dramatically reduce the prevalence and impact of bugs.
In light of the potentially enormous impact of bugs, it is important that we can trust a type system to be succesful in preventing errors. A key property of type systems that reflects this criterium is type soundness, which establishes that “well-typed programs cannot go wrong”. That is, programs that are deemed safe by the type system should not exhibit certain wrong behaviour when executed. To gain trust in a type system’s ability to prevent errors, we can give a formal system of both a language’s type system and semantics, and mathematically verify that the type system is sound with respect to the defined semantics. While this provides airtight evidence that a type system is succesful in ruling out certain mistakes, the formal specification and verification of programming languages requires a formidable amount of time and expertise on behalf of the language designer, and is therefore infeasible in most cases....