done | next |

- The usual definition of lambda-terms
- We are mostly interested in closed lambda-terms
- Actually, we are mostly interested in equivalence classes
- Definition of equivalence classes
- A different definition of lambda-terms
- Examples of lambda-terms
- The usual definition of types
- A different definition of types
- Examples of types
- Change the notation for pictures of types
- Redrawing ((B->C)->((A->B)->(A->C))
- Redrawing ((A->(B->C))->(B->(A->C)))
- A surprising observation
- The transformation from BCI-nf to their types
- Typing B
- Typing C
- Data structure for implementation
- Pseudo-code for parsing BCI-nf terms
- Pseudo-code for printing types
- Conclusion

change style |