Kripke-style semantics in computation

Kripke-style semantics have gained an important role and wide applicability in logic and computation since they were introduced by Saul Kripke in the late 1950s as semantics for modal logics. In logic, these semantics were later adapted to intuitionistic logic and other non-classical logics. In computation, a class of Kripke-style models was defined for typed lambda calculus. In this talk, we present a novel approach to Kripke semantics for simply typed lambda calculus endowed with conjunction, disjunction and negation. We show soundness and completeness of this typed lambda calculus w.r.t. the proposed semantics. Further, we discuss this semantics for typed combinatory logic and logic of combinatory logic, a logic for reasoning about combinatory logic.

Silvia Ghilezan

Last modified: Mon Feb 17 2025