This thesis embarks on a comprehensive exploration of formal computational models that underlie typed programming languages. We focus on programming calculi, both functional (sequential) and concurrent, as they provide a compelling rigorous framework for evaluating program semantics and for developing analyses and program verification techniques. This is the full version of the thesis containing appendices.

翻译：本论文对构成类型化编程语言基础的形式化计算模型展开全面探索。我们聚焦于编程演算——包括函数式（顺序）演算与并发演算——因其为评估程序语义、发展程序分析与验证技术提供了严谨而有力的框架。此为包含附录的论文完整版本。