Lambda Calculus: Syntax and Abstractions

This lecture covers the syntax and semantics of the lambda calculus, a fundamental model of computation. It introduces terms, abstractions, applications, and values in the pure lambda calculus, emphasizing the power of functions as the building blocks of computation. The lecture explores the scoping rules of lambda abstractions, the curried style for multi-argument functions, and the operational semantics for function application. It also discusses the significance of the lambda calculus as the foundation for functional programming languages like ML, Haskell, and Scheme.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related lectures (46)

Related concepts (95)

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr

Lambda cube

In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to: x-axis (): types that can bind terms, corresponding to dependent types.

Calculus of constructions

In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants. Some of its variants include the calculus of inductive constructions (which adds inductive types), the calculus of (co)inductive constructions (which adds coinduction), and the predicative calculus of inductive constructions (which removes some impredicativity).

Lambda calculus

Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. Lambda calculus consists of constructing lambda terms and performing reduction operations on them.

Operational semantics

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics).

Pure type system

NOTOC In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of Barendregt's lambda cube, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts. In fact, Barendregt (1991) framed his cube in this setting.

Logic and Sets

Introduces logic, sets, and their operations, including subsets, Cartesian product, and set equivalence.

Weyl character formula MATH-680: Monstrous moonshine

Explores the proof of the Weyl character formula for finite-dimensional representations of semisimple Lie algebras.

Differential Forms Integration MATH-410: Riemann surfaces

Covers the integration of differential forms on smooth manifolds, including the concepts of closed and exact forms.

Open Mapping Theorem MATH-410: Riemann surfaces

Explains the Open Mapping Theorem for holomorphic maps between Riemann surfaces.

Local Homeomorphisms and Coverings MATH-410: Riemann surfaces

Covers the concepts of local homeomorphisms and coverings in manifolds, emphasizing the conditions under which a map is considered a local homeomorphism or a covering.