Computability in Europe 2008
Logic and Theory of Algorithms 

Regular Talk:

Speaker:  Anastasia Veneti 
Author(s):  Anastasia Veneti and Yiorgos Stavrinos 
Slot:  Tue, 11:0011:20, Room 22 (col. 4) 
We present a logical formalism for the
intersection and union type assignment system IUT [1]. A
first attempt to this end is the
intersection and union logic IUL, a logic whose main structures are binary
trees called kits [3,4]. The rules of IUL are in natural
deduction style and are categorized as global or
local according to whether they affect all leaves of the
kits involved or not. While rules for the intersection and union are meant to
be local, the complex notation of kits conceals a certain kind of globality
inherent in the union elimination rule. This becomes explicit if we abandon
kits and resort to the linear structures employed in [2]. These structures are
multisets of judgements (atoms) called
molecules. A logic for IUT using molecules, but still in
natural deduction style, incorporates a union elimination
rule
[(Γ_{i} ⊢
φ_{i})]_{i}
∪
[(Γ ⊢ σ ∪ τ)]
[(Γ_{i}, φ_{i}
⊢ ψ_{i})]_{i}
∪
[(Γ, σ ⊢ ρ),(Γ,
τ ⊢ ρ)]

(∪E)
[(Γ_{i} ⊢
ψ_{i})]_{i} ∪
[(Γ ⊢ ρ)]
which has both a global and a local behaviour. Here globality and locality
refer to the number of atoms modified by the rule in the premise molecules.
In the present work we describe IUL with molecules
in sequent calculus style. The main advantage of this formulation is that
globality and locality of the union elimination rule are separated in the
cut rule
and left union rule, respectively.
[(Γ_{i} ⊢
φ_{i})]_{i}
[(Γ_{i}, φ_{i}
⊢
ψ_{i})]_{i}

(cut)
[(Γ_{i} ⊢
ψ_{i})]_{i}
M ∪ [(Γ, σ ⊢
ρ),(Γ,
τ ⊢ ρ)]

(L∪)
M ∪ [(Γ, σ ∪
τ ⊢ ρ)]
These improvements lead the way in yielding the
relation of IUT to the logic IUL.
References
[1] Barbanera F., DezaniCiancaglini M., and de'Liguoro U., Intersection and Union Types: Syntax and Semantics, Information and Computation 119, 202230 (1995)
[2] Pimentel E., Ronchi Della Rocca S., and Roversi L., Intersection Types from a prooftheoretic perspective, 4th Workshop on Intersection Types and Related Systems, Torino (2008)
[3] Ronchi Della Rocca S. and Roversi L., Intersection Logic, Proceedings of CSL'01, LNCS 2142, 414428 (2001)
[4] Veneti A. and Stavrinos Y., Towards an intersection and union logic, 4th Workshop on Intersection Types and Related Systems, Torino (2008)
websites: Arnold Beckmann  20080615 