Kripke-style Semantics and Completeness for Full Simply Typed Lambda Calculus
Simona Kašterović, Silvia Ghilezan · Journal of Logic and Computation · 2020
Abstract Full simply typed lambda calculus is the simply typed lambda calculus extended with product types and sum types. We propose a Kripke-style semantics for full simply typed lambda calculus. We then prove soundness and completeness of type assignment in full simply typed lambda calculus with respect to the proposed semantics. The key point in the proof of completeness is the notion of a canonical model.