Introduction to Tarski's High School Algebra Problem. Review of decidability and finite axiomatizability results for (fragments of) it. Type isomorphisms. Connections between the fragments and typed lambda calculi with product and sum types. Discussion on NBE (Danvy's TDPE) for sum types w.r.t. the the presented material. Calculations with the Agda version of the TDPE for CBN lambda callculus with sums. Reading material corresponding to the lectures:
Agda code corresponding to this day to be added once the homework deadline has passed. |