Towards a logical framework with intersection and union types