2009 | OriginalPaper | Buchkapitel
A Polymorphic Type System for the Lambda-Calculus with Constructors
verfasst von : Barbara Petit
Erschienen in: Typed Lambda Calculi and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present a Curry-style second-order type system with union and intersection types for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an extension of lambda-calculus with a pattern matching mechanism for variadic constructors. To prove the strong normalisation property for this system, we translate well-typed terms in an auxiliary calculus of case-normal forms using the interpretation method. We finally prove the strong normalisation property for the auxiliary calculus using the standard reducibility method.