### System λ

The untyped Lambda Calculus

```
e ::=             terms:
  x               variable
  e e             application
  λ x . e         abstraction
```

### System λ→

The first-order simply typed Lambda Calculus (Propositional Calculus/Logic)

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)

```
k :: =            kinds:
  *               type of types

t ::=             types:
  a               variable
  t → t           arrow type

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
```

Where `bool : *` and `int : *`

```
idBool : bool → bool
idBool = λ x : bool . x

idInt : int → int
idInt = λ x : int . x
```

### System λΠ

The first-order dependently typed Lambda Calculus (Predicate Calculus/Logic)

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
- Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)

```
t ::=             types:
  a               variable
  t → t           arrow type
  Π x : t . e     abstraction

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
```

### System λ2

The second-order polymorphic typed Lambda Calculus (Propositional Calculus/Logic)

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
- Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)

```
k :: =            kinds:
  *               type of types

t ::=             types:
  a               variable
  t → t           arrow type

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
  e t             type application
  Λ a : k . e     type abstraction
```

### System λω_

The (weakly) higher-order (higher-kinded) typed Lambda Calculus (Propositional Calculus/Logic), Type Constructors

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
- Types depending on types (allows types to depend on types, i.e. types that can bind types)

```
k :: =            kinds:
  *               type of types
  k → k           arrow kind

t ::=             types:
  a               variable
  t → t           arrow type
  t t             application
  ∀ a : k . t     universal quantification

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
```

### System λΠ2 (λP2)

The second-order dependently typed polymorphic Lambda Calculus (Predicate Calculus/Logic)

λΠ + λ2

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
- Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
- Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)

### System λΠω_ (λPω_)

The (weakly) higher-order (higher-kinded) dependently typed Lambda Calculus (Predicate Calculus/Logic)

λΠ + λω_

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
- Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
- Types depending on types (allows types to depend on types, i.e. types that can bind types)

### System λω

The higher-order (higher-kinded) typed polymorphic Lambda Calculus (Propositional Calculus/Logic)

Standard ML, OCaml, F#, Nemerle, Haskell, Scala 2

λ2 + λω_

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
- Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)
- Types depending on types (allows types to depend on types, i.e. types that can bind types)

```
k :: =            kinds:
  *               type of types
  k → k           arrow kind

t ::=             types:
  a               variable
  t → t           arrow type
  t t             application
  ∀ a : k . t     universal quantification

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
  e t             type application
  Λ a : k . e     type abstraction
```

```
id : ∀ a : * . a → a
id = Λ a : * . λ x : a . x
```

### System λΠω (λPω, λC)

The higher-order (higher-kinded) dependently typed polymorphic Lambda Calculus (CoC - Calculus of Constructions)

Dependent ML, ATS, F*, Coq/Gallina, Matita, ALF, Cayenne, Epigram, Lean, LEGO, Agda, Idris, Ur/Web, Scala 3 (DOTty - Dependent Object Types)

λΠ + λ2 + λω_

- Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
- Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
- Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)
- Types depending on types (allows types to depend on types, i.e. types that can bind types)

```
e ::=
  x              variables
  *              type of types
  e e            application
  ∀ x : e . e    quantification (∀ + Π)
  λ x : e . e    abstraction (λ + Λ)
```