lambdacube

Implementation Lambda Calculus with various type systems: from simple type lambda up to lambda with dependency types.

It's research project which aims to study various types systems.

Goals:

Implement follow type system:

• pure lambda (without types)
• simple typed lambda calculus
• STLC with Dependency Types
• Linear types

Based on

• Lambda Calculus

Greg Michaelson
AN INTRODUCTION TO FUNCTIONAL PROGRAMMING THROUGH LAMBDA CALCULUS
https://pdfs.semanticscholar.org/d986/546bc3780db3a3c0f8d88b35e421ae4eec21.pdf

• System F + Polymorphic Type System

Types and Programming Languages 
Benjamin C. Pierce
http://www.cis.upenn.edu/~bcpierce/tapl/

• STLC with Dependency Typed

A Tutorial Implementation of a Dependently Typed Lambda Calculus
Andres Löh, Conor McBride and Wouter Swierstra
http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf

• Linear types

'Use-Once' Variables and Linear Objects -- Storage Management, Reflection and Multi-Threading
http://www.pipeline.com/~hbaker1/Use1Var.html

A Brief Introduction to Linear Programming
https://www.courses.psu.edu/for/for466w_mem14/Ch11/HTML/Sec1/ch11sec1.htm