Proof theory of the lambda calculus
Filed under:
TALK
Prof. Masahiko Sato (Kyoto University, Japan), 17 October 2016, 1:30 p.m., RISC seminar room pond
When |
Oct 17, 2016
from 01:30 PM to 02:30 PM |
---|---|
Where | RISC seminar room pond |
Add event to calendar |
vCal iCal |
We develop a proof theory of the lambda calculus where we study the set of closed lambda terms by inductively defining the set as a free algebra. The novelty of the approach is that we construct and study lambda calculus without using the notions of variables and alpha-equivalence. In this approach we can study lambda terms as combinators and can have a clean proof of the Church-Rosser Theorem in the Minlog proof assistant.