Concept# Lambda calculus

Summary

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. In the simplest form of lambda calculus, terms are built using only the following rules:
# x : Some lambda term, a character or string representing a parameter, or mathematical/logical value.

# (\lambda x.M): A lambda abstraction is a function definition M, where the x between the λ and the punctum (the dot .) will need explicit substitution in M itself. (See

Official source

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 publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related publications (39)

Loading

Loading

Loading

Related concepts (119)

Related courses (31)

Functional programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function d

Algorithm

In mathematics and computer science, an algorithm (ˈælɡərɪðəm) is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algo

Mathematical logic

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research i

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 program part or a language. Students will learn how to apply these concepts in their reasoning.

CS-119(c): Information, Computation, Communication

L'objectif de ce cours est d'introduire les étudiants à la pensée algorithmique, de les familiariser avec les fondamentaux de l'Informatique et de développer une première compétence en programmation (langage C++).

CS-210: Functional programming

Understanding of the principles and applications of functional programming, the fundamental models of program
execution, application of fundamental methods of program composition, meta-programming through the construction of
interpreters and advanced programming techniques.

Guillaume André Fradji Martres

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not enough to declare a particular subset of the language as sound. While a few examples of Scala snippets have been manually translated into DOT, no systematic compilation scheme has been presented so far. In this report we take advantage of the fact that the Featherweight Generic Java (FGJ) calculus can be seen as a subset of Scala (you just have to squint a little bit!) and present a compilation scheme from cast-less FGJ into DOT as well as a proof that a well-typed cast-less FGJ program compiles down to a well-typed DOT term. Due to limitations in DOT subtyping rules, this requires imposing one limitation on our source program: the type parameters of the base types of a class can never refer back to the class itself (this excludes class C extends B[C] as well as class D extends B[E]; class E extends D). While this result is not especially interesting by itself given that FGJ is already known to be sound, it is a first step towards establishing soundness for larger subsets of Scala like the Pathless Scala calculus, the author plans to pursue this in his thesis (currently under preparation) which will also include the content of this report. It also clearly illustrates limitations in DOT that future work may wish to focus on.

2022Related people (3)

, ,

Related units (2)

Guillaume André Fradji Martres, Martin Odersky, Dmytro Petrashko

dotty is a new, experimental Scala compiler based on DOT, the calculus of Dependent Object Types. Higher-kinded types are a natural extension of first-order lambda calculus, and have been a core construct of Haskell and Scala. As long as such types are just partial applications of generic classes, they can be given a meaning in DOT relatively straightforwardly. But general lambdas on the type level require extensions of the DOT calculus to be expressible. This paper is an experience report where we describe and discuss four implementation strategies that we have tried out in the last three years. Each strategy was fully implemented in the dotty compiler. We discuss the usability and expressive power of each scheme, and give some indications about the amount of implementation difficulties encountered.

SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes type safety unclear. The goal of this thesis is to initiate a rigorous and formal process of validation of the SCALA type system. The correctness of a type system can only be established in relation to a formal description of a program execution. The first contribution of this thesis is the definition of a formal semantics for SCALA, by translation in a minimal class-based calculus. SCALA offers two means for expressing type abstraction: type parameters and type members, also called virtual types. Virtual types seem more primitive since they allow to encode type parameters whereas the existence of a reverse encoding is not clear. The soundness of virtual types has been the object of a long debate in the community; they are now commonly believed to be safe, but at this time, there exists no formal argument that would confirm this belief. The second contribution of this thesis is to provide a formal proof of type safety for virtual types.

Related lectures (72)