A General Approach to Define Binders Using Matching Logic

on YouTube ↗15m

" summary

Defines binders by using matching logic’s built‑in exists to form the graph set [X]E and then a constructor to build the binder term, encapsulated as the theory Gamma_lambda. Proves conservative extension so equational proofs coincide with lambda calculus, proves soundness and completeness of the theory, and gives representational completeness: for every lambda theory T there is a matching‑logic model M_T that satisfies exactly T and for every concrete CCC model A there is a corresponding matching‑logic model M_A.

AI-written summary · about

" chapters (4)

1. 0:00Start
2. 0:30Motivation: K and Matching Logic
3. 2:47Main Contribution 1. We propose a simple variant of matching logic that is more suitable to capture binders (Sections 3-4).
4. 5:55Overview of the Talk