# 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.