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

Concept# Simply typed lambda calculus

Résumé

The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) 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). In contrast, systems which introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered simply typed. The simple types, except for full recursion, are still considered simple because the Church encodings of such structures can be done using only \to and suitable type variables, while po

Source officielle

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.

Publications associées

Chargement

Personnes associées

Chargement

Unités associées

Chargement

Concepts associés

Chargement

Cours associés

Chargement

Séances de cours associées

Chargement

Publications associées (9)

Personnes associées (1)

Chargement

Chargement

Chargement

Unités associées (1)

Concepts associés (20)

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éma

Lambda-calcul

Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application. On y manipule des expressions appelées λ-expr

Correspondance de Curry-Howard

La correspondance de Curry-Howard, appelée également isomorphisme de Curry-de Bruijn-Howard, correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière e

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.

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

Séances de cours associées (8)

Cours associés (3)

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

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into the new web standard for portable binaries called WebAssembly ( https://webassembly.org/ )

Philippe Altherr, Vincent Cremet

This paper studies the interplay between inner classes and virtual types. The combination of these two concepts can be observed in object-oriented languages like Beta or Scala. This study is based on a calculus of classes and objects composed of a very limited number of constructs. For example the calculus has neither methods nor class constructors. Instead it has a more general concept of abstract inheritance which lets a class extend an arbitrary object. Thanks to an interpretation of terms as types the calculus also unifies type fields and term fields. The main contribution of this work is to show that typing virtual types in the presence of inner classes requires some kind of alias analysis and to formalize this mechanism with a simple calculus.

2005