Lam

A formally verified interpreter for Lambda Calculus.

Dependencies: agda2hs version 1.2.

Build with the build.sh script.

Roadmap

Infrastructure

• Lexer
• Parser
• Tests
  • Parser
  • Evaluator
• De Bruijn Indices
• Basic formalization
  • Type checker
  • Evaluator

Features

• Simple Types
• Extensions (TaPL ch 11)
  • Uninterpreted (opaque) Types
  • Numbers, booleans, ITE
  • Equality, Strings
  • Pairs
  • Sums
  • General recursion
  • Pattern Matching
• Polymorphism
• Verify properties using Agda (Progress/Preservation)
• Library of examples

Usability

• Code Generation
• Support for commentary
• Error messages
• Commands
  • Eval
  • Define
  • Load
  • Typedef

Future Work

• DAG instead of AST
• System F omega
• Type Inference
• Type Classes
• Dependent Types