Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Séance de cours

Types dans Lambda Calculus

Dans cours

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 ...

Description

Cette séance de cours introduit le concept de types dans le calcul lambda, en se concentrant sur deux langages dexemples: taper des expressions arithmétiques et simplement taper le calcul lambda. L'instructeur explique comment définir des types, spécifier des règles de frappe et prouver la solidité. La séance de cours couvre des sujets tels que les règles d'évaluation, la sécurité de type, l'algorithme de vérification de type, les formes canoniques, la progression, la préservation et les propriétés de la relation de frappe.

Enseignant·e·s (2)

Martin Odersky

Martin Odersky heads the programming research group at EPFL. His research interests cover fundamental as well as applied aspects of programming languages. They include semantics, type systems, programming language design, and compiler construction. The main focus if his work lies in the integration of object-oriented and functional programming. His research thesis is that the two paradigms are just two sides of the same coin and should be unified as much as possible. To prove this he has experimented a number of language designs, from Pizza to GJ to Functional Nets. He has also influenced the development of Java as a co-designer of Java generics and as the original author of the current javac reference compiler. His current work concentrates on the Scala programming language, which unifies FP and OOP, while staying completely interoperable with Java and .NET. Martin Odersky got his doctorate from ETHZ, in 1989. He held research positions at the IBM T.J. Watson Research Center from 1989 and at Yale University from 1991. He was then a professor at the University of Karlsruhe from 1993 and at the University of South Australia from 1997. He joined EPFL as full professor in 1999. He is associate editor of the Journal of Functional Programming and member of IFIP WG 2.8. He was conference chair for ICFP 2000, and program chair for ECOOP 2004 as well as ETAPS/CC 2007.

Sébastien Jean Robert Doeraene

Source officielle

Proximité ontologique

Informatique théorique

Théorie des langages de programmation: Langage de programmation de haut niveau

Concepts associés (32)

Type system

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

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).

Théorie des types

En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduits pour résoudre le paradoxe d'un axiome de compréhension non restreint. En théorie des types, il existe des types de base et des constructeurs (comme celui des fonctions ou encore celui du produit cartésien) qui permettent de créer de nouveaux types à partir de types préexistant.

Sûreté du typage

La sûreté du typage est un principe permettant d'améliorer la qualité de la programmation. Dans les langages à typage statique, l'un des objectifs est d'intercepter les erreurs de type de données lors de la compilation. Un type peut être vu comme un ensemble de valeurs et un ensemble d'opérateurs. La programmation objet a introduit les notions d'objets, messages, classes, héritage. Il est tentant de faire coller les classes à des types.

Strong and weak typing

In computer programming, one of the many ways that programming languages are colloquially classified is whether the language's type system makes it strongly typed or weakly typed (loosely typed). However, there is no precise technical definition of what the terms mean and different authors disagree about the implied meaning of the terms and the relative rankings of the "strength" of the type systems of mainstream programming languages.

Afficher plus

Séances de cours associées (53)

Vérification de type et reconstruction: équations et unification

S'intéresse à la vérification de type, à la reconstruction, aux équations, à l'unification, au système Hindley/Milner, au polymorphisme et aux principaux types.

Programmation Fonctionnelle Vérifiée : Nicolas Voirol défense de thèse de doctorat publique

Explore la programmation fonctionnelle vérifiée, la vérification formelle, les résolveurs SMT, la vérification de type, les fonctionnalités Scala, l'automatisation et les types dépendants.

Lambda Calculus: Numéros d'église

Explore les chiffres de l'église, les booléens, les paires, la récursion et l'équivalence comportementale dans Lambda Calculus.

Type Systems: Règles de conservation et de dactylographie

Couvre la préservation, la substitution, l'affaiblissement et le séquençage dans les systèmes de type.

Formules logiques et types: comprendre l'isomorphisme de Kerry Howard

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.

Afficher plus

Concepts associés (32)

Type system

Simply typed lambda calculus

Théorie des types

Sûreté du typage

Strong and weak typing

Afficher plus