Practical foundations for programming languages

Robert Harper

2016

A mathematically rigorous treatment of programming language theory grounded in proof theory and type theory. Defines language concepts through static and dynamic semantics using only elementary mathematics.