UC San Diego

Formalizing the semantics of a programming language enables powerfultechniques for understanding the correctness of tooling related to that language (e.g. compilers) as well as for understanding the correctness of programs written in that language. Traditional approaches to formalizing semantics lead to the production of monolithic systems whose components are difficult to reuse. In this dissertation we describe Gazelle, a system for composing programming-language semantics out of reusable fragments. Gazelle demonstrates an approach to surmounting these obstacles, enabling greater reuse and thus potentially more efficient development of formalized language semantics. Through an extended example, we show the usage of Gazelle in practice to formalize the Imp language and prove the correctness of an iterative Imp program. The entire development of Gazelle is done in Isabelle, and all key results are foundationally verified with machine-checked proofs.