# Natural Deduction and Normalization Proofs for the Intersection Type Discipline

## TL;DR

This paper develops a systematic approach to intersection types using natural deduction, linking beta reduction steps to Prawitz reductions, and proves normalization theorems for systems D and Omega.

## Contribution

It introduces a new natural deduction framework for intersection types and derives normalization results directly from typing derivations.

## Key findings

- Beta reduction corresponds to Prawitz reductions in derivations
- System D is strongly normalizing
- System Omega terminates leftmost reductions for typable terms

## Abstract

Refining and extending previous work by Retor\'e, we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as performing, at the level of typing derivations, Prawitz reductions in parallel. Then we derive as immediate consequences of Subject Reduction the main theorems about normalization for intersection types: for system D, strong normalization, for system Omega, the leftmost reduction termination for terms typable without Omega.