Combining type disciplines (Q1319505): Difference between revisions

This paper presents a type inference system for pure \(\lambda\)-calculus combining the main constructors: arrow, union, intersection, quantifiers and recursion. After a description in a natural-deduction style, this system is reformulated in a sequent-calculus style. Having shown the equivalence of these two descriptions, the authors use the sequent calculus to investigate preservation of types under reduction. This preservation fails for \(\beta\)-reduction, but is true for a notion of parallel reduction generalizing Gross-Knuth reduction based on complete developments. This is shown using a modification of Gentzen's proof of the Hauptsatz. A model for this system is provided using a \(D_ \infty\) model for \(\lambda\)-calculus, in which types are interpreted as special subsets. This is applied to check soundness of the system. Both syntactical and semantical studies are compared to be closely related work by MacQueen, Plotkin and Sethi, and the authors emphasize the simplifications brought about by the present framework.