Skip to content

Dependently Typed Lambda Calculus in Haskell

License

Notifications You must be signed in to change notification settings

DeSevilla/lambdapi

 
 

Repository files navigation

Dependently Typed Lambda Calculus

This project is reorganization of the source code for the paper A Tutorial Implementation of a Dependently Typed Lambda Calculus.

The goal of this project is to make code readable and understandable.

An interested reader may also look at this darcs repo.

The goal of this project is to make reading and navigation of the code as simple as possible.

How to play with examples

Simply Typed Lambda Calculus

$ stack run st
Interpreter for the simply typed lambda calculus.
Type :? for help.
ST> :load prelude.st

Dependently Typed Lambda Calculus

$ stack run lp
Interpreter for lambda-Pi.
Type :? for help.
LP> :load prelude.lp

About

Dependently Typed Lambda Calculus in Haskell

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Haskell 98.7%
  • Smalltalk 1.3%