[an error occurred while processing this directive] An error occured whilst processing this directive

LFCS Theory Seminar
Room 6206, JCMB, King's Buildings
3pm, Thursday 4th December 1997

(* NOTE NONSTANDARD DAY, TIME AND ROOM *)

Title: Operational interpretation of recursive subtyping

Speaker: Fritz Henglein (DIKU, U. of Copenhagen)

We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule, which captures a coinduction principle: it has has the form

A, P |- P
---------
A |- P
where P is either a type equality t = t' or type containment t <= t'. We define what it means for a proof to be _contractive_ and show that the fixpoint rule is _sound_ if the proof of the antecedent A, P |- P is contractive in a formal sense. (A proof of A, P |- P using the assumption axiom is, of course, _not_ contractive.) The fixpoint rule allows us to capture a coinductive relation in the fundamentally inductive framework of inference systems.

The axiomatizations give rise to a natural operational interpretation of proofs as coercions, where the fixpoint rule corresponds to definition by recursion.

We sketch two applications of the axiomatization and its coercion interpretation, one theoretically, the other practically motivated.

Joint work with Michael Brandt, Prolog Development Center.

[References:

Brandt, Michael and Henglein, Fritz, "Coinductive axiomatization of recursive type equality and subtyping," Proc. 3d Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), Nancy, France, April 2-4, 1997, Springer LNCS 1210, pp. 63-81

Brandt, Michael, "Recursive Subtying: Axiomatizations and Operational Interpretation", Master's Thesis, DIKU, U. of Copenhagen, Sep. 1997, 132 pp.]

An error occured whilst processing this directive