RUS  ENG
Full version
SEMINARS

Seminars "Proof Theory" and "Logic Online Seminar"
December 12, 2022 18:30, Moscow, Steklov Mathematical Institute (8 Gubkina), room 313 + Zoom


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

Silvia Ghilezan

University of Novi Sad



Abstract: 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.

Language: English

References
  1. Simona Kasterovic, Silvia Ghilezan, “Kripke semantics and completeness for full simply typed lambda calculus”, Journal of Logic and Computation, 30:8 (2020), 1567–1608  crossref
  2. Silvia Ghilezan, Simona Kasterovic, “Semantics for combinatory logic with intersection types”, Frontiers in Computer Science, 4 (2022)  crossref


© Steklov Math. Inst. of RAS, 2024