Advanced Topics in Category Theory

Part I

Study material

M Fiore. Rough notes on presheaves.
F Loregian. Coend calculus.
M Fiore, G Plotkin and D Turi. Abstract syntax and variable binding.
M Fiore and D Szamozvancev. Formal metatheory of second-order abstract syntax.
M Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. [conference paper] [journal paper]
M Fiore. A normalisation-by-evaluation program for typed lambda calculus in Agda. [note] [agda code] [agda code (bis)]