Silvano Dal

Andrew D Gordon

Region Analysis and a π-Calculus with Groups

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed π-calculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and de-allocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our π-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin's rather elaborate co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the π-calculus with effects.

Motivation

This paper reports a new proof of correctness of region-based memory management [START_REF] Tofte | Region-based memory management[END_REF], based on a new garbage collection principle for the π-calculus.

Tofte and Talpin's region calculus is a compiler intermediate language that, remarkably, supports an implementation of Standard ML that has no garbage collector, the ML Kit compiler [START_REF] Birkedal | From region inference to von Neumann machines via region representation inference[END_REF]. The basic idea of the region calculus is to partition heap memory into a stack of regions. Each boxed value (that is, a heap-allocated value such as a closure or a cons cell) is annotated with the particular region into which it is stored. The construct letregion ρ in b manages the allocation and de-allocation of regions. It means: "Allocate a fresh, empty region, denoted by the region variable ρ; evaluate the expression b; de-allocate ρ." A type and effect system for the region calculus guarantees the safety of de-allocating the defunct region as the last step of letregion. The allocation and de-allocation of regions obeys a stack discipline determined by the nesting of the letregion constructs. A region inference algorithm compiles ML to the region calculus by computing suitable region annotations for boxed values, and inserting letregion constructs as necessary. In practice, space leaks, where a particular region grows without bound, are a problem. Still, they can practically always be detected by profiling and eliminated by simple modifications. The ML Kit efficiently executes an impressive range of benchmarks without a garbage collector and without space leaks. Region-based memory management facilitates interoperability with languages like C that have no garbage collector and helps enable realtime applications of functional programming.

Tofte and Talpin's semantics of the region calculus is a structural operational semantics. A map from region names to their contents represents the heap. A fresh region name is invented on each evaluation of letregion. This semantics supports a co-inductive proof of type safety, including the safety of de-allocating the defunct region at the end of each letregion. The proof is complex and surprisingly subtle, in part because active regions may contain dangling pointers that refer to de-allocated regions.

The region calculus is a strikingly simple example of a language with type generativity. A language has type generativity when type equivalence is by name (that is, when types with different names but the same structure are not equivalent), and when type names can be generated at run-time. A prominent example is the core of Standard ML [START_REF] Milner | The Definition of Standard ML (Revised)[END_REF], whose datatype construct effectively generates a fresh algebraic type each time it is evaluated. (The ML module system also admits type generativity, but at link-time rather than run-time.) The region calculus has type generativity because the type of a boxed value includes the name of the region where it lives, and region names are dynamically generated by letregion. The semantics of Standard ML accounts operationally for type generativity by inventing a fresh type name on each elaboration of datatype. Various researchers have sought more abstract accounts of type generativity [START_REF] Leroy | A syntactic theory of type generativity and sharing[END_REF][START_REF] Russo | Standard ML type generativity as existential quantification[END_REF].

This paper describes a new semantics for a form of the region calculus, obtained by translation to a typed π-calculus equipped with a novel effect system. The π-calculus [START_REF] Milner | Communicating and Mobile Systems: the π-Calculus[END_REF] is a rather parsimonious formalism for describing the essential semantics of concurrent systems. It serves as a foundation for describing a variety of imperative, functional, and object-oriented programming features [START_REF] Sangiorgi | Interpreting functions as π-calculus processes: a tutorial[END_REF][START_REF] Taylor | Formalising and Reasoning about Fudgets[END_REF][START_REF] Walker | Objects in the pi-calculus[END_REF], for the design of concurrent programming languages [START_REF] Fournet | The reflexive CHAM and the Join-calculus[END_REF][START_REF] Pierce | Pict: A programming language based on the pi-calculus[END_REF], and for the study of security protocols [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF], as well as other applications. The only data in the π-calculus are atomic names. Names can model a wide variety of identifiers: communication channels, machine addresses, pointers, object references, cryptographic keys, and so on. A new-name construct (νx)P generates names dynamically in the standard π-calculus. It means: "Invent a fresh name, denoted by x; run process P ." One might hope to model region names with π-calculus names but unfortunately typings would not be preserved: a region name may occur in a region-calculus type, but in standard typed π-calculi [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF], names may not occur in types.

We solve the problem of modelling region names by defining a typed πcalculus equipped with name groups and a new-group construct [START_REF] Cardelli | Ambient groups and mobility types[END_REF]. The idea is that each π-calculus name belongs to a group, G. The type of a name now includes its group. A new-group construct (νG)P generates groups dynamically. It means: "Invent a fresh group, denoted by G; run process P ." The basic ideas of the new semantics are that region names are groups, that pointers into a region ρ are names of group ρ, and that given a continuation channel k the continuation-passing semantics of letregion ρ in b is simply the process (νρ) [[b]]k where [[b]]k is the semantics of expression b. The semantics of other expressions is much as in earlier π-calculus semantics of λ-calculi [START_REF] Sangiorgi | Interpreting functions as π-calculus processes: a tutorial[END_REF]. Parallelism allows us to explain a whole functional computation as an assembly of individual processes that represent components such as closures, continuations, and function invocations.

This new semantics for regions makes two main contributions.

-First, we give a new proof of the correctness of memory management in the region calculus. We begin by extending a standard encoding with the equation

[[letregion ρ in b]]k = (νρ)[[b]]k.
Then the rather subtle correctness property of de-allocation of defunct regions turns out to be a simple instance of a new abstract principle expressed in the π-calculus. Hence, an advantage of our π-calculus proof is that it is conceptually simpler than a direct proof. -Second, the semantics provides a more abstract, equational account of type generativity in the region calculus than the standard operational semantics.

The specific technical results of the paper are:

-A simple proof of type soundness of the region calculus (Theorem 1).

-A new semantics of the region calculus in terms of the π-calculus with groups.

The translation preserves types and effects (Theorem 2) and operational behaviour (Theorem 3). -A new garbage collection principle for the π-calculus (Theorem 4) whose corollary (Theorem 5) justifies de-allocation of defunct regions in the region calculus.

We organise the rest of the paper as follows. Section 2 introduces the region calculus. Section 3 describes the π-calculus with groups and effects. Section 4 gives our new π-calculus semantics for regions. Section 5 concludes. Omitted proofs may be found in a long version of this paper [START_REF] Zilio | Region analysis and a π-calculus with groups[END_REF].

A λ-Calculus with Regions

To focus on the encoding of letregion with the new-group construct, we work with a simplified version of the region calculus of Tofte and Talpin [START_REF] Tofte | Region-based memory management[END_REF]. Our calculus omits the recursive functions, type polymorphism, and region polymorphism present in Tofte and Talpin's calculus. The long version of this paper includes an extension of our results to a region calculus with recursive functions, finite lists, and region polymorphism. To encode these features, we need to extend our πcalculus with recursive types and group polymorphism. Tofte and Talpin explain that type polymorphism is not essential for their results. Still, we conjecture that our framework could easily accommodate type polymorphism.

Syntax

Our region calculus is a typed call-by-value λ-calculus equipped with a letregion construct and an annotation on each function to indicate its storage region. We assume an infinite set of names, ranged over by p, q, x, y, z. For the sake of simplicity, names represent both program variables and memory pointers, and a subset of the names L = { 1 , . . . , n } represents literals. The following table defines the syntax of λ-calculus expressions, a or b, as well as an auxiliary notion of boxed value, u or v.

Expressions and Values:

x, y, p, q, f, g name: variable, pointer, literal We shall explain the type A later. In both let x = a in b and λ(x:A)b, the name x is bound with scope b. Let fn(a) be the set of names that occur free in the expression a. We identify expressions and values up to consistent renaming of bound names. We write P {x←y} for the outcome of renaming all free occurrences of x in P to the name y. Our syntax is in a reduced form, where an application x(y) is of a name to a name. We can regard a conventional application b(a) as an abbreviation for let f = b in let x = a in f (x), where f = x and f is not free in a.

We explain the intended meaning of the syntax by example. The following expression,

ex 1 ∆ = letregion ρ in let f = λ(x:Lit)x at ρ in let g = λ(y:Lit)f (y) at ρ in g(5)
means: "Allocate a fresh, empty region, and bind it to ρ ; allocate λ(x:Lit)x in region ρ , and bind the pointer to f ; allocate λ(y:Lit)f (y) in region ρ (an already existing region), and bind the pointer to g; call the function at g with literal argument 5; finally, de-allocate ρ ." The function call amounts to calling λ(y:Lit)f (y) with argument 5. So we call λ(x:Lit)x with argument 5, which immediately returns 5. Hence, the final outcome is the answer 5, and a heap containing a region ρ with g pointing to λ(y:Lit)f (y). The intermediate region ρ has gone. Any subsequent invocations of the function λ(y:Lit)f (y) would go wrong, since the target of f has been de-allocated. The type and effect system of Section 2.3 guarantees there are no subsequent allocations or invocations on region ρ , such as invoking λ(y:Lit)f (y).

Dynamic Semantics

Like Tofte and Talpin, we formalize the intuitive semantics via a conventional structural operational semantics. A heap, h, is a map from region names to regions, and a region, r, is a map from pointers (names) to boxed values (function closures). In Tofte and Talpin's semantics, defunct regions are erased from the heap when they are de-allocated. In our semantics, the heap consists of both live regions and defunct regions. Our semantics maintains a set S containing the region names for the live regions. This is the main difference between the two semantics. Side-conditions on the evaluation rules guarantee that only the live regions in S are accessed during evaluation. Retaining the defunct regions simplifies the proof of subject reduction. Semmelroth and Sabry [START_REF] Semmelroth | Monadic encapsulation in ML[END_REF] adopt a similar technique for the same reason in their semantics of monadic encapsulation.

Regions, Heaps, and Stacks:

r ::= (p i → v i ) i∈1..n region, p i distinct h ::= (ρ i → r i ) i∈1..n heap, ρ i distinct S ::= {ρ 1 , . . . , ρ n } stack of live regions A region r is a finite map of the form p 1 → v 1 , . . . , p n → v n ,
where the p i are distinct, which we usually denote by (p i → v i ) i∈1..n . An application, r(p), of the map r to p denotes v i , if p is p i for some i ∈ 1..n. Otherwise, the application is undefined. The domain, dom(r), of the map r is the set {p 1 , . . . , p n }. We write ∅ for the empty map. If r = (p i → v i ) i∈1..n , we define the notation r -p to be

p i → v i i∈(1..n)-{j} if p = p j for some j ∈ 1.
.n, and otherwise to be simply r. Then we define the notation r + (p → v) to mean (r -p), p → v.

We use finite maps to represent regions, but also heaps, and various other structures. The notational conventions defined above for regions apply also to other finite maps, such as heaps. Additionally, we define dom 2 (h) to be the set of all pointers defined in h, that is, ρ∈dom(h) dom(h(ρ)).

The evaluation relation, S • (a, h) ⇓ (p, h ), may be read: in an initial heap h, with live regions S, the expression a evaluates to the name p (a pointer or literal), leaving an updated heap h , with the same live regions S.

Judgments:

S • (a, h) ⇓ (p, h ) evaluation

Evaluation Rules:

(Eval Var) S • (p, h) ⇓ (p, h) (Eval Alloc) ρ ∈ S p / ∈ dom 2 (h) S • (v at ρ, h) ⇓ (p, h + (ρ → (h(ρ) + (p → v)))) (Eval Appl) ρ ∈ S h(ρ)(p) = λ(x:A)b S • (b{x←q}, h) ⇓ (p , h ) S • (p(q), h) ⇓ (p , h ) (Eval Let) S • (a, h) ⇓ (p , h ) S • (b{x←p }, h ) ⇓ (p , h ) S • (let x = a in b, h) ⇓ (p , h ) (Eval Letregion) ρ / ∈ dom(h) S ∪ {ρ} • (a, h + ρ → ∅) ⇓ (p , h ) S • (letregion ρ in a, h) ⇓ (p , h )
Recall the example expression ex 1 from the previous section. Consider an initial heap h = ρ → ∅ and a region stack S = {ρ}, together representing a heap with a single region ρ that is live but empty. We can derive S • (ex

1 , h) ⇓ (5, h ) where h = ρ → (g → λ(y:Lit)f (y)), ρ → (f → λ(x:Lit)x). Since ρ ∈ S but ρ /
∈ S, ρ is live but ρ is defunct.

Static Semantics

The static semantics of the region calculus is a simple type and effect system [START_REF] Gifford | Integrating functional and imperative programming[END_REF][START_REF] Talpin | Polymorphic type, region and effect inference[END_REF][START_REF] Wadler | The marriage of effects and monads[END_REF]. The central typing judgment of the static semantics is:

E a : {ρ1,...,ρn} A
which means that in a typing environment E, the expression a may yield a result of type A, while allocating and invoking boxed values stored in regions ρ 1 , . . . , ρ n . The set of regions {ρ 1 , . . . , ρ n } is the effect of the expression, a bound on the interactions between the expression and the store. For simplicity, we have dropped the distinction between allocations, put(ρ), and invocations, get(ρ), in Tofte and Talpin's effects. This is an inessential simplification; the distinction could easily be added to our work. An expression type, A, is either Lit, a type of literal constants, or (A e → B) at ρ, the type of a function stored in region ρ. The effect e is the latent effect: the effect unleashed by calling the function. An environment E has entries for the regions and names currently in scope.

Effects, Types, and Environments: The following tables present our type and effect system as a collection of typing judgments defined by a set of rules. Tofte and Talpin present their type and effect system in terms of constructing a region-annotated expression from an unannotated expression. Instead, our main judgment simply expresses the type and effect of a single region-annotated expression. Otherwise, our system is essentially the same as Tofte and Talpin's.

Type and Effect Judgments:

E good environment E A
good type E a : e A good expression, with type A and effect e

Type and Effect Rules: The rules for good environments are standard; they assure that all the names and region variables in the environment are distinct, and that the type of each name is good. All the regions in a good type must be declared. The type of a good expression is checked much as in the simply typed λ-calculus. The effect of a good expression is the union of all the regions in which it allocates or from which it invokes a closure. In the rule (Exp Letregion), the condition ρ / ∈ fr (A) ensures that no function with a latent effect on the region ρ may be returned. Calling such a function would be unsafe since ρ is de-allocated once the letregion terminates. In the rule (Exp Fun), the effect e of the body of a function must be contained in the latent effect e of the function. For the sake of simplicity we have no rule of effect subsumption, but it would be sound to add it: if E a : e A and e ⊆ dom(E) then E a : e∪e A. In the presence of effect subsumption we could simplify (Exp Fun) by taking e = e .

(Env ∅) ∅ (Env x) (recall L is the set of literals) E A x / ∈ dom(E) ∪ L E, x:A (Env ρ) E ρ / ∈ dom(E) E, ρ (Type Lit) E E Lit (Type →) E A ρ ∪ {e} ⊆ dom(E) E B E (A e → B) at ρ (Exp x) E, x:A, E E, x:A, E x : ∅ A (Exp ) E ∈ L E : ∅ Lit (Exp Appl) E x : ∅ (B e → A) at ρ E y : ∅ B E x(y) : {ρ}∪e A (Exp Let) E a : e A E
Recall the expression ex 1 from Section 2.1. We can derive the following:

ρ, ρ (λ(x:Lit)x) at ρ : {ρ } (Lit ∅ → Lit) at ρ ρ, ρ , f :(Lit ∅ → Lit) at ρ (λ(x:Lit)f (x)) at ρ : {ρ} (Lit {ρ } → Lit) at ρ ρ, ρ , f :(Lit ∅ → Lit) at ρ , g:(Lit {ρ } → Lit) at ρ g(5) : {ρ,ρ } Lit
Hence, we can derive ρ ex 1 : {ρ} Lit.

For an example of a type error, suppose we replace the application g(5) in ex 1 simply with the identifier g. Then we cannot type-check the letregion ρ construct, because ρ is free in the type of its body. This is just as well, because otherwise we could invoke a function in a defunct region.

For an example of how a dangling pointer may be passed around harmlessly, but not invoked, consider the following. Let F abbreviate the type (Lit ∅ → Lit) at ρ . Let ex 2 be the following expression:

ex 2 ∆ = letregion ρ in let f = λ(x:Lit)x at ρ in let g = λ(f :F )5 at ρ in let j = λ(z:Lit)g(f ) at ρ in j We have ρ ex 2 : {ρ} (Lit {ρ} → Lit) at ρ. If S = {ρ} and h = ρ → ∅, then S • (b, h) ⇓ (j, h ) where the final heap h is ρ → (g → λ(f :F )5, j → λ(z:Lit)g(f )), ρ → (f → λ(x:Lit)x).
In the final heap, there is a pointer f from the live region ρ to the defunct region ρ . Whenever j is invoked, this pointer will be passed to g, harmlessly, since g will not invoke it.

Relating the Static and Dynamic Semantics

To relate the static and dynamic semantics, we need to define when a configuration is well-typed. First, we need notions of region and heap typings. A region typing R tracks the types of boxed values in the region. A heap typing H tracks the region typings of all the regions in a heap. The environment env (H) lists all the regions in H, followed by types for all the pointers in those regions.

Region and Heap Typings:

R ::= (p i :A i ) i∈1..n region typing

H ::= (ρ i → R i ) i∈1..n heap typing ptr (H) ∆ = R 1 , . . . , R n if H = (ρ i → R i ) i∈1..n env (H) ∆ = dom(H), ptr (H)
The next tables describe the judgments and rules defining well-typed regions, heaps, and configurations. The main judgment H |= S • (a, h) : A means that a configuration S •(a, h) is well-typed: the heap h conforms to H and the expression a returns a result of type A, and its effect is within the live regions S. Intuitively, the theorem asserts that evaluation of a well-typed configuration S •(a, h) leads to another well-typed configuration S •(p , h ), where H represents types for the new pointers and regions in h .

(Region Good) E v i at ρ : {ρ} A i ∀i ∈ 1..n E (p i → v i ) i∈1..n at ρ : (p i :A i ) i∈1..
The following proposition shows that well-typed configurations avoid the run-time errors of allocation or invocation of a closure in a defunct region.

Proposition 1. (1) If H |= S • (v at ρ, h) : A then ρ ∈ S. (2) If H |= S • (p(q), h) : A then there are ρ and v such that ρ ∈ S, h(ρ)(p) = v,
and v is a function of the form λ(x:B)b with env (H), x:B b : e A.

Combining Theorem 1 and Proposition 1 we may conclude that such runtime errors never arise in any intermediate configuration reachable from an initial well-typed configuration. Implicitly, this amounts to asserting the safety of region-based memory management, that defunct regions make no difference to the behaviour of a well-typed configuration. Our π-calculus semantics of regions makes this explicit: we show equationally that direct deletion of defunct regions makes no difference to the semantics of a configuration.

A π-Calculus with Groups

In this section, we define a typed π-calculus with groups. In the next, we explain a semantics of our region calculus in this π-calculus. Exactly as in the ambient calculus with groups [START_REF] Cardelli | Ambient groups and mobility types[END_REF], each name x has a type that includes its group G, and groups may be generated dynamically by a new-group construct, (νG)P . So as to model the type and effect system of the region calculus, we equip our π-calculus with a novel group-based effect system. In other work [START_REF] Cardelli | Group creation and secrecy[END_REF], not concerned with the region calculus, we consider a simpler version of this π-calculus, with groups but without an effect system, and show that new-group helps keep names secret, in a certain formal sense.

Syntax

The following table gives the syntax of processes, P . The syntax depends on a set of atomic names, x, y, z, p, q, and a set of groups, G, H. For convenience, we assume that the sets of names and groups are identical to the sets of names and region names, respectively, of the region calculus. We impose a standard constraint [START_REF] Fournet | The reflexive CHAM and the Join-calculus[END_REF][START_REF] Merro | On asynchrony in name-passing calculi[END_REF], usually known as locality, that received names may be used for output but not for input. This constraint is actually unnecessary for any of the results of this paper, but is needed for proofs of additional results in the long version [START_REF] Zilio | Region analysis and a π-calculus with groups[END_REF]. Except for the addition of type annotations and the new-group construct, and the locality constraint, the following syntax and semantics are the same as for the polyadic, choice-free, asynchronous π-calculus [START_REF] Milner | Communicating and Mobile Systems: the π-Calculus[END_REF].

Expressions and Processes:

x, y, p, q name: variable, channel P, Q, R ::= process x(y 1 :T 1 , . . . , y n :T n ).P input (no y i ∈ inp(P )) x y 1 , . . . , y n output (νG)P new-group: group restriction (νx:T )P new-name: name restriction

P | Q composition !P replication 0 inactivity
The set inp(P ) contains each name x such that an input process x(y 1 :T 1 , . . . , y n :T n ).P occurs as a subprocess of P , with x not bound. We explain the types T below. In a process x(y 1 :T 1 , . . . , y n :T n ).P , the names y 1 , . . . , y n are bound; their scope is P . In a group restriction (νG)P , the group G is bound; its scope is P . In a name restriction (νx:T )P , the name x is bound; its scope is P . We identify processes up to the consistent renaming of bound groups and names. We let fn(P ) and fg(P ) be the sets of free names and free groups, respectively, of a process P . We write P {x←y} for the outcome of a capture-avoiding substitution of the name y for each free occurrence of the name x in the process P .

Next, we explain the semantics of the calculus informally, by example. We omit type annotations and groups; we shall explain these later.

A process represents a particular state in a π-calculus computation. A state may reduce to a successor when two subprocesses interact by exchanging a tuple of names on a shared communication channel, itself identified by a name. For example, consider the following process:

f (x, k ).k x | g(y, k ).f y, k | g 5, k
This is the parallel composition (denoted by the | operator) of two input processes g(y, k ).f y, k and f (x, k ).k x , and an output process g 5, k . The whole process performs two reductions. The first is to exchange the tuple 5, k on the channel g. The names 5 and k are bound to the input names y and k, leaving f (x, k ).k x | f 5, k as the next state. This state itself may reduce to the final state k 5 via an exchange of 5, k on the channel f .

The process above illustrates how functions may be encoded as processes. Specifically, it is a simple encoding of the example ex 1 from Section 2.1. The input processes correspond to λ-abstractions at addresses f and g; the output processes correspond to function applications; the name k is a continuation for the whole expression. The reductions described above represent the semantics of the expression: a short internal computation returning the result 5 on the continuation k.

The following is a more accurate encoding:

(νf )(νg)(

f →λ(x)x !f (x, k ).k x | g →λ(y)f (y) !g(y, k ).f y, k | g(5)
g 5, k )

A replication !P is like an infinite parallel array of replicas of P ; we replicate the inputs above so that they may be invoked arbitrarily often. A name restriction (νx)P invents a fresh name x with scope P ; we restrict the addresses f and g above to indicate that they are dynamically generated, rather than being global constants.

The other π-calculus constructs are group restriction and inactivity. Group restriction (νG)P invents a fresh group G with scope P ; it is the analogue of name restriction for groups. Finally, the 0 process represents inactivity.

Dynamic Semantics

We formalize the semantics of our π-calculus using standard techniques. A reduction relation, P → Q, means that P evolves in one step to Q. It is defined in terms of an auxiliary structural congruence relation, P ≡ Q, that identifies processes we never wish to tell apart.

Structural Congruence

: P ≡ Q P ≡ P (Struct Refl) Q ≡ P ⇒ P ≡ Q (Struct Symm) P ≡ Q, Q ≡ R ⇒ P ≡ R (Struct Trans) P ≡ Q ⇒ x(y 1 :T 1 , . . . , y n :T n ).P ≡ x(y 1 :T 1 , . . . , y n :T n ).Q (Struct Input) P ≡ Q ⇒ (νG)P ≡ (νG)Q (Struct GRes) P ≡ Q ⇒ (νx:T )P ≡ (νx:T )Q (Struct Res) P ≡ Q ⇒ P | R ≡ Q | R (Struct Par) P ≡ Q ⇒ !P ≡ !Q (Struct Repl) P | 0 ≡ P (Struct Par Zero) P | Q ≡ Q | P (Struct Par Comm) (P | Q) | R ≡ P | (Q | R) (Struct
P → Q ⇒ P | R → Q | R (Red Par) P → Q ⇒ (νG)P → (νG)Q (Red GRes) P → Q ⇒ (νx:T )P → (νx:T )Q (Red Res) P ≡ P, P → Q, Q ≡ Q ⇒ P → Q (Red ≡)
Groups help to type-check names statically but have no dynamic behaviour; groups are not themselves values. The following proposition demonstrates this precisely; it asserts that the reduction behaviour of a typed process is equivalent to the reduction behaviour of the untyped process obtained by erasing all type and group annotations.

Erasing type annotations and group restrictions: erase(x(y 1 :T 1 , . . . , y n :T n ).P ) ∆ = x(y 1 , . . . , y n ).erase(P ) erase(x y 1 , . . . , y n ) ∆ = x y 1 , . . . , y n Proposition 2 (Erasure). For all typed processes P and Q, if P → Q then erase(P ) → erase(Q) and if erase(P ) → R then there is a typed process Q such that P → Q and R ≡ erase(Q).

Static Semantics

The main judgment E P : {G 1 , . . . , G n } of the effect system for the π-calculus means that the process P uses names according to their types and that all its external reads and writes are on channels in groups G 1 , . . . , G n . A channel type takes the form G[T 1 , . . . , T n ]\H. This stipulates that the name is in group G and that it is a channel for the exchange of n-tuples of names with types T 1 , . . . , T n . The set of group names H is the hidden effect of the channel. In the common case when H = ∅, we abbreviate the type to G[T

f : ρ [Lit[], K[Lit[]]] and g : ρ[Lit[], K[Lit[]]].
Given these typings for names, we have g(y, k ).f y, k : {ρ, ρ } because the reads and writes of the process are on the channels g and f whose groups are ρ and ρ . Similarly, we have f (x, k ).k x : {ρ , K} and g 5, k : {ρ}. The composition of these three processes has effect {ρ, ρ , K}, the union of the individual effects.

The idea motivating hidden effects is that an input process listening on a channel may represent a passive resource (for example, a function) that is only invoked if there is an output on the channel. The hidden effect of a channel is an effect that is masked in an input process, but incurred by an output process. In the context of our example, our formal translation makes the following type assignments:

f : ρ [Lit[], K[Lit[]]]\{K} and g : ρ[Lit[], K[Lit[]]
]\{K, ρ }. We then have f (x, k ).k x : {ρ }, g(y, k ).f y, k : {ρ}, and g 5, k : {ρ, ρ , K}. The hidden effects are transferred from the function bodies to the process g 5, k that invokes the functions. This transfer is essential in the proof of our main garbage collection result, Theorem 5.

The effect of a replicated or name-restricted process is the same as the original process. For example, abbreviating the types for f and g, we have:

(νf :ρ )(νg:ρ)(!f (x, k ).k x | !g(y, k ).f y, k | g 5, k ) : {ρ, ρ , K}.
On the other hand, the effect of a group-restriction (νG)P is the same as that of P , except that G is deleted. This is because there can be no names free in P of group G; any names of group G in P must be internally introduced by namerestrictions. Therefore, (νG)P has no external reads or writes on G channels. For example, (νρ

)(νf )(νg)(!f (x, k ).k x | !g(y, k ).f y, k | g 5, k ) : {ρ, K}.
The following tables describe the syntax of types and environments, the judgments and the rules defining our effect system. Let fg(G[T 1 , . . . , T n ]\H)

∆ = {G} ∪ fg(T 1 ) ∪ • • • ∪ fg(T n ) ∪ H.
(Env ∅) ∅ (Env x) E T x / ∈ dom(E) E, x:T (Env G) E G / ∈ dom(E) E, G (Type Chan) E {G} ∪ H ⊆ dom(E) E T 1 • • • E T n E G[T 1 , . . . , T n ]\H (Exp x) E , x:T, E E , x:T, E x : T (Proc Input) E x : G[T 1 , . . . , T n ]\H E, y 1 :T 1 , . . . , y n :T n P : G E x(y 1 :T 1 , . . . , y n :T n ).P : {G} ∪ (G -H) (Proc Output) E x : G[T 1 , . . . , T n ]\H E y 1 : T 1 • • • E y n : T n E x
P : G E Q : H E P | Q : G ∪ H (Proc Repl) E P : H E !P : H (Proc Zero) E E 0 : ∅ (Proc Subsum) E P : G G ⊆ H ⊆ dom(E) E P : H
The rules for good environments and good channel types ensure that declared names and groups are distinct, and that all the names and groups occurring in a type are declared. The rules for good processes ensure that names are used for input and output according to their types, and compute an effect that includes the groups of all the free names used for input and output.

In the special case when the hidden effect H is ∅, (Proc Input) and (Proc Output) specialise to the following: In this situation, we attribute all the effect G of the prefixed process P to the input process x(y 1 :T 1 , . . . , y n :T n ).P . The effect G of P is entirely excluded from the hidden effect, since H = ∅.

A dual special case is when the effect of the prefixed process P is entirely included in the hidden effect H. In this case, (Proc Input) and (Proc Output) specialise to the following: The effect of P is not attributed to the input x(y 1 :T 1 , . . . , y n :T n ).P but instead is transferred to any outputs in the same group as x. If there are no such outputs, the process P will remain blocked, so it is safe to discard its effects.

These two special cases of (Proc Input) and (Proc Output) are in fact sufficient for the encoding of the region calculus presented in Section 4; we need the first special case for typing channels representing continuations, and the second special case for typing channels representing function pointers. For simplicity, our actual rules (Proc Input) and (Proc Output) combine both special cases; an alternative would be to have two different kinds of channel types corresponding to the two special cases.

The rule (Proc GRes) discards G from the effect of a new-group process (νG)P , since, in P , there can be no free names of group G (though there may be restricted names of group G). The rule (Proc Subsum) is a rule of effect subsumption. We need this rule to model the effect subsumption in rule (Exp Fun) of the region calculus. The other rules for good processes simply compute the effect of a whole process in terms of the effects of its parts.

We can prove a standard subject reduction result.

Proposition 3. If E P : H and P → Q then E Q : H.

Next, a standard definition of the barbs exhibited by a process formalizes the idea of the external reads and writes through which a process may interact with its environment. Let a barb, β, be either a name x or a co-name x.

Exhibition of a barb: P ↓ β x(y 1 :T 1 , . . . , y n :T n ).P ↓ x

x y 1 , . . . , y n ↓ x P ↓ β (νG)P ↓ β P ↓ β β / ∈ {x, x} (νx:T )P ↓ β

P ↓ β P | Q ↓ β P ≡ Q Q ↓ β P ↓ β
The following asserts the soundness of the effect system. The group of any barb of a process is included in its effect.

  allocation of v at ρ x(y) application let x = a in b sequencing letregion ρ in b region allocation, de-allocation u, v ::= boxed value λ(x:A)b function

  e ::= {ρ 1 , . . . , ρ n } effect A, B ::= type of expressions Lit type of literals (A e → B) at ρ type of functions stored in ρ E ::= environment ∅ empty environment E, ρ entry for a region ρ E, x:A entry for a name x Let fr (A) be the set of region variables occurring in the type A. We define the domain, dom(E), of an environment, E, by the equations dom(∅) = ∅, dom(E, ρ) = dom(E) ∪ {ρ}, and dom(E, x:A) = dom(E) ∪ {x}.

  , x:A b : e B E let x = a in b : e∪e B (Exp Letregion) E, ρ a : e A ρ / ∈ fr (A) E letregion ρ in a : e-{ρ} A (Exp Fun) E, x:A b : e B e ⊆ e {ρ} ∪ e ⊆ dom(E) E λ(x:A)b at ρ : {ρ} (A e → B) at ρ

  E x : G[T 1 , . . . , T n ]\∅ E, y 1 :T 1 , . . . , y n :T n P : G E x(y 1 :T 1 , . . . , y n :T n ).P : {G} ∪ G E x : G[T 1 , . . . , T n ]\∅ E y 1 : T 1 • • • E y n : T n E xy 1 , . . . , y n : {G}

  E x : G[T 1 , . . . , T n ]\H E, y 1 :T 1 , . . . , y n :T n P : H E x(y 1 :T 1 , . . . , y n :T n ).P : {G} E x : G[T 1 , . . . , T n ]\H E y 1 : T 1 • • • E y n : T n E x y 1 , . . . , y n : {G} ∪ H

  These predicates roughly correspond to the co-inductively defined consistency predicate of Tofte and Talpin. The retention of defunct regions in our semantics allows a simple inductive definition of these predicates, and a routine inductive proof of the subject reduction theorem stated below.We now present a subject reduction result relating the static and dynamic semantics. Let H H if and only if the pointers defined by H and H are disjoint, that is, dom 2 (H) ∩ dom 2 (H ) = ∅. Assuming that H H , we write H + H for the heap consisting of all the regions in either H or H ; if ρ is in both heaps, (H + H )(ρ) is the concatenation of the two regions H(ρ) and H(ρ ).

		n
	(Heap Typing Good)	(Heap Good) (where dom(H) = dom(h))
	env (H)	env (H) h(ρ) at ρ : H(ρ) ∀ρ ∈ dom(H)
	H |=	H |= h
	Theorem

(Config Good) (where S ⊆ dom(H)) env (H) a : e A e ∪ fr (A) ⊆ S H |= h H |= S • (a, h) : A 1. If H |= S • (a, h) : A and S • (a, h) ⇓ (p , h ) there is H such that H H and H + H |= S • (p , h ) : A.

  = x 2 ⇒ (νx 1 :T 1 )(νx 2 :T 2 )P ≡ (νx 2 :T 2 )(νx 1 :T 1 )P , . . . , y n | x(z 1 :T 1 , . . . , z n :T n ).P → P {z 1 ←y 1 } • • • {z n ←y n } (Red Interact)

		Par Assoc)
	!P ≡ P | !P	(Struct Repl Par)
	x 1 (Struct Res Res)
	x / ∈ fn(P ) ⇒ (νx:T )(P | Q) ≡ P | (νx:T )Q	(Struct Res Par)
	(νG 1 )(νG 2 )P ≡ (νG 2 )(νG 1 )P	(Struct GRes GRes)
	G / ∈ fg(T ) ⇒ (νG)(νx:T )P ≡ (νx:T )(νG)P	(Struct GRes Res)
	G / ∈ fg(P ) ⇒ (νG)(P | Q) ≡ P | (νG)Q	(Struct GRes Par)
	Reduction: P → Q
	x y 1

  1 , . . . , T n ]. As examples of groups, in our encoding of the region calculus we have groups Lit and K for literals and continuations, respectively, and each region ρ is a group. Names of type Lit[] are in group Lit and exchange empty tuples, and names of type K[Lit[]] are in group K and exchange names of type Lit[]. In our running example, we have 5 : Lit[] and k : K[Lit[]]. A pointer to a function in a region ρ is a name in group ρ. In our example, we could have

Acknowledgements Luca Cardelli participated in the initial discussions that led to this paper. We had useful conversations with Cédric Fournet, Giorgio Ghelli and Mads Tofte. Luca Cardelli, Tony Hoare, and Andy Moran commented on a draft.

 Proposition 4. If E P : H and P ↓ β with β ∈ {x, x} then there is a type G[T 1 , . . . , T n ]\G such that E x : G[T 1 , . . . , T n ]\G and G ∈ H.

Encoding Regions as Groups

This section interprets the region calculus in terms of our π-calculus. Most of the ideas of the translation are standard, and have already been illustrated by example. A function value in the heap is represented by a replicated input process, awaiting the argument and a continuation on which to return a result. A function is invoked by sending it an argument and a continuation. Region names and letregion ρ are translated to groups and (νρ), respectively.

The remaining construct of our region calculus is sequencing: let x = a in b. Assuming a continuation k, we translate this to (νk

This process invents a fresh, intermediate continuation k . The process [[a]]k evaluates a returning a result on k . The process k (x). [[b]]k blocks until the result x is returned on k , then evaluates b, returning its result on k.

The following tables interpret the types, environments, expressions, regions, and configurations of the region calculus in the π-calculus. In particular, if S • (a, h) is a configuration, then [[S •(a, h)]]k is its translation, a process that returns any eventual result on the continuation k. In typing the translation, we assume two global groups: a group, K, of continuations and a group, Lit, of literals. The environment [[∅]] declares these groups and also a typing i :Lit for each of the literals 1 , . . . , n .

Translating of the region calculus to the π-calculus: In the following equations, where necessary to construct type annotations in the π-calculus, we have added type subscripts to the syntax of the region calculus. The notation i∈I P i for some finite indexing set I = {i 1 , . . . , i n } is short for the composition

Translation rules:

The following theorem asserts that the translation preserves the static semantics of the region calculus.

Theorem 2 (Static Adequacy).

(1)

Next we state that the translation preserves the dynamic semantics. First, we take our process equivalence to be barbed congruence [START_REF] Milner | Barbed bisimulation[END_REF], a standard operational equivalence for the π-calculus. We use a typed version of (weak) barbed congruence, as defined by Pierce and Sangiorgi [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF]; the long version of this paper contains the detailed definition. Then, our theorem states that if one region calculus configuration evaluates to another, their π-calculus interpretations are equivalent. In the following, let E P mean there is an effect G such that E P : G. Typed process equivalence: E P ≈ Q For all typed processes P and Q, let E P ≈ Q mean that E P and E Q and that P and Q are barbed congruent.

Recall the evaluations of the examples ex 1 and ex 2 given previously. From Theorem 3 we obtain the following equations (in which we abbreviate environments and types for the sake of clarity):

Next, we present a general π-calculus theorem that has as a corollary a theorem asserting that defunct regions may be deleted without affecting the meaning of a configuration.

Suppose there are processes P and R such that R has effect {G} but G is not in the effect of P . So R only interacts on names in group G, but P never interacts on names in group G, and therefore there can be no interaction between P and R. Moreover, if P and R are the only sources of inputs or outputs in the scope of G, then R has no external interactions, and therefore makes no difference to the behaviour of the whole process. The following makes this idea precise equationally. We state the theorem in terms of the notation (νE)P defined by the equations: (ν∅)P Now, by applying this theorem, we can delete the defunct region ρ from our two examples. We obtain:

The first equation illustrates the need for hidden effects. The hidden effect of g is {K, ρ }, and so the overall effect of the process [[g → λ(y)f (y)]] | k 5 is simply {ρ, K}. This effect does not contain ρ and so the theorem justifies deletion of the process [[f → λ(x)x]], whose effect is {ρ }. In an effect system for the π-calculus without hidden effects, the effect of [[g → λ(y)f (y)]] | k 5 would include ρ , and so the theorem would not be applicable.

A standard garbage collection principle in the π-calculus is that if f does not occur free in P , then (νf )(!f (x, k).R | P ) ≈ P . One might hope that this principle alone would justify de-allocation of defunct regions. But neither of our example equations is justified by this principle; in both cases, the name f occurs in the remainder of the process. We need an effect system to determine that f is not actually invoked by the remainder of the process.

The two equations displayed above are instances of our final theorem, a corollary of Theorem 4. It asserts that deleting defunct regions makes no difference to the behaviour of a configuration:

Conclusions

We showed that the static and dynamic semantics of Tofte and Talpin's region calculus are preserved by a translation into a typed π-calculus. The letregion construct is modelled by a new-group construct originally introduced into process calculi in the setting of the ambient calculus [START_REF] Cardelli | Ambient groups and mobility types[END_REF]. We showed that the rather subtle correctness of memory de-allocation in the region calculus is an instance of Theorem 4, a new garbage collection principle for the π-calculus. The translation is an example of how the new-group construct accounts for the type generativity introduced by letregion, just as the standard new-name construct of the π-calculus accounts for dynamic generation of values.

Banerjee, Heintze, and Riecke [START_REF] Banerjee | Region analysis and the polymorphic lambda calculus[END_REF] give an alternative proof of the soundness of region-based memory management. Theirs is obtained by interpreting the region calculus in a polymorphic λ-calculus equipped with a new binary type constructor # that behaves like a union or intersection type. Their techniques are those of denotational semantics, completely different from the operational techniques of this paper. The formal connections between the two approaches are not obvious but would be intriguing to investigate. A possible advantage of our semantics in the π-calculus is that it could easily be extended to interpret a region calculus with concurrency, but that remains future work. Another line of future work is to consider the semantics of other region calculi [START_REF] Aiken | Better static memory management: Improving region-based analysis of higher-order languages[END_REF][START_REF] Crary | Typed memory management in a calculus of capabilities[END_REF][START_REF] Hughes | Recursion and dynamic data-structures in bounded space: Towards embedded ML programming[END_REF] in terms of the π-calculus. Finally, various researchers [START_REF] Moggi | Monadic encapsulation of effects: a revised approach[END_REF][START_REF] Semmelroth | Monadic encapsulation in ML[END_REF] have noted a connection between the monadic encapsulation of state in Haskell [START_REF] Launchbury | State in Haskell[END_REF] and regions; hence it would be illuminating to interpret monadic encapsulation in the π-calculus.


Promoting an Institute: An essential obligation for Technical Education Evolution

Keywords: Enrollments, Segmentation, Promotion Mix, Technical Education

Purpose:Technical education in India contributes a major share to the overall education system and plays a vital role in the social and economic development of the nation. Despite of rapid growth of technical education in last decade in terms of the no. of institutes and intake capacity in India, institutes failed to attract enrollments. Last three years saw, increasing gap in between the actual no. of enrollments and intake capacity; 46% of seats were vacant in Technical Education in India in 2015. The purpose of this paper is to highlight institute's role in promoting enrollments in Technical education. Design methodology: A qualitative research by a survey (through a structured questionnaire) of students who are presently enrolled (Current-students) and those who have completed their study (Alumni) belonging to the institutes offering Technical Education situated in Khandesh region of India and affiliated to the North Maharashtra University, Jalgaon. Findings: The study found that diversified characteristics of enrollments are related with the promotion mix of TE institute in selection of technical educational institute. This study investigates the usefulness of school visits, institution publications, websites, campus visits, word-of-mouth (friends, alumni, school teachers), advertisements (radio, television, magazines) and events on campus, as a tool of promotion. Social Networking and Institute's Website are the new forms of promotion mix in selection TE institute in rural part of India.

Research limitations:

The survey is delimited to the enrollments of technical education belonging to North Maharashtra University, Jalgaon and located in Khandesh region of India. Practical implications 60-70% of population belongs to rural part of India. Different promotional strategies of promotion mix can be used based on geographic and demographic segmentation. This will enhance, making awareness, fondness regarding Technical Education in the rural part and will act as lubricant in decision making of selecting their technical educational institute.

INTRODUCTION

Technical education is a basic and essential input for national development and for strengthening of the industry, economy and ultimately improving the quality of life of the people. It has made a significant contribution to India's economic development. Technical Education contributes 23% in terms of enrollments in higher education in India [START_REF]Data Source: Government of India[END_REF]. The program which have advanced the country and diversified and augmented its production since independence are largely because of the man power produced by technical institution of the country. Technical education contributes substantially to the socio-economic development of the country [START_REF] Kasturirangan | Technical education and national development[END_REF]. The economic growth of a country largely depends on technological improvements and on its scientific and technical manpower. Technical education, therefore, has a crucial role in speeding up the country's industrial development. It provides one of the most potent means for development of skilled manpower as required by various sectors in the country's economy. India possesses Asia's oldest, largest and most diverse infrastructure for scientific and technical training that has made important contributions to the country's scientific and industrial development [START_REF] Dasgupta | Urban Affairs and Employment[END_REF]. Literature showed, historically, institutes & universities have been extremely slow in adapting to societal change [START_REF] Smith | Marketing Planning for Colleges & Universities[END_REF]. [START_REF] Kotler | A Generic Concept of Marketing[END_REF], has an argument that marketing is a generic concept applicable to all organizations (not just profit seeking business corporations), various sectors of our society have "discovered marketing" [START_REF] Kotler | A Generic Concept of Marketing[END_REF]. While laggards to the adoption of a marketing orientation, many universities have now adopted the conscious practice of strategic marketing [START_REF] Kotler | Strategic Planning for Higher Education[END_REF]. Because marketing and strategy are not at the top of the administration's things-to-do list, many institutes find themselves in reactive positions to repair damages left from their inability to adjust. Whether it is higher education or business, the strategic framework should be underpinned by the same characteristics: reflective, innovative, brand supportive dominant logic and exceptional capabilities [START_REF] Beverland | Industrial global brand leadership[END_REF]. According to Darrell Norman Bureell, Brain C, [START_REF] Bureell | Competitive Marketing and Planning Strategy in Higher Education[END_REF], the most successful institutes will be those that can do strategic marketing planning carve out niches and fulfill needs of students by adding valuable services that will drive students to the institution [START_REF] Bureell | Competitive Marketing and Planning Strategy in Higher Education[END_REF]. Part of this planning will include investment in advertising and marketing initiatives aimed at developing institutional brand names and student prospect leads. Growth in this climate will be hinged on organizational changes that support environment that is market driven and sales oriented. Because today's students have so many choices, enrollment personnel must become more skilled at selling prospective students on the benefits of their institution over another [START_REF] Levine | The future of colleges: 9 inevitable Changes[END_REF]. Johnson and Jones (2006), in ‗Declining Interest in Engineering Studies at a Time of Increased Business Need', have stated that the area of concern in the engineering education pipeline is the lack of diversity in the student population [START_REF] Wayne | Declining Interest in Engineering Studies at a Time of Increased Business Need[END_REF]. They suggested to expand precollege efforts at attracting women into the engineering education pipeline and enhance the public understanding of engineering and its contributions to society. P.B. Sathivel (2003) see demographic variable like type of institutions, gender of respondents, size of institutions, age of institutions and commitment of top management and its leadership as major factor in attracting the prospective students [START_REF] Sathivel | TQM Implementation and students' satisfaction of academic performance[END_REF]. He also emphasis on some value based education services like customer focus, course delivery, communication, campus facilities learning environment as major factors. Kelley and Mahady (2003:2) believe that promotion is an element sometimes overlooked by non-profit organizations [START_REF] Kelley | Marketing for non-profit organizations -Introduction[END_REF]. The increasingly competitive higher education market, which began decades ago and continues today, has more recently pushed colleges and universities to evaluate their identity and their image, establish what their strengths and weakness are, and develop a clear mission and vision that reflects organizational identity and aspiration as colleges and universities develop strategies for positioning or repositioning themselves [START_REF][END_REF].

PROMOTION MIX AND HOLISTIC MARKETING

Promotion is a process of communication between an institute and service user with an aim to create a positive attitude on services, which leads accepting services. An effective communication understands that the institute knows students' needs and wishes. The marketing communicator must make the following decisions [START_REF] Kotler | Strategic marketing for educational institutions[END_REF]: (1) identify the target audience, (2) clarify the sought response, (3) develop a message, (4) choose the medium or media, (5) select source attributes, and (6) collect feedback. Lamb et al. (2004:466) describe the promotional strategy as a plan for the optimal use of the elements of promotion, namely advertising, sales promotion, publicity and personal selling [START_REF] Kotler | Strategic marketing for educational institutions[END_REF]. Higher education institutions are making use of radio, television, newspapers, buses, taxis and open days as well as more professional brochures and promotional material as vehicles for communication Higher education institutions are the senders, while the receivers of the message are the potential students, existing students, parents, employers or alumni. The most popular communication/promotion objectives are general image enhancement and awareness of the institutions [START_REF] Kittle | Institutional advertising in higher education[END_REF]. [START_REF] Kotler | Strategic marketing for educational institutions[END_REF] view that Higher education institutions need to select a medium that will attract attention, arouse interest and present the message clearly. Higher education institutions need knowledge about the language of the prospective students, knowledge of forms of communication and general background information about the prospective students in order to encode successfully. [START_REF] Laurer | Advancing higher education in uncertain times[END_REF] suggests that institutions must coordinate all the promotional elements so that they meet the needs of students and parents who will pay for their products and services [START_REF] Laurer | Advancing higher education in uncertain times[END_REF]. As Technical Education (TE) in India is turning more competitive, it has become necessary for TE institutions to engage in strategic marketing. More than promotional activities, strategic marketing involves to draw students toward the institution; it should also include market segmentation and positioning [START_REF] Cann | Key elements of a successful drive toward marketing strategy making[END_REF]. The reason why segmentation is important and timely is that universities and institutes are currently struggling with how to best serve their learners in the face of declining financial resources, increased calls for accountability by Government, increasing competition among institutions and more discerning students, particularly those referred to as the ‗millennials' [START_REF] Howe | Millennials rising: the next great generation[END_REF]. The holistic marketing concept is based on the development, design, and implementation of marketing programs, processes, and activities that recognizes their breadth and inter-dependencies. Holistic marketing recognizes that "everything matters" with marketing-and that a broad, integrated perspective is often necessary. Four components of holistic marketing are relationship marketing, integrated marketing, internal marketing, and social responsibility marketing [START_REF] Kevine | Holistic Marketing -A broad, Integrated Prospective to Marketing Management[END_REF]. Internal marketing: Internal marketing refers to the process of planning and executing marketing activities aimed at the creation and improvement of exchange processes within the organization. The goal of internal marketing is to accomplish the organization's objectives and communication processes in a more efficient and effective way [START_REF] Lamb | Marketing management[END_REF]. Internal marketing ensures that the promises made by the marketing function of TE institutions to external markets are delivered. For internal marketing to be effective and function properly, various process is needed: exchanges between the institutions and their staff & current-students, exchanges between top management and the departments, exchanges between different departments, and exchanges between the department and current-students and alumni. In internal marketing communication flows, vertically as well as in horizontal directions. In addition, [START_REF] Ahmed | Internal Marketing and the Mediating role of Organizational Competencies[END_REF] propose the concept of IM mix or set of controllable instrument inside the organizational that can be used effectively to influence employees so that they are motivated and acted in customer-oriented fashion [START_REF] Ahmed | Internal Marketing and the Mediating role of Organizational Competencies[END_REF]. Lamb et al. (2004:323) express that opinion that relationship selling emphasizes a win-win situation and the accomplishment of mutual objectives that benefit both the buyer and seller in the long-term. Integrated marketing: Integrated marketing communications (IMC) is an expansion of modern and traditional marketing strategies, to optimize the communication of a consistent message conveying the company's brands to stakeholders [START_REF] Kitchen | Integrated marketing communications: Making it work at a strategic level[END_REF]. Integrated Marketing is an approach to creating a unified and seamless experience for consumers to interact with the brand/enterprise; it attempts to meld all aspects of marketing communication such as advertising, sales promotion, public relations, direct marketing, and social media, through their respective mix of tactics, methods, channels, media, and activities, so that all work together as a unified force. It is a process designed to ensure that all messaging and communications strategies are consistent across all channels and are centered on the customer [START_REF] Belch | Advertising and promotion: An integrated Marketing communications perspective[END_REF]. Integrated marketing communication enables all aspects of service mix to work together in harmony to promote institute's service effectively among end-users.

promote their brands, logos and products. Social responsibility is a factor of why companies get involved in sponsorship. Sponsorship of schools can help boost the reputation of a company in its given community. This will give a caring and socially responsible image to the consumers [START_REF] Jobber | Principles and Practice of Marketing[END_REF]. It creates social impact on community. Institutes sponsors sports event, cultural nights, technical symposium or competitions; even they sponsor social events like health & medical camps, education fairs, cleanliness drive etc. Attributes of such events are then associated with sponsored institutes. TE institutes use sponsoring programs to improve goodwill, enhancing image, increase awareness, staff and student's recruitment and to create competitive advantage. Publicity: It is non-paid form of promotion which may be due to the customers ‗word of mouth' with the other customers or with the community. Institute's best publicity is through the news published in the newspapers. It creates a huge impact on customers as well as on community. TE institutes can make use of public relations and publicity, not only to maintain a positive image but also to educate the public about the institutions' goals, objectives, introduce new programs. [START_REF] Chester | EDU Internet strategies to market higher education organizations[END_REF] believes the new tool that higher education institutions must make use of is writing press releases or articles that will be highly visible on search engines like Google [START_REF] Chester | EDU Internet strategies to market higher education organizations[END_REF]. Publicity is directly related to the attitude of institute towards its service and the satisfaction of the customers towards the service delivered. Institute that delivers quality service and have satisfied customers are more likely to get positive publicity. Institutes have now started to follow social networking (Facebook, twitter, LinkedIn) for their publicity. More likes, more followers; more favorable the institute is. Direct Marketing through E-mail, SMS and Telephonic Communication: Direct marketing is defined as the use of mail, telephone, fax, e-mail and other non-personal tools to communicate directly with specific consumers to obtain a direct response [START_REF] Du Plessis | Buyer behavior: A multi-cultural approach[END_REF]. This form of promotion used when the institute has known customers with the database of customer. Institute design highly focused communication with highlighting features. Institute can even negotiate on the financial aspects. Social and Digital marketing: Webpages and brochures must be user-friendly and reflect the image of the institution. Students are making use of search engines as a tool for finding higher education institutions [START_REF] Seymour | Giving the Web the new college try: Students online surf to sample life on campus[END_REF]. The terms -social‖ and -digital‖ refer to the use of both social media and digital marketing more generally, and include the role of effective and intuitive websites. Institutes are making greater use of social media and digital platforms like Twitter, Facebook, YouTube, and podcasts to market their programs, while website design and interface is proving a crucial component in how institutes present themselves to prospective students. The latest poll indicated that 100 percent of respondent institutions are now using some form of social mediabut there is no reliable data on how effective the use of such tools are in terms of enrollment or elevating institutional value [START_REF] Barnes | Social Media Adoption Soars as Higher-Ed Experiments and Reevaluates Its Use of New Communications Tools[END_REF].

Relationship marketing

It is a key goal of marketing is to develop deep, enduring relationships with all customers of TE that could directly or indirectly affect the success of the institute's marketing activities. American Marketing Association (AMA) defines relationship marketing as Marketing is an organizational function and a set of processes for creating, communicating and delivering value to customers and for managing customer relationships in ways that benefit the organization and its stakeholders.' As per [START_REF] Morgan | The commitment-trust theory of relationship marketing[END_REF]; ‗RM refers to all marketing activities toward establishing, developing, and maintaining successful relational exchanges' [START_REF] Morgan | The commitment-trust theory of relationship marketing[END_REF]. TE institutes through relationship management seek to create new value for its customers and then share it with other customers. Relationship management represents continuous cooperative effort between the institutes and students, parents, schools, alumni and community. Despite of fee reimbursement schemes of Central Government of India for ecumenical backward and category students with some fee concessions offered by TE institutes at institute levels, TE institutes have failed to attract enrollments. Every year 60-70% of students are benefited through these schemes. This created an importance of holistic marketing and promotion mix to encourage the enrollments in TE.

Conceptual framework of Promotion Mix in Technical Education

Relationship

RESEARCH METHODOLOGY

The objective of this research was to find out people's influence, which is a referred group for a student, on the geographic and demographic characteristics in selection of technical educational institute for a student.

A qualitative research through a survey was made. It comprised of a structured questionnaire sent through email to the current-students enrolled and passed-out students (alumni .05 for all these promotional mix. The strength of relationship can be measured by F-value, which is high for Institute Website, Social Networking, Face-to-face counseling and Educational fairs, which indicates that these promotional mixes are highly associated with the gender. However, based on the same test, there is no difference in gender (male & female) on the influence of Visual/Air Media (p=0.163) and Banners/Hoardings (p=0.142), where p value is >0.05. We reject H1 for these influencers.

)
It can be seen from bar-chart that mean of female responses on the influence of all promotion mix is higher than male students which indicates that female students have more influence of promotional mix in selecting TE institute than male students.

Descriptive statistics of influence of promotion mix on Native Place in selecting TE Institute. Bar-chart 2 represents mean of responses given by students residing in District, taluka and Village place on promotion mix which influenced them in selecting TE institute. Table 2 shows MANOVA calculated for all responses combined is significant at 0.05 i.e. p =0.002<0.05 with F-value 2.252. Hypothesis H1 is accepted for native place. This means, there is difference in between students residing in District, Taluka and Village place in accepting ‗Promotion Mix' as an influencer. Responses of these students are not same on at least for one promotion mix. Table 2 shows F-value and p-value of responses of students as per their native place on Promotion Mix in the selection of TE institute, calculated with On-Way ANOVA by Minitab 17. There is a relationship between native place of students and influence of promotional mix on them in selecting TE institute. Banners/Hoardings (F-value= 5.43, p-value= 0.005), Face-to-face counseling (F-value= 4.64, p-value= 0.010), Educational fairs (F-value= 9.46, p-value= 0.000), Brochure/leaflet (F-value= 4.21, p-value= 0.015), Sponsorship Programs (F-value= 9.94, p-value= 0.000) are significant at 0.05; as p<0.05 for all these promotional mixes and hence their influences are related to the native place of students. The strength of relationship can be measured by F-value, which is high for Educational fairs, Sponsorship Programs & Banners/Hoardings which indicates that these promotional mixes are highly associated with their Native Place. However, based on the same test, there is no difference in the responses given by students residing in District, taluka and Village place on the influence of Visual/Air Media (p=0.223), institute Website (p=0.082) and Publicity (p=0.062), where p value is >0.05. We reject H1 for these influencers.

It can be seen from bar-chart 2 that Banners/Hoardings (mean=2.67) have created much impact on Village students than the District (mean=2.10) and Taluka students (mean=2.84). Similarly, Face-to-face counseling, Educational fairs, Brochure/leaflet and Sponsorship Programs for which mean of responses belonging to Village students is higher than the mean of students belonging to District and Taluka place which shows Village students are more influenced by these promotional mixes than District and taluka students in selecting TE institutes. Descriptive statistics of influence of promotion mix on Technical Program in selecting TE institute. Bar-chart 3 shows mean of responses given by students admitted in Engineering, Management and Pharmacy on promotion mix which influenced them in selecting TE institute. Table 3 shows MANOVA calculated for all responses combined is significant at 0.05 i.e. p =0.000<0.05 with F-value 3.241. Hypothesis H1 is accepted for Technical Program. This means, there is difference in between students admitted in different Technical Program in accepting ‗Promotion Mix' as an influencer. Responses of these students are not same on at least for one promotion mix.

CONCLUSION

It is important to know institute's strongest influencers and the customers of technical education, so that the institute can create a communication and promotional strategy that incorporates them into the outreach process. Technical Educational (TE) institutions need to communicate effectively with their target groups. TE institutes must inform students and parents about its brand, program offered, its goals, service activities facilities available, campus life and culture and offerings and should motivate them to take an interest in the institution. Everything and everybody in an institution shall have a responsibility of communicating all information related to institute. While some prospective students share similar characteristics but most of them are not similar in gender, age, geographical location, parent's income etc. Students with similar characteristics can be grouped and can be yielded for definable segments. Technical Education (TE) institutions communicate with various groups (students, parents, donors, employees and community), whose interests vary. Schools, universities and other educational institutions are interested in achieving understanding and sympathy of the public. The public, particularly, can affect attitudes and behavior of other members of external environment through an institution. Their enthusiasm will additionally motivate the teachers, professors, to improve their services. In addition, alumni can be generous donors and promoters of a faculty, and in that way students influence the attitudes and behavior of the remaining part of university public/ partners. Promotion, and especially promotion that provides a value service, can play a great part in increasing the visibility, prestige and status of institutes. The success key is to provide services to sources of pre-students, current-students, alumni and schools who in return through word of mouth marketing, make an effective marketing and public relation at low-cost. The most successful promotional efforts in the future will involve alumni and parents in developing promotional programs and generating publicity themselves with gentle oversight from the campus. Social media (engagement through Facebook pages, LinkedIn) is an important part of alumni, current-students and pre-students' engagement. It's a means to stay connected for long way and forever. The other source of low-cost of promotion is publicity. Publicity can be effortless when the institutes are in focus with their services, campaign, sponsorship programs and social activities through media; may be print or visual. Institute website can act as mirror image for the institute. It is a primary source and can be impressive source through creative design, informative stats and the depth of engagement. As one can now tell these are not futuristic and farfetched predictions. Emerging trends related to TE marketing suggest that there are numerous methods of recruiting and engaging with students, including institutional websites, mobile marketing, and social media, among others. As such, it is a crucial time to create an integrated branding and marketing approach that ties together these various approaches. All the areas discussed already exist at numerous institutions. Yet change with technology is difficult especially in TE institutes. Trustees need to accept new forms of promoting an institution and a holistic marketing approach by developing relationships and bonds with the community as their customer.

  belonging to the technical institutes affiliated to North Maharashtra University. Sample size (n) was calculated at 95% Confidence Level for which Standard Normal Variate (Z) is 1.96 & at Standard Error (e) of 0.03 by n=Z 2 (p)(1-p)/e 2 ; where n = Sample Size to be used for this study, N = unknown population, p = Estimated Portion of Population N. For p = 90%, ‗n' comes out to be 553. However, sample size of 655 was selected by quota sampling from technical institutes offering different programs in engineering, pharmacy and management & different students (Current as well Post-students) based on their location of native place, gender, father's qualification, occupation and income and technical educational program. The questionnaire comprised of geographic and demographic factors of students with questions measuring influencers impact on the selection of technical institute on a scale ranging from 0 to 5, where value zero, was no influence at all and value five, was most influence. The characteristics of the sample is described as below; represents mean of responses given by Male and Female on promotion mix which influenced them in selecting TE institute. Table1shows MANOVA calculated for all responses combined is significant at 0.05 i.e. p =0.010<0.05 with F-value 3.3. Hypothesis H1 is accepted for factor, gender. This means, there is difference in between male and female students in accepting ‗Promotion Mix' as an influencer. Male and Female responses are not same on at least for one promotion mix. Table1shows F-value and p-value of gender-wise responses on Promotion Mix in the selection of TE institute, calculated with On-Way ANOVA by Minitab 17. There is a relationship between Gender and

	Figures in bold are significant at 0.05. (p <0.05; confidence level 95%
					Visual/Air Media	Banners/Hoardings		Institute Website	Social Networking	Face-to-face	Counseling	Educational Fairs	Brochure/ Leaflet	Sponsorship	Program	Publicity	MANOVA for Gender Wilks'	by
		Gender	F-value	1.95	2.16	20.51 17.99 10.55 7.65	6.02	5.50	5.25	F-value= 3.3
			p-value	0.163 0.142 0.000 0.000 0.001 0.006 0.014 0.019 0.022 p-value= 0.010
	Bar-chart 1 influence of promotional mix; Institute Website (F-value= 20.51, p-value= 0.000), Social Networking (F-
	value= 17.99, p-value= 0.000), Face-to-face counseling (F-value= 10.55, p-value= 0.001), Educational fairs
	(F-value= 7.65, p-value= 0.006), Brochure/leaflet (F-value= 6.02, p-value= 0.014), Sponsorship Programs
	(F-value= 5.50, p-value= 0.019) and Publicity (F-value= 5.25, p-value= 0.022); which is significant at 0.05;
	By Gender as p<0
	Male: 447;				Female: 208
	By Native Place
	District: 162;				Taluka: 278;					Village: 215
	By Technical Educational Program
	Engineering: 486;			Pharmacy: 112;					Management: 57
	By Institute's Location
		District: 54;				Taluka: 578;					Village: 23
	Hypothesis
	H1:	Promotion mix which influences the selection of TE institute is associated with diversified students.
	DATA INTERPRETATION AND FINDINGS
	Descriptive statistics of influence of promotion mix on Gender in selecting TE institute.
		5 3 4	2.385	2.1767	2.519	2.2998	3.245	3.188 Bar-chart 1: Mean of Promotion Mix Genderwise 2.861 2.793 3.014 2.726 2.5861 2.5593 2.3468 2.3669 2.6555	2.3579	3	2.6465
		2
		1
		0
			Visual/Air Media	Banners/Hoardings	Institute Website Female Male Social Networking	Face-to-face	counseling	Educational Fairs	Brochure/Leaflet	Sponsorship Program	Publicity

Table 2 :

 2 Cells contains F-value & p-value obtained from One-Way ANOVA calculated from Minitab17: Figures in bold are significant at 0.05. (p <0.05; confidence level 95%

		Visual/Air Media	Banners/Hoardings	Institute Website	Social Networking	Face-to-face	Counseling	Educational Fairs	Brochure/ Leaflet	Sponsorship	Program	Publicity	MANOVA for Gender by Wilks'
	Native	F-value 1.5	5.43	2.51	2.49	4.64	9.46	4.21	8.94	2.79	F-value=2.252
	Place
		p-value 0.223 0.005 0.082 0.084 0.010 0.000 0.015 0.000 0.062 p-value=0.002

: Mean of Promotion Mix Vs Native Place

	5
	0 0.5 1 1.5 2 2.5 3 3.5 4 4.5	2.062	2.241 Visual/Air Media	2.381	2.105	2.58 Bar-chart 2District 2.506 2.284 2.773 2.784 2.679 2.986 Banners/Hoardings Institute Website Social Networking Taluka Village 2.916	2.13	2.579 Face-to-face counseling	2.707	1.981	2.59 Educational Fairs	2.781	2.451	2.799 Brochure/Leaflet	2.972	1.988	2.507 Sponsorship Program	2.8	2.463	2.86 Publicity	2.851

Table 3 :

 3 Cells contains F-value & p-value obtained from One-Way ANOVA calculated from Minitab17:

	Figures in bold are significant at 0.05. (p <0.05; confidence level 95%
		Visual/Air Media	Banners/Hoardings	Institute Website	Social Networking	Face-to-face	Counseling	Educational Fairs	Brochure/ Leaflet	Sponsorship	Program	Publicity	MANOVA for Gender Wilks'	by
	Technical	F-value 0.39	0.83	9.86	5.09	13.33 4.91	4.3	5.65	4.66	F-value= 3.241
	Program
		p-value 0.676 0.436 0.000 0.006 0.000 0.008 0.014 0.004 0.010 p-value= 0.000

Table 3

 3 is presented with F-value and p-value of responses of students admitted in different technical programs; engineering, management and pharmacy, on their influence of Promotion Mix in the selection of TE institute, calculated with On-Way ANOVA by Minitab 17. There is a relationship between such students who differs by technical program and influence of promotional mix on them in selecting TE institute. -value= 4.66, p-value= 0.010) are significant at 0.05; as p<0.05 for all these promotional mixes and hence their influences are related to the students admitted in different Technical Programs. The strength of relationship can be measured by F-value, which is high for Face-to-face Counseling & Institute Website which indicates that these promotional mixes are highly associated with types of Technical Programs.

	Institute website (F-value= 9.86, p-value= 0.000), Social Networking (F-value= 5.09, p-value= 0.006), Face-
	to-face counseling (F-value= 13.33, p-value= 0.000), Educational fairs (F-value= 4.91, p-value= 0.008),
	Brochure/leaflet (F-value= 4.3, p-value= 0.014), Sponsorship Programs (F-value= 5.65, p-value= 0.004) and
	Publicity (F

Mean of Promotion Mix Vs Technical Program

  on the same test, there is no difference in the responses given by students differed by type of Technical Program on the influence of Visual/Air Media (p=0.676), Banners/Hoardings (p=0.436), where p value is >0.05. We can reject H1 for these influencers. Students admitted in Management program are highly influenced by Education Fairs, Institute Website followed by the Pharmacy and Engineering students. Descriptive statistics of influence of promotion mix on Location of Institute in selecting TE institute. Bar-chart 4 shows mean of responses given by students admitted in institutes located at District, Taluka and Village on promotion mix which influenced them in selecting TE institute. Table4shows MANOVA calculated for all responses combined is significant at 0.05 i.e. p =0.002<0.05 with F-value 2.259. Hypothesis H1 is accepted. This means, there is difference in between students admitted in institutes located at District, Taluka and Village in accepting ‗Promotion Mix' as an influencer. Responses of these students are not same on at least for one promotion mix. Students admitted in different location of institutes have different opinions on accepting Banners/Hoardings (p-value=0.033, F-value=3.42) and Brochure/Leaflet (p-value=0.021, F-value=3.86) as an influencer in selecting TE institute. Students belonging to institutes located at Taluka have more impact of Banners/Hoardings (mean=2.433) and Brochure/Leaflet (mean=2.827) than the students belonging to institutes located at District and Village.

	However, based
	Engineering	Management	Pharmacy

Table 4 :

 4 Cells contains F-value & p-value obtained from One-Way ANOVA calculated from Minitab17:

	5
	4.5									Bi-
	2 2.5 3 3.5 4	2.111	2.284	1.522	2	2.433	1.652	2.667	2.822	2.435	2.667	2.756	3.043	2.481	2.531	2.043	2.185	2.563	2.391	2.537	2.827	1.87	2.278	2.51	2.043	2.722	2.798	1.87
	1.5
	1
	0.5
	0
			Visual/Air Media			Banners/Hoardings			Institute Website			Social Networking			Face-to-face counseling			Educational Fairs			Brochure/Leaflet			Sponsorship Program			Publicity
	Figures in bold are significant at 0.05. (p <0.05; confidence level 95%
							Visual/Air Media			Banners/Hoardings	Institute Website		Social Networking		Face-to-face	Counseling	Educational Fairs		Brochure/ Leaflet		Sponsorship	Program	Publicity	MANOVA for Gender Wilks'	by
	Location	F-value 2.21		3.42	0.69		0.36		0.74	0.94	3.86	1.01	2.83	F-value= 2.259
	of
	Institute
					p-value 0.110 0.033 0.501 0.695 0.480 0.392 0.021 0.365 0.060 p-value= 0.002

chart 4: Mean of Promotion Mix Vs Location of Institute

	However, there is no difference among the students differed by location of their institutes on the influence of
	Visual/Air Media (p=0.110), Institute Website (p=0.501), Social Networking (p=0.695), Face-to-face
	Counseling (p=0.480)
	District	Taluka	Village

, Educational Fairs (p=0.392), Sponsorship Program (p=0.365), and Publicity (p=0.060) where p value is >0.05. We can reject H1 for these influencers. SUMMARY OF FINDINGS

  It is found that female students, search and analyze all sources of primary information available through promotional activities. Institute website, social networking sites, face-to-face communication, education fairs, institute's print material, sponsorship and publicity programs have influenced them in selecting institute of TE of their choice. This is may be for, backing-up their decision and to convince their parents and family for the decision which is essential in case of female. It is surprising that, instead of less infrastructural facilities, rural students (belonging to village) are keen to search and gather information from institute websites and social networking sites. Villages students have considered all sources of promotion mix as well as they are influenced from these sources. Management students are influenced by all the promotional activities of institute ahead of engineering and pharmacy students. Engineering students are less influenced by the promotional mix, this means that they are searching new sources. Institutes who are placed in villages are concentrating only on social networking. They are lagging in other promotional mix. Institutes placed in urban are strong in their publicity program than the others. Institute those who are placed in urban area are strong in face-to-face interactions, website and print materials.