Ph.D. Thesis
The computational core: reduction theory and intersection type discipline