Kripke-style semantics in typed lambda calculus, combinatory logic and more

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 new 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, [1]. This approach is extended to typed combinatory logic, [2].
Building on the previous results, we develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed combinatory terms as basic propositions, along with the semantics based on applicative structures extended with special elements corresponding to primitive combinators. Both the equational theory of untyped combinatory logic and the proposed axiomatic system are proved to be sound and complete w.r.t. the given semantics. In addition, we prove that combinatory logic is sound and complete w.r.t. the given semantics.
This is joint work with Simona Kasterovic.