How does employment density influence individuals’ wages? : A micro data approach.

We estimate the effect of employment density on wages in Sweden in a large geocoded data set on individuals and workplaces. Employment density is measured in four circular zones around each individual’s place of living. The data contains a rich set of control variables that we use in an instrumental variables framework. Results show a relatively strong but rather local positive effect of employment density on wages. Beyond 5 kilometers the effect becomes negative. This might indicate that the effect of agglomeration economies falls faster with distance than the effects of congestion.

Part-time employment within the Swedish retail business : – A study of part-time employment from a management perspective

Research question: How has the presence of PT employees affected the role of managers in the Swedish food retail business? Research purpose: The purpose of this paper was to describe the change that accompanies part-time employment from a management perspective, and particularly, describe how the presence of part-time employment has influenced the role of the manager within the Swedish food retail business. Conceptual framework: The main focused in this chapter is directed towards the role of managers. The basis of the conceptual framework consist of the model developed by Mintzberg including the ten managerial roles and Quinn's eight leadership roles and how the presence of PT employments might affect these roles. Methodology: In this paper, the authors adopted a qualitative design and used narrative inquiry as a research strategy in order to gain a deep understanding of the context. Semi- structured interviews have been collected through a self-selection sampling and the total number of participants was ten. Conclusions: Based on the findings of this paper the presence of PT employees have not influenced and changed the role of managers. The changes that have influenced and caused the change of the role of the managers constitutes of the increased workload, the delegations of tasks and responsibilities, changed positions, the change of the organisational structure of the individual store, and the increased workforce.

Fred: An approach to generating real, correct, reusable programs from proofs

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique to reduce higher-order logic to many-sorted (first-order) logic; 2. the free use of new rules for induction subject to certain conditions; 3. the extensive use of previously programmed (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). As an example of our system we give a constructive proof of the well known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.

Protocols between programs and proofs

In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the production of more powerful programs. The methodology we use for automatically extracting “correct” programs from proofs is a development of the well-known Curry-Howard process. Program extraction has been developed by many authors, but our presentation is ultimately aimed at a practical, usable system and has a number of novel features. These include 1. a very simple and natural mimicking of ordinary mathematical practice and likewise the use of established computer programs when we obtain programs from formal proofs, and 2. a conceptual distinction between programs on the one hand, and proofs of theorems that yield programs on the other. An implementation of our methodology is the Fred system. As an example of our protocol we describe a constructive proof of the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph as input, the extracted program produces a list of the (non-trivial) disjoint cycles as promised.

Extraction of structured programs from specification proofs

We present a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL. These programs are “correct” in the sense that they satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, is novel because it adds structural rules corresponding to the standard ways of modifying specifications: translating (renaming), taking unions, and hiding signatures. Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We use this to produce an executable refinement of a given specification and we then provide a method for producing a program module that maximally respects the original structure of the specification. Throughout the paper we demonstrate the technique with a simple example.