Lambdascope -- Another optimal implementation of the lambda-calculus
目次。
- Introduction
- λ-calculus
- From terms to nets
- Interaction net reduction
- From nets to terms
- Static correctness
- Directed nets
- Tree nets
- The automaton
- Reading back trees
- Binding loops
- λ-nets
- △≅▲
- Dynamic correctness
- Related and further work
- Optimal vs. efficient
- Disconnected vs. connected scopes
- The ideal explicit substitution calculus?
- Scoping first vs. replication first
- Conclusion