Wyniki wyszukiwania - BazTech

1

On Realisability Semantics for Intersection Types with Expansion Variables

Kamareddine F., Nour K., Rahli V., Wells J. B.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

153-184

EN

Expansion is a crucial operation for calculating principal typings in intersection type systems. Because the early definitions of expansion were complicated, E-variables were introduced in order to make the calculations easier to mechanise and reason about. Recently, E-variables have been further simplified and generalised to also allow calculating other type operators than just intersection. There has been much work on semantics for type systems with intersection types, but none whatsoever before our work, on type systems with E-variables. In this paper we expose the challenges of building a semantics for E-variables and we provide a novel solution. Because it is unclear how to devise a space of meanings for E-variables, we develop instead a space of meanings for types that is hierarchical. First, we index each type with a natural number and show that although this intuitively captures the use of E-variables, it is difficult to index the universal type ωwith this hierarchy and it is not possible to obtain completeness of the semantics if more than one E-variable is used. We then move to a more complex semantics where each type is associated with a list of natural numbers and establish that both ů and an arbitrary number of E-variables can be represented without losing any of the desirable properties of a realisability semantics.

2

Arithmetical Proofs of Strong Normalization Results for Symmetric [lambda]-calculi

David R., Nour K.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 4

489-510

EN

We give arithmetical proofs of the strong normalization of two symmetric l-calculi corresponding to classical logic. The first one is the [`(l)]m[(m~)]-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric lm-calculus. It is the lm-calculus introduced by Parigot in which the reduction rule m?, which is the symmetric of m, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.

3

A Short Proof of the Strong Normalization of the Simply Typed lambda mi-calculus

David R., Nour K.

Schedae Informaticae

|

2003

|

Vol. 12

27-33

EN

We give an elementary and purely arithmetical proof of the strong normalization of Parigot's simply typed lambda-calculus.