Skip to content

Latest commit

 

History

History
53 lines (36 loc) · 1.24 KB

README.md

File metadata and controls

53 lines (36 loc) · 1.24 KB

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.

alt lambda_cube.png

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