The Extension λ_ω_ (Lambda Weak Omega)

CONTENT This video is part of the playlist "Lambda Cube Unboxed", a series of 13 videos that explores and exposes the basics of (un-)typed λ-calculus including higher-order parametric polymorphism and dependent types. The resources, from which this video series extracts the offered material, are listed in the description of the playlist. This video (4): After discussing polymorphism in the previous two videos, we return to the simply typed lambda calculus to explore the notion of “types depending on types” as a different way of extending simple types. This leads us to a type system known as lambda weak omega. AUTHORS / OWNERS The slides and script of the videos were made by Michelle Döring, Felix Moebius and Falk Schimweg. The video was narrated and edited by Douglas Rouse. (Under supervision of Prof. Uwe Nestmann at the Technical University of Berlin.) © 2021 (CC-BY-NC-ND) Michelle Döring Felix Moebius Falk Schimweg Douglas Rouse