Lam

A formally verified interpreter for Lambda Calculus.

Dependencies: agda2hs version 1.2.

Build with the build.sh script.

Roadmap

Basics

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

Features

• Simple Types
• Verify properties using Agda (Progress/Preservation)
• Extensions (TaPL ch 11)
  • Uninterpreted (opaque) Types
  • Numbers, booleans, ITE, ltNat
  • Pairs
  • Sums
  • Pattern Matching
  • General recursion
• More preprocessing besides erasing names (enable larger sums or products, for instance)
• Polymorphism
• Recursive Types (Enabling strings)
• Library of examples

Usability

• Editor Support
  • Syntax Highlight (Vim, Emacs)
  • Language Server Protocol
• Package Manager
• Nicer REPL
  • Interpret arrows
  • Autocomplete
• Code Generation
• Support for commentary
• Specific error nessages
  • Lexer
  • Parser
  • Type checker
• Documentation
• Commands
  • Eval
  • Define
  • Load
  • Typedef
  • Read

Future Work

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