Natural Deduction and Normalization Proofs for the Intersection Type Discipline
Logic in Computer Science
2019-04-24 v1
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.
Keywords
Cite
@article{arxiv.1904.10106,
title = {Natural Deduction and Normalization Proofs for the Intersection Type Discipline},
author = {Federico Aschieri},
journal= {arXiv preprint arXiv:1904.10106},
year = {2019}
}
Comments
In Proceedings DCM 2018 and ITRS 2018, arXiv:1904.09561