Natural Deduction and Normalization Proofs for the Intersection Type Discipline

Federico Aschieri

Refining and extending previous work by Retoré, 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.

In Michele Pagani and Sandra Alves: Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems (DCM 2018 and ITRS 2018 ), Oxford, UK, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 293, pp. 29–37.
Published: 23rd April 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: