Seminars
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
Calendar
Search
Add a seminar

RSS
Forthcoming 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
Video records:
MP4 190.5 Mb

Number of views:
This page:141
Video files:38



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
 
  Contact us:
 Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024