## Cube: Barendregt's Lambda-Cube

This directory contains the theory sources for the Lambda-Cube in Isabelle/Pure.

The `ex` subdirectory contains some examples.

NB: the formalization is not completely sound! It does not enforce distinctness of variable names in contexts!

For more information about the Lambda-Cube, see

- H. Barendregt
  Introduction to Generalised Type Systems
  J. Functional Programming