Why Type Soundness Matters in Functional Programming Languages

This article outlines the typing rules for two minimal languages, Fun and Core, focusing on type soundness, control flow constructs, and the translation of typeability between them. It also explores how producer/consumer variables and codata types are handled within a formal sequent calculus framework.

Table of Links

A. The Relationship to the Sequent Calculus

B. Typing Rules for Fun

C. Operational Semantics of label/goto

References

4 Typing Rules

In this section, we introduce the typing rules for Fun in Section 4.1 and for Core in Section 4.2. In Section 4.3 we state type soundness for both languages and prove that the translation from Fun to Core preserves the typeability of programs. We use the same constructors, destructors, types and typing contexts for both Fun and Core, which are summarized in Definition 4.1. Note that we distinguish between producer and ...