A formally verified interpreter for Lambda Calculus.
Dependencies: agda2hs version 1.2.
Build with the build.sh
script.
- Lexer
- Parser
- Tests
- Parser
- Evaluator
- De Bruijn Indices
- Basic formalization
- Type checker
- Evaluator
- 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
- Code Generation
- Support for commentary
- Error messages
- Commands
- Eval
- Define
- Load
- Typedef
- DAG instead of AST
- System F omega
- Type Inference
- Type Classes
- Dependent Types