Typed lambda calculus | EPFL Graph Search

Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?

Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.

Découvrez-en plus sur les applications Graph.

A typed lambda calculus is a typed formalism that uses the lambda-symbol () to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type. Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages such as ML and Haskell and, more indirectly, typed imperative programming languages. Typed lambda calculi play an important role in the design of type systems for programming languages; here, typability usually captures desirable properties of the program (e.g., the program will not cause a memory access violation). Typed lambda calculi are closely related to mathematical logic and proof theory via the Curry–Howard isomorphism and they can be considered as the internal language of certain classes of . For example, the simply typed lambda calculus is the language of (CCCs) Various typed lambda calculi have been studied. The simply typed lambda calculus has only one type constructor, the arrow , and its only types are basic types and function types . System T extends the simply typed lambda calculus with a type of natural numbers and higher order primitive recursion; in this system all functions provably recursive in Peano arithmetic are definable. System F allows polymorphism by using universal quantification over all types; from a logical perspective it can describe all functions that are provably total in second-order logic. Lambda calculi with dependent types are the base of intuitionistic type theory, the calculus of constructions and the logical framework (LF), a pure lambda calculus with dependent types.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (31)

Système F

Le est un formalisme logique qui permet d'exprimer de façon très riche et très rigoureuse des fonctions et d'y démontrer formellement des propriétés difficiles. Plus précisément, le (également connu sous le nom de lambda-calcul polymorphe ou de lambda-calcul du second ordre) est une extension du lambda-calcul simplement typé introduite indépendamment par le logicien Jean-Yves Girard et par l'informaticien John C. Reynolds. Ce système se distingue du lambda-calcul simplement typé par l'existence d'une quantification universelle sur les types qui permet d'exprimer du polymorphisme.

Simply typed lambda calculus

The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. The term simple type is also used to refer extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF).

Type dépendant

En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé. Les langages Agda et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. Les types dépendants permettent par exemple de définir le type des listes à n éléments. Voici un exemple en Coq. Inductive Vect (A: Type): nat -> Type := | nil: Vect A 0 | cons (n: nat) (x: A) (t: Vect A n): Vect A (S n).

Cours associés (7)

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

FIN-406: Macrofinance

This course provides students with a working knowledge of macroeconomic models that explicitly incorporate financial markets. The goal is to develop a broad and analytical framework for analyzing the

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 thr

Afficher plus

Séances de cours associées (75)

Système F

Simply typed lambda calculus

Type dépendant

Séance papier et stylo: Lambda Calculus Proofs CS-452: Foundations of software

Plonge dans Lambda Calculus preuves, mettant l'accent sur l'induction structurelle et la manipulation variable.

Codage de la récursivité comme auto-application CS-210: Functional programming

Explore le calcul lambda, les fonctions d'ordre supérieur et l'encodage récursif des fonctions.

Formules logiques et types: comprendre l'isomorphisme de Kerry Howard CS-452: Foundations of software

Explore l'isomorphisme de Kerry Howard, traduisant des propositions logiques en types et en termes, en mettant l'accent sur la preuve par induction et la préparation à l'examen.