Index of /ports/math/isabelle/work/Isabelle/src/Cube

 Name                    Last modified       Size  Description

 Parent Directory        09-Aug-2008 06:09      -  
 Cube.thy                05-Sep-2005 08:38     4k  
 Cube.thy.html           09-Aug-2008 06:09     0k  
 Example.thy             17-Sep-2005 03:50     6k  
 Example.thy.html        09-Aug-2008 06:09     0k  
 IsaMakefile             17-Sep-2005 03:50     1k  
 IsaMakefile.html        09-Aug-2008 06:09     2k  
 ROOT.ML                 17-Sep-2005 03:50     1k  
 ROOT.ML.html            09-Aug-2008 06:09     0k  

Cube: Barendregt's Lambda-Cube

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