Skip to content

Single file Lambda Calculus implementations demonstrating various type system features and interpretation techniques

License

Notifications You must be signed in to change notification settings

solomon-b/lambda-calculus-hs

Repository files navigation

Lambda Calculus Examples

A series of Lambda Calculus implementations starting from Simply Typed evaluation, then work up through bidirectional typechecking, normalization by evaluation, elaboration and then various type system extensions.

The goal is to provide best practices examples of all the features you might want to include in your custom language in one place.

  • SimplyTypedEvaluation
  • BidirectionalTypechecking
  • NormalizationByEvaluation
  • Elaboration
  • TypedHoles
  • SystemT
  • Records
  • Subtyping
  • Inductive Types (with eliminator based pattern matching)
  • Row Polymorphism
  • System F
  • System Omega
  • Linear Types
  • Case-Trees
  • Martin-Lof Type Theory (Pi and Sigma Types)
  • Equality

About

Single file Lambda Calculus implementations demonstrating various type system features and interpretation techniques

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published