An important concern in programming language semantics is to find fully abstract models, where all the semantically equivalent programs are identified; for the so called interactive systems, labelled transition systems (LTS) equipped with bisimilarity provide a solution in simpler cases. Often, the semantics of a programming language has to deal with resource allocation. For example, in the π-calculus, mobility is achieved by allocating fresh communication channels. The LTS semantics is not completely satisfactory, since the definition of bisimu­lation is non-standard, due to the necessity of matching allocation on both sides of the bisimulation game. 
This problem is elegantly addressed by coalgebras over some presheaf cate­gory, that is, a functor category SetC . Each program is equipped with a type representing the available resources. Allocation functors can be combined with polynomials to take into account resource generation in the standard (coalge­braic) bisimulation. Varying the index category C, resources can have a rich structure. A well known case is when C is the category I offinite sets and injective relabellings; here the modelled resources are pure names. 
The presheaf approach makes it difficult to implement finite state methods such as partition refinement and model checking, since programs with the same “shape”, that only di.er for the identity of their resources, are not identified. In particular, this is a problem forfi.nite memory programs that allocate some resouces and discard other ones in a loop, giving rise to infinite models. In the case of pure names, the alternative approach of named sets allows one to specify coalgebras with local names, featuring an implicit garbage collection machinery. Pullback-preserving presheaves in SetI and named sets are linked by a categorical equivalence. 
In this talk, we see how the equivalence result extends to other index cat­egories, giving rise to the categorical model of families. Locality of interfaces leads to constructions that are typical when handling resources in computing. For example, the categorical product is made up of triples consisting of a pair of elements, and a binding between their local resources. We propose families as an alternative model for the semantics of resource-aware programming lan­guages, and explain how the categorical equivalence defines a framework where both approaches can be used simultaneously, for specification purposes on the side of presheaves, and implementation offinite state methods on the other side. 
 In this talk, we discuss the advantages and the open problems in
extending the equivalence result to other index categories, giving
rise to the categorical model of families. Locality of interfaces
leads to constructions that are typical when handling resources in
computing. For example, the categorical product is made up of triples
consisting of a pair of elements, and a binding between their local resources. We propose families as an alternative model for the semantics of resource-aware programming languages, and explain how the categorical equivalence defines a framework where both approaches can be used simultaneously, for specification purposes on the side of presheaves, and implementation of finite state methods on the other side.