The Theory of Twiners and Linear
Parametricity (Note)
Ryu Hasegawa
Graduate School of Mathematical Sciences, The University of Tokyo, Komaba 3-8-1,
Meguro-ku, Tokyo 153-8914, Japan

1 Introduction
We want to show that solutions of domain equations, or equivalently existenceof recursive types, can be derived from a computer theoretic concept, called theprinciple of linear parametricity. Existence of recursive types has applicationsin, for example, semantics of functional programming, type-theoretic study ofobject-oriented programming, and the theory of programme transformation, as
reviewed in the following. In usual, the existence of recursive types is ensured
using a mathematical theory of Scott domains or alike. Our innovation lies inthat it can be derived from a more computer theoretic concept. In this work,
we focus on giving a model satisfying the principle of linear parametricity in areasonable sense, leaving more syntax-oriented matters such as axiomatization
to a future work.
In many activities of computing, we often need the structures de ned recursively. Simple data structures such as lists, trees, and even natural numbers areexamples of recursively de ned data. These examples are rather easily rationalized, since they are given as xed points of operators where indeterminates
occur only positively. A naive set-theoretic understanding is sucient for themin most occasions.
A more challenging problem is whether we can give rationale for xed points ofoperators that may contain negative occurrences as well. One of early speculations leading to this problem was to provide semantics for the untyped lambda
calculus. The calculus has a rather peculiar structure where functions anddata have no distinction and everything can be applied to everything. Thisobservation leads us to the fact that giving semantics of the untyped lambda
calculus amounts to detecting an entity X that is isomorphic to the function
space X ) X on itself. Namely we need a xed point of the operator F (X )de ned by X ) X where the indeterminate X occurs both positively and negatively. If we work in set theory and interpret X ) X as the set of all functions,simple cardinality argument reveals that there are only trivial solutions where
the xed point X is a singleton. Hence we must give away naive set-theoreticinterpretation, and try to nd certain exotic structures in which we can havexed points of the operators of the type above. It was late sixties that Scott

The Theory of Twiners and Linear Parametricity (Note)2nally gave a construction by which we can form xed-points of such operators [18]. His construction uses certain (not even Hausdor ) topological spaces
and continuous functions. Later the idea leaded to evoluation of domain theory[7], which nowadays is matured so as to be used as fundamental tools to givemathematical reasoning to programming languages.
Turning to more up-to-date topics, we still hold the same sort of problems inseveral situations. One of them comes from a type-theoretic study of objectoriented programming. During the attempt to pin down the essence of theobject-oriented programming in functional programming setting, several new
ideas are discovered and imported into the traditional theory. These include
how to incorporate the concepts of inheritance and self-reference. At an earlystage, unfortunately, in the author's opinion, inheritance was emphasized too
much. It was a vogue to adjoin the structure of partial orders to systems inorder to interpret inheritance. However the author believes the concept of selfreference is equally or more important as the heart of object-oriented programming and should be dealt with in suitable respects (to be fair, we remark thatmany systems pay attention to also self-reference properly). A philosophy ofobject-orientedness is that each de nition of object should be self-contained(putting inheritance aside) so that the behaviour of an object is determined byinformation written in the de nition of the object itself. As a natural consequence, there should be a mechanism with which certain methods, often calledbinary methods, can refer the object itself. For example, the de nition of theobjects of queues should contain the method to update queues, this method
accessing the object itself and modifying it. To comprehend this phenomenon
type-theoretically, we usually employ recursive types where indeterminates may
occur negatively [1, 15, 17]. Of course, the consistency of recursive types isa sensitive matter. A conceivable way to check it is to build mathematicalsemantics, employing domain theory.
Another example is taken from the theory of programme transformation. The
fusion rule is a machinery to eliminate intermediate structures passed between
two functional procedures, when they are composed. The rule asserts that,
if two canonical functions from inductive types satisfy certain commutativity
conditions, we can combine them into a single function so that intermediate
return values are never created. Under lazy evaluation of functional programming, we can use also coinductive types as potentially in nite data types. The
corresponding fusion rules can be de ned for coinductive types as well. Whatis more interesting, however, occurs when inductive and coinductive types interact. Hylomorphism is by de nition the composition of a canonical function
into coinductive types X: F (X ) followed by a canonical function from inductive
types X: F (X ), provided that these coinductive and inductive types coincide,that is X: F (X ) = X: F (X ) [4, 11]. An advantage of hylomorphism is thatintermediate structures can be always eliminated. But, to use this notion, wemust assume that inductive types coincide coinductive types. At rst sight,

The Theory of Twiners and Linear Parametricity (Note)3

this assumption looks rather unnatural. For example, intuitively, the inductive
type for the operator 1 + A  X is that of nite lists of members of A while
the coinductive type is that of possibly in nite sequences. We can show thatthe assumption of coincidence is equivalent to existence of recursive types undercertain conditions. To ensure the notion of hylomorphism to be consistent, wemust appeal to domain theory again.
Therefore many subjects rely on exquisite theory of Scott domains; from old
problem of giving semantics to the untyped lambda calculus, to newer elds oftheoretical computer science, e.g., object-oriented programming and the theoryof programme transformation. There is no doubt that domain theory was one of
the most successful theories to give rigid foundations to the theory of programming. At this point, however, we want to address a fundamental query. Can thetheory of programming be built only on Scott domains? Trained theoreticians
may fully use domain theory as a vehicle for veri cation, whereas the working
programmers (even the theoreticians themselves when they write actual codes)
would not take Scott domains into account to understand how the programmes
they write work. A role of semantics is to give an intuition of the behaviour ofprogrammes. In this respect, domain theory is too apart from computational
concepts programmers naturally bear in mind.
Our goal is to propose a computer theoretic concept from which we can derive
the construction usually achieved by domain theory. Namely we want to havethe same e ect as domain thoery without appealing to Scott domains. The newconcept is called linear parametricity. An advantage of our method is that we
can obtain various results from a single principle, and that the principle of linear
parametricity can be understood from a computer theoretic point of view.
Earlier we investigated the notion of (full) parametricity for polymorphic programming languages. The intuition behind parametricity can be easily understood computationally. That is, a polymorphic programme is called parametricif it makes no explicit use of information of types. Then the principle of parametricity assures that, if a polymorphic programme is parametric, it behaves in a
uniform way, irrelevant of the types with which we substitute type-parameters.
In earlier works, we studied the principle of parametricity from several perspectives, including categorical and logical ones, and demonstrated that thissimple principle induce many nice properties [8, 9, 10]. However the principleof parametricity can coexist solely with a fragment of polymorphic languages
where only terminating programmes matter. The property of languages allowing recursive programming contradicts to the categorical consequences of theprinciple.
Linear parametricity is a reduced version of full parametricity, and does notcontradict to existence of recursive programmes. Furthermore, in accordancewith recursive programmes, linear parametricity yields better results: solutionsof domain equations, i.e, recursive types, which cannot be consequences of fullThe Theory of Twiners and Linear Parametricity (Note)

4parametricity. Linearity means the same thing as that in linear logic [5]. Namely
linear parametricity is the principle of parametricity asserted in the context oflinear logic. A similar approach is proposed in [16].
In this work, we develop a model of second order linear logic, using new mathematical stu s called twiners, which may be interesting in their own right. They
are extensions of Joyal's analytic functors [12, 13] and Girard's normal functors[6]. Into the twiner model of second order linear logic, we incorporate the notion of linear parametricity, and form a second more elaborate model satisfying
the principle of linear parametricity. Finally we verify that, in the new model,
we can solve domain equations using syntax of linear logic, rather than Scott
D1 -style construction. It would take dozens of pages to fully expand the theoryof twiners. So, in this paper, we must be content with overview of the theories,
leaving details to the full paper in prepration.

2 First Model
We assume certain amount of knowledge in 2-category and bicategory theory.
We refer the reader to standard literatures [14, 3]. To x terminology, we
use the following terms: pseudo-functors, quasi-natural transformations, andmodi cations.
A groupoid is a small category where every morphism has an inverse. In particular, if a groupoid has a single object only, the set of all morphisms formsa group. Conversely every group may be regarded as a groupoid with a single
object. We note that, since every morphism of a groupoid A is invertible, theopposite category Aop is equivalent to A as groupoids. To distinguish objects
etc. in Aop from those in A, we often use notation x for the thing in Aop corresponding to x in A. We sometimes write the overline as in A to denote theopposite groupoid itself.
A groupoid-enriched category is such that its homsets are endowed with thestructure of groupoids satisfying certain conditions we do not specify here.
It comes from standard enriched category theory by taking the category of
all groupoids and all groupoid homomorphisms with cartesian product as a
monoidal structure. We note that a groupoid-enriched category is nothing elsethan a 2-category where every 2-cells are invertible.
Example: (i) Gpoid is the groupoid-enriched category of all groupoids, allgroupoid homomorphisms, and all natural transformations which turns out automotically to be isomorphisms.
(ii) For each groupoid A, the groupoid-enriched category GpoidA is given by
all pseudo-functors on A into Gpoid, all quasi-natural transformations, and all

The Theory of Twiners and Linear Parametricity (Note)

5modi cations. By an analogy that an object of SetG for a group G is the samething as a G-set, we call an object of GpoidA an A-groupoid.
(iii) We can de ne the slice groupoid-enriched category Gpoid=A, the objects
f A on some groupoid T . We omitof which are groupoid homomorphisms T ;!
the details here.

2.1 Proposition

Let A be a groupoid.
Biequivalence GpoidA = Gpoid=A between groupoid-enriched categories holds.

The right-to-left direction of the biequivalence is given by the Grothendieckconstruction [2]. For each object t in GpoidA , we denote the groupoid over A
obtained as
R the Grothendieck construction by either Gr(t) or, bollowing integral
notation, x2A t[x]. In particular, an Aop  B -groupoid M corresponds to a span

SM

R

A
B,
taking A = Aop into considertation. We call Aop  B -groupoids M biprofunctors
 B . We
from A into B as a generalization of profunctors, and write M : A ;!
might regard such a biprofunctor M as a matrix of A columns and B rows. If
N is a biprofunctor from BR into C , we de ne the matrix composition NM :
 C by (NM )[x; z ] := y2B N [y; z ]M [x; y]. In terms of spans, the matrix
A ;!
composition corresponds to taking a bipullback SM B SN .

We can give the interpretation of the additive-multiplicative fragment of linear
logic at this point. Each type is interpreted as a groupoid A. A term of type
A is interpreted as an A-groupoid, that is, an object of GpoidA . We givethe interpretations of types only, leaving those of terms to the full paper. If
we identify types A with their interpretations, the interpretations are given as
follows:[ A? ] = Aop[ A B] = [ A B] = A  B[ A & B] = [ A  B] = A + B[ 1]] = [ ?] = 1[ >] = [ 0]] = ;:In particular, the interpretation of linear implication is given as [ A ( B ] =Aop  B . Namely a term of type A ( B is interpreted as a biprofunctor from
A into B .
&To de ne the intepretation of exponential in linear logic, we introduce wreath

The Theory of Twiners and Linear Parametricity (Note)

6

product of groupoids. Let G be a groupoid endowed with a pseudo-functor' Gpoid. The wreath product A wr G is de ned by the Grothendieck
G ;!
R
construction x2G Gpoid('(x); A). We remark that this concept is a generalization of the traditional wreath product of groups, occurring as a special caseof semidirect product [19]. To be more general, if C is a groupoid-enrichedcategory, we can de ne wreath product A wr G for each object A 2 C and a' C from a groupoid G, simply by putting the groupoid
pseudo-functorR G ;!
A wr G to be x2G C('(x); A). For the interpretation of linear logic, we mustslightly extend groupoid G in de nition of wreath product. We allow G to havea family C of empty components. Namely we formally consider G to be a pairof a groupoid G0 and a set C . The contribution of one empty component towreath product is a singleton as a sum over an empty set. Hence, for such apair G, we de ne A wr G to be a direct sum of A wr G0 and a disjoint groupoid(i.e., a set) C .

2.2 De nition (of S )An extended groupoid S is a direct sum of symmetric groups Sn where n ranges
over the set N of natural numbers. For n = 0, we regard S0 to be an empty
component in the sense above.
The interpretation of exponential is given as wreath product [ !A] = A wr S .
Accordingly [ ?A] = A wr S op, which is equivalent to A wr S .
Next we turn to second order variable types. We want to consider types such
as !X where X is a type variable. To interpret !X , we are interested in theoperation X 7! (X wr S ). It turns outthat (-) wr S is a 2-functor from Gpoid' C is a 2-functor on C into Gpoid
to itself. In general, (-) wr G for G ;!
f B essentially onto if
In a groupoid-enriched category C, we call a 1-cell A ;!
the groupoid homomorphism C(B; X ) ! C(A; X ) induced by composition isfaithful for every object X . Likewise we call f surjective if C(B; X ) ! C(A; X )is full and faithful for every X . An object A is biprojective i the 2-functor
C(A; -) carries surjections to surjections. We call A quasi-biprojective i C(A; -)carries surjections to essentially onto groupoid homomorphisms. Moreover wecall A nitely bipresentable i C(A; -) preserves ltered bicolimits.

2.3 Theorem

Let C be a groupoid-enriched category having all bilimits and all ltered bicolF Gpoid be a pseudo-functor.
imits, and let C ;!
The following are equivalent.
(i) The pseudo-functor F is quasi-naturally
equivalent to the 2-functor (-)wr G' C subject to the condition that '(x)associated to a pseudo-functor G ;!
is nitely bipresentable for every object x 2 G.

The Theory of Twiners and Linear Parametricity (Note)7(ii) The pseudo-functor F preserves ltered bicolimits and bipullbacks.
(iii) For each object (A; x) of the Grothendieck construction Gr(F ), the slicek; )groupoid-enriched category Gr(F )=(A; x) has a biinitial object (Z; c) (;!
(A; x) where Z is nitely bipresentable.

2.4 De nition

Let C be a groupoid-enriched category having all bilimits and all ltered bicolimits.
F Gpoid satisfying one of the equivalent
A twiner on C is a pseudo-functor C ;!
conditions in the preceding theorem. A twiner is called discrete i it carries surjections to surjections. A twiner is called quasi-discrete i it carries surjections
to essentially onto groupoid homomorphisms.
' C is discrete i all '(x) are biprojective. It is
A twiner (-) wr G for G ;!
quasi-discrete i all '(x) are quasi-biprojective.
Now we give the interpretation of types and terms having type variables inlinear logic. A type F (X1 ; X2 ; : : : ; Xn ) with n type variables is interpreted asa discrete twiner on Gpoidn . Moreover a term of type F (X1 ; X2 ; : : : ; Xn ) isinterpreted as a quasi-discrete twiner on the Grothendieck construction Gr(F ).
t Gpoid and a groupoid A, we can associate a FA-groupoid tA by
To Gr(F ) ;!
de nition tA [x] := t(A; x).
For a later use, we note that a twiner extends to operations on biprofunctors.
 B is a biprofunctor, we can associate
If F is a twiner on Gpoid and M : A ;!
 FB . In fact, M corresponds to a span SM over A and B .
Fbipro M : FA ;!
So we simply de ne Fbipro M to correspond to F (SM ) over FA and FB . In thesequel, we write simply FM instead of cumbersome Fbipro M .
Finally we must give the interpretation of second order quanti ed types. Indeed we give two interpretations. The rst one stated here is based on theobservations summarized so far. Later we provide with more elaborate construction so that the model enjoys the principle of linear parametricity. Let
Bqb (Gpoid) be the 2-groupoid of all quasi-biprojective, nitely bipresentablegroupoids, all equivalences between such groupoids, and all natural isomorphisms. We note that every quasi-biprojective groupoid is equivalent to a direct
sum of free groups. The 2-groupoid Bqb (Gpoid) is actually biequivalent to agroupoid, as a consequence of the fact that all free groups have trivial centers.
For each discrete twiner F on Gpoid, we de ne groupoid F by
R
F = X 2B (Gpoid) F (X ).
qb

Then the interpretation of second order quanti ed types is given as [ 8 X: F (X )]]= F . Now we have obtained the rst model of second order linear logic.

The Theory of Twiners and Linear Parametricity (Note)8

2.5 Theorem

The interpretation above gives a sound model of second order linear logic.

3 Linear Parametricity and Recursive Types
We truncate the rst model to the one satisfying linear parametricity. First we
introduce a linear dependent type theory with realizability semantics informally.
Types are identi ed with groupoids and terms of type A are objects of groupoidenriched category GpoidA . The only logical connective we are concerned withis the linear rst order universal quanti cation (8 x : A)'(x). As an atomic
formula, we take equality predicate t =A u for each type A. We interpret each
formula as a groupoid. For equality, the formula t =A u is interpreted as thegroupoidR
hujti := x2A u[x]t[x]where the concatenation is an abbreviation of direct product of two groupoids.
We note that there is an embedding Aop ! GpoidA carrying x to the Agroupoid denoted by fxg which carries a 2 A to the discrete groupoid A(x; a).
For interpretation of linear quanti er, if '(x) is interpreted as F : GpoidA !
Gpoid, then
R the formula (8 x : A)'(x) is interpreted by the Grothendieck construction x2A F fxg. In particular, equality t =? u for type ? (that is, asingleton 1) is interpreted by uop  t. Then t =A u may be regarded as anacronym of (8 x : A? )(tx =? ux).
So far linearity does not come on the scene yet. It involves the witness relations  ' we introduce below, read as s witnesses '. Here s is an A-groupoid if theformula ' is interpreted by groupoid A. For equality predicate, s  (t =? u) i
s is an identity biprofunctor from u intoR t. For the linear quanti er, the witness
relation s  (8 x : A)'(x) holds for an ( x2A F fxg)-groupoid s i su  Fu holds
for every u 2 GpoidA . Here an Fu-groupoid su is de ned assu[y] =ZZ

x2A;c2F fxgs[x; c]Zk2u[x]Fu(Fk(c); y)

for y in the groupoid Fu. We note u[x] equals GpoidA (fxg; u). So Fk isa groupoid homomorphism from F fxg into Fu. We emphasize that linearlity
involves witnesses only. There may be several occurrences of x in the linearly
quanti ed formula (8 x : A)'(x), including the case of null occurrence. The nullcase, say (8 x : A)B , is written linear implication A ( B .
A (binary) linear predicate between types A and B is a predicate P (x; y) for B
x : A and y : B , endowed with its interpretation as a biprofunctor M : A ;!
and witness relation s  P (t; u) for each RR
pair of t and t0 . Here s is a hujM jtigroupoid, where hujM jti is de ned to be x2A;y2B u[y]M [x; y]t[x].

The Theory of Twiners and Linear Parametricity (Note)

9

Example: (i) x =A y is a linear predicate between A and A. It is interpreted
as an identity biprofunctor, and witness relation has been de ned above.
 A0(ii) If R and S are linear predicates interpreted by biprofunctors M : A ;!
00
 B , then R 0 S is a binary predicate between A B and A B 0 .
and N : B ;!
Its interpretation is M N de ned as (M N )[x; y; x0 ; y0] := M [x; x0 ]N [y; y0].
Witness relation is de ned to hold for r s  R(t; t0 ) S (u; u0) i both r  R(t; t0 )and s  S (u; u0) hold.
(iii) If R is a linear predicate between A and A0 , the dual R? between Aop andA0 op is de ned. We regard
R? (t; t0 ) = (8 x : A)(8 x0 : A0 ) (R(x; x0 ) ( (tx =? t0 x0 )),from which its interpretation and witness relation are induced.

3.1 De nition

A factual predicate is a linear predicate R satisfying that s  R(t; t0 ) i s 
R?? (t; t0 ).
As a basic observation, the double dual R?? is a factual predicate for every
linear predicate R. Using this observation, we associate factual predicates F (R)to each type F (X ) with a type variable X and each factual predicate R. We
have given a linear predicate R 0 S in the examples above. Likewise we cande ne linear predicates R &0 S and !0 R in a straightforward way. De nition of
80 Y: F (R; Y ) is more complicated, and we omit it here. These predicates withsux 0 are not factual. So we de ne as follows:
F (R) G(R) = (F (R)? 0 G(R)? )?
F (R) G(R) = (F (R)? G(R)? )?
F (R)  G(R) = (F (R)? &0 G(R)? )?
F (R) & G(R) = (F (R)?  G(R)? )?
?F (R)= (!0 F (R)? )?
!F (R)= (?F (R)? )?
9 Y: G(R; Y ) = (80 Y: G(R; Y )? )?
8 Y: G(R; Y ) = (9 Y: G(R; Y )? )?
 B , then F (R) is interpreted
If a linear predicate R is interpreted by M : A ;!
by the biprofunctor FM .
We extend a twiner t on Gr(F ) to operations on biprofunctors, as a twiner F B,
on Gpoid extends to Fbipro M = FM . For each biprofunctor M : A ;!
we want to de ne a htB jFM jtA i-groupoid tM . In terms of spans, the groupoid
&

&

10

The Theory of Twiners and Linear Parametricity (Note)htB jFM jtA i corresponds
to bipullback TA FA F SM FB TB where by convention tA 2 GpoidFA corresponds to a groupoid TA over FA and so on. ThentM is de ned to correspond TSM factoring through TA FA F SM FB TB .

3.2 De nition

Let t be a quasi-discrete twiner on Gr(F ) where F is a discrete twiner on Gpoid.
t is linearly parametric i witness relation tM  F (R)(tA ; tB ) holds for every
 B.
factual linear predicate R interpreted by M : A ;!
We recall that a twiner is Requivalent to a 2-functor given as wreath product. It
has the shape (-) wr G = z2G h'(z) where h'(z) is the representable 2-functor
h'(z) (A; x) = Gr(F )('(z ); (A; x)). The following is our main lemma towards
the principle of linear parametricity.

3.3 LemmaR

Let t be a quasi-discrete twiner on Gr(F ), given as wreath product z2G h'(z).
Then t is linearly parametric i a representable 2-functor h'(z) is linear parametric for every object z 2 G.

We de ne P F be the full subgroupoid of F of all objects (Z; c) satisfyingthat the representable 2-functor Gr(F )((Z; c); -) is linearly parametric. With
' Gr(F ) is linearly
this lamme, a quasi-discrete twiner (-) wr G induced by G ;!
Pparametric i the image of ' is contained in  F . Now we de ne the second
model of second order linear logic simply by changing the interpretation of quanti er. We interpret 8 X: F (X ) by P F . We can verify that the interpretationof every term is actually linearly parametric, that is:

3.4 Theorem

The second interpretation given above provides a sound model of second orderlinear logic.

An advantage of our linearly parametric model to earlier models satisfying fullparametricity is that we can have xed-point operator, which is needed to interpret recursive programmes.

3.5 Theorem

We have a linearly parametric xed-point combinatorX) ( X.

x of type 8 X: !(!X (The Theory of Twiners and Linear Parametricity (Note)11

We can represent recursive types in the linearly parametric second model asfollows. Let F (X ) be a type where X may occur both positively and negatively.
Separating positive occurrences X + and negative occurrences X ; , we may write
F (X ;; X + ). We de ne two types A and B as
A = 9 X; Y: !(X ( F (Y; X )) !(F (X; Y ) ( Y ) X
B = 8 X; Y: !(X ( F (Y; X )) !(F (X; Y ) ( Y ) ( Y .
Then we can verify that B = F (A; B ) and A = F (B; A). The proof simulates that of representation of initial algebras and nal coalgebras under fullparametricity. Moreover A = B holds in the linearly parametric model, as aconsequence of the existence of the xed-point combinator x. Thus the following holds:

3.6 Theorem

Suppose that groupoids A and B are given as above.
Then A = F (A) holds in the linearly parametric model of twiners. Namely A
gives an encoding of recursive type rec X: F (X ) in the framework of second orderlinear logic augmented with a xed-point combinator.

References[1] M. Abadi and L. Cardelli, A theory of primitive objects, Second-order systems,
Sci. Computer Programming 25 (1995) 81{116.
[2] M. Barr and C. Wells, Category Theory for Computing Science, Prentice-Hall
International Series in Computer Science, (Prentice-Hall, 1990).
[3] J. Benabou, Introduction to bicategories, in: Reports of the Midwest Category
Seminar, (Springer, 1967) pp. 1{77.
[4] R. S. Bird, Functional algorithm design, Sci. Computer Programming 26 (1996)
15{31.
[5] J.-Y. Girard, Linear logic, Theoretical Computer Sci. 50 (1987) 1{101.
[6] J.-Y. Girard, Normal functors, power series and -calculus, Ann. Pure Applied
Logic 37 (1988) 129{177.
[7] C. A. Gunter, Semantics of Programming Languages. Structures and Techniques,Foundations of Computing Series, (MIT Press, 1992).
[8] R. Hasegawa, Categorical data types in parametric polymorphism, Mathematical
Structures in Computer Science 4 (1994) 71{109.
[9] R. Hasegawa, Relational limits in general polymorphism, Publications of ResearchInstitute for Mathematical Sciences 30 (1994) 535{576.
[10] R. Hasegawa, A logical aspect of parametric polymorphism, in: Computer Science
Logic, 9th International Workshop CSL'95, H. K. Buning, ed., Paderborn, Germany, 1995, Lecture Notes in Computer Science 1092, (Springer, 1995) pp. 291{
307.

The Theory of Twiners and Linear Parametricity (Note)12[11] Z. Hu, H. Iwasaki, and M. Takeichi, Deriving structural hylomorphisms fromrecursive de nitions, in: ACM SIGPLAN International Conference on Functional
Programming, Philadelphia, USA, (ACM Press, 1996) pp. 73{82.
[12] A. Joyal, Une theorie combinatoire des series formelles, Advances Math. 42 (1981)1{82.
[13] A. Joyal, Foncteurs analytiques et especes de structures, Combinatoire Enumerative, Proceedings, Montreal, Quebec, Canada, 1985, G. Labelle, P. Leroux, eds.,
Lecture Notes in Mathematics 1234, (Springer, 1986) pp. 126{159.
[14] G. M. Kelly and R. Street, Review of the elements of 2-categories, in: Category
Seminar, Sydney, Australia, 1972/1973, Lecture Notes in Math. 420, (Springer,1974) pp. 75{103.
[15] J. C. Mitchell, Foundations for Programming Languages, Foundations of Computing Series, (MIT Press, 1996).
[16] G. Plotkin, Second order type theory and recursion, unpublished notes, 1993.
[17] D. Remy and J. Vouillon, Objective ML: An e ective object-oriented extension
to ML, Theory Practice Object Systems 4 (1998) 27{50.
[18] D. S. Scott, Continuous Lattices, in: Toposes, Algebraic Geometry and Logic,
Halifax, Canada, 1971, Lecture Notes in Mathematics 274, (Springer, 1972) pp. 97{
136.
[19] M. Suzuki, Group Theory, I, Grundlagen der mathematischen Wissenshaften 247,
(Springer, 1982).