文章基本信息

标题：Intersection Types for the lambda-mu Calculus
本地全文：下载
作者：de'Liguoro, Ugo ; Barbanera, Franco ; van Bakel, Steffen 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2018
卷号：14
期号：1
语种：English
出版社：Technical University of Braunschweig
摘要：We introduce an intersection type system for the lambda-mu calculus that isinvariant under subject reduction and expansion. The system is obtained bydescribing Streicher and Reus's denotational model of continuations in thecategory of omega-algebraic lattices via Abramsky's domain-logic approach. Thisprovides at the same time an interpretation of the type system and a proof ofthe completeness of the system with respect to the continuation models by meansof a filter model construction. We then define a restriction of our system,such that a lambda-mu term is typeable if and only if it is stronglynormalising. We also show that Parigot's typing of lambda-mu terms withclassically valid propositional formulas can be translated into the restrictedsystem, which then provides an alternative proof of strong normalisability forthe typed lambda-mu calculus.
关键词：F.4.1;F.4;Computer Science - Logic in Computer Science