20/11/2001: Jerzy Tiuryn (Univ. Varsovie)
Products and Polymorphic Subtypes.
Résumé
The talk will be devoted to a study of polymorphic subtypes with
products. We give a sound and complete Hilbert style axiomatization of
the relation of being a subtype.
The semantics we use is based on
logical relations over applicative structutes with projections.
We
propose a new form of a sequent which plays a key role in the natural
deduction and Gentazen style calculus for the sybtyping relation on
polymorphic types with product.
During the talk we will discuss the
basic metamathematical properties of the system: subject reduction,
cut elimination, decidability/undecidability issues.