Search

Informed by the Social-Emotional and Character Development (SECD) approach to school turnaround, the present study examined the relationship between students’ recollection and reflection of their experience in a SECD program and academic achievement and explored the mediating effect of student-teacher relationships. Based on an intervention in an urban New Jersey school district, three data sources were used: program feedback surveys, student self-report surveys that assessed students on key SECD variables, and academic grades. The final sample consisted of 255 youths from two middle schools. Results demonstrated a significant relationship between SECD reflection and academic achievement. Partial mediation also was observed, with an indirect relationship between SECD reflection, student-teacher relationships, and academic achievement. Results of this study imply that positive SECD program reflections and student-teacher relationships can positively, and uniquely, impact academic achievement. Other implications of these findings for future research and practice, as well as the study’s strengths and weaknesses that may have contributed to these results, are discussed.

Chipping potatoes are bred for their ability to produce light-colored, defect-free chips. Chips with stem-end chip defect (SECD) have dark blemishes and are undesirable to consumers and chip processors. The heritability of SECD is not known and genetic loci linked to defect formation have not been identified. Chip processing varieties ‘Wauseon’ and ‘Lenape’ were crossed and tubers from parents and 191 progeny were evaluated over four years for chip color descriptors L*, a*, and b* and SECD score in January, March, and May. Broad sense heritability for SECD was 0.64 or greater at each sampling time. Genotype data were used to construct a 1282 cM linkage map. Nine quantitative trait loci (QTL) for SECD were detected, and seven overlapped QTL for chip color traits. The QTL identified are starting points for developing molecular markers that are used to select genotypes that produce light-colored chips and have resistance to SECD formation.

Considering the key role of social-emotional and character development (SECD) competencies in college, career, and life success — and considering that many of those competencies are teachable — there is no excuse for failing to incorporate them systematically into our education system. That would be the equivalent of depriving children of oxygen. This article is addressed to the U.S. Secretary of Education and other education policymakers and offers them specific recommendations to guide policy that would yield high-quality programs of support for SECD in all schools.

(Coinductive) natural semantics is presented as a unifying framework for the verification of total correctness of compilers in Coq (with the feature that a verified compiler can be obtained). In this way, we have a simple, easy, and intuitive framework, to carry out the verification of a compiler, using a proof assistant in which both cases are considered: terminating and non-terminating computations (total correctness).

Cooper and Wadler introduced the RPC calculus, which is obtained by incorporating a mechanism for remote procedure calls (RPC) into the lambda calculus. The location where a caller’s code is executed is designated in a lambda abstraction in the RPC calculus. Nishizaki et al. proposed a simplified abstract machine for the lambda calculus, known as a Simple Abstract Machine (SAM). The configuration of an SECD machine is a quadruple of data sequences: Stack, Environment, Code, and Dump. In contrast, the SAM configuration is a double of data sequences: Stack and Code. In this paper, we introduce a SAM-based abstract machine for the RPC calculus, called a Location-aware Simple Abstract Machine (LSAM). This machine makes it possible to model parallelism more clearly. We provide a translation of the RPC calculus into LSAM, and prove a correctness theorem for the translation. We then show that the translation can be extended to allow parallel execution in LSAM.

Bacteria, Archaea and Eukaryotes have evolved a plethora of mechanisms to translocate proteins across their various membranes. The bacterial Sec pathway is ubiquitous and essential for cell viability and is used by most proteins destined for the inner membrane, the periplasm or beyond. In bacteria, Sec system components include the heterotrimers SecY/SecE/SecG and SecD/SecF/YajC and the peripherally associated ATPase motor SecA. SecA in solution is mainly dimeric. Unexpectedly, structures of SecA dimers from different or even the same bacterium do not have a consistent dimerization interface. Analysis of the functional assembled translocase complexes blurs the picture even further as the functional quaternary state of the SecYEG channel is also disputed. Several experimental approaches tried to define the oligomeric state of SecA during preprotein 'pushing' through SecYEG. One high-resolution SecA-SecYEG complex has been visualized. This snapshot might be a step closer to the actual translocating machinery. Nevertheless, because of the use of detergent, the true quartenary state of the translocase might have been disturbed. Hence, even after this and other studies, several issues remain puzzling. New approaches must be combined with current tools to gain insight into the functionally relevant quartenary states of SecA and SecYEG during preprotein translocation.

The Peter Landin prize honours the best paper presented at each year's International Symposium on the Implementation and Application of Functional Languages (IFL). It has been awarded every year since 2003, and covers a range of topics including functional operating systems, static analysis for cost information of functional programs, techniques to improve array processing for data locality and parallelism, explicit parallel coordination, supercompilation, and a rational deconstruction of Landin's SECD machine itself. This article describes the history of the prize, explains why Peter Landin was chosen as nominee, and describes each of the articles that have been awarded the prize to date.

There is a missing piece to America’s education agenda, and children will continue to be left behind until that piece is addressed. Furthermore, children are not being systematically prepared for their complex roles as citizens in our democracy. A growing body of evidence from research and practice suggests reconceptualizing education as an integration of social-emotional and character development (SECD) and academic learning. This article reviews skills children need for effective social and academic participation, characteristics of schools that effectively integrate these forms of learning, and key reasons to adopt this integration. It concludes with examples of, and suggestions for, bringing SECD to prominence in educational policy making.

We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.

The process of compiler generation from lambda-calculus definitions is studied. The compiling schemes developed utilize as their object language the set of state transition machines (STMs): automata-like transition sets using first-order arguments. An intermediate definition form, the STM-interpreter, is treated as central to the formulation of STMs. Three compiling schemes are presented: one derived directly from an STM-interpreter for the lambda-calculus; one formulated from an STM-interpreter variant of Landin's SECD-machine; and one defined through meaning-preserving transformations upon a denotational definition of the lambda-calculus. The results are compared and some tentative conclusions are made regarding the utility of compiler generation with the STM forms.

New software tools for quantitative analysis of mass spectrometric lipidome data have been developed. The LIMSA tool finds and integrates peaks in a mass spectrum, matches the peaks with a user-supplied list of expected lipids, corrects for overlap in their isotopic patterns, and quantifies the identified lipid species according to internal standards. Three different algorithms for isotopic correction (deconvolution) were implemented and compared. LIMSA has a convenient user interface and can be applied on any type of MS spectrum. Typically, analysis of one spectrum takes only a few seconds. The SECD tool, designed for analysis of LC-MS data sets, provides an intuitive and informative display of MS chromatograms as two-dimensional "maps" for visual inspection of the data and allows the user to extract mass spectra, to be further analyzed with LIMSA, from arbitrary regions of these maps. More reliable analysis of complex lipidome data with improved signal-to-noise ratio is obtained when compared to standard time-range averaged spectra. The functionality of these tools is demonstrated by analysis of standard mixtures as well as complex biological samples. The tools described here make accurate, high-throughput analysis of extensive sample sets feasible and are made available to the scientific community free of charge.

The majority of secretory proteins are translocated into and across hydrophobic membranes via the universally conserved Sec pore. Accessory proteins, including the SecDF-YajC Escherichia coli membrane complex, are required for efficient protein secretion. E. coli SecDF-YajC has been proposed to be involved in the membrane cycling of SecA, the cytoplasmic bacterial translocation ATPase, and in the stabilizing of SecG, a subunit of the Sec pore. While there are no identified archaeal homologs of either SecA or SecG, many archaea possess homologs of SecD and SecF. Here, we present the first study that addresses the function of archaeal SecD and SecF homologs. We show that the SecD and SecF components in the model archaeon Haloferax volcanii form a cytoplasmic membrane complex in the native host. Furthermore, as in E. coli , an H. volcanii Δ secFD mutant strain exhibits both severe cold sensitivity and a Sec-specific protein translocation defect. Taken together, these results demonstrate significant functional conservation among the prokaryotic SecD and SecF homologs despite the distinct composition of their translocation machineries.

A remarkable feature of proteins of the SecD and SecF family involved in protein translocation is that they possess a very large first periplasmic domain. Here we report that this large first periplasmic domain is not required for the SecD-SecF interaction but that it is important for catalyzing protein translocation.

We analyse machines that implement the call-by-value reduction strategy of the λ-calculus: two environment machines – CAM and SECD – and two encodings into the $\pi$-calculus – due to Milner and Vasconcelos. To establish the relation between the various machines, we setup a notion of reduction machine and two notions of correspondences: operational – in which a reduction step in the source machine is mimicked by a sequence of steps in the target machine – and convergent – where only reduction to normal form is simulated. We show that there are operational correspondences from the λ-calculus into CAM, and from CAM and from SECD into the $\pi$-calculus. Plotkin completes the picture by showing that there is a convergent correspondence from the λ-calculus into SECD.

The Escherichia coli preprotein translocase is composed of a "preprotein conducting channel" domain that consists of the peripherally bound translocation ATPase SecA and the heterotrimeric SecYEG membrane protein complex. SecD, SecF, and YajC form another heterotrimeric complex that can associate with the SecYEG complex. YidC is an essential membrane protein that plays a role in the integration of newly synthesized membrane proteins, and has been shown to co-purify with SecYEG when all translocase components are overproduced. Here, we demonstrate that under conditions that YidC co-purifies with overproduced SecDFyajC it does not co-purify with overproduced SecYEG. Moreover, this interaction of YidC with the SecDFyajC complex is also found at chromosomal protein levels of SecD, SecF and YajC. Closer examination of the SecDFyajC-YidC complex showed that YidC binds to SecD and SecF, whereas YajC interacts only with SecF. As SecF and YajC have previously been shown to interact with SecY, we propose that these two proteins link the heterotetrameric SecDFyajC-YidC complex to the SecYEG complex.

Vibrio alginolyticus caused great losses to aquaculture. Adhesion is an important virulence factor of V. alginolyticus. In this study, the relationship between V. alginolyticus adhesion and type II secretion system genes (secA, secD, secF, yajC, and yidC) was determined using gene silencing, qRT‐PCR and in vitro adhesion assay. The results showed that the expression of target genes and the bacterial adhesion exhibited significant decreases after transient gene silencing and stable gene silencing, which indicated that secA, secD, secF, yajC, and yidC played roles in the bacterial adhesion of V. alginolyticus. The expression of secA, secD, secF, yajC, and yidC were significantly influenced by temperature, salinity, pH and starvation. The results indicated that the expression of secA, secD, secF, yajC, and yidC were sensitive to different environmental factors, whereas environmental factors can affect V. alginolyticus adhesion via the expression of secA, secD, secF, yajC, and yidC.

We present a new abstract machine, called DCESH, which models the execution of higher-order programs running in distributed architectures. DCESH implements a native general remote higher-order function call across node boundaries. It is a modernised version of SECD enriched with specialised communication features required for implementing the remote procedure call mechanism. The key correctness result is that the termination behaviour of the remote procedure call is indistinguishable (bisimilar) to that of a local call. The correctness proofs and the requisite definitions for DCESH and other related abstract machines are formalised using Agda. We also formalise a generic transactional mechanism for transparently handling failure in DCESHs.We use the DCESH as a target architecture for compiling a conventional call-by-value functional language ("Floskel") which can be annotated with node information. Conventional benchmarks show that the single-node performance of Floskel is comparable to that of OCaml, a semantically similar language, and that distribution overheads are not excessive.

It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between small-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature. We start by distilling the KAM, the CEK, and a sketch of the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. The LSC is a complexity-preserving abstraction of abstract machines. Fil: Accattoli, Beniamino. Universidad de Bologna; Italia. University of Carnegie Mellon; Estados Unidos Fil: Barenbaum, Pablo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Universidad de Buenos Aires; Argentina Fil: Mazza, Damiano. Centre National de la Recherche Scientifique; Francia. Universite de Paris 13-Nord; Francia

One method for producing verified implementations of programming languages is to formally derive them from abstract machines. Tail-recursive abstract machines provide efficient support for iterative processes via the ordinary procedure call mechanism. This document argues that the use of tail-recursive abstract machines incurs only a small increase in theorem-proving burden when compared with what is required when using ordinary abstract machines. The position is supported by comparing correctness proofs performed using the Boyer–Moore theorem prover. A by-product of this effort is a syntactic criterion based on tail contexts for identifying which procedure calls must be implemented as tail calls. The concept of tail contexts was used in the latest Scheme Report, the only language specification known to the author that defines the requirement that its implementations must be tail recursive.

This note introduces Peter Landin‘s 1965 technical report “A Generalization of Jumps and Labels”, which is reprinted in this volume. Its aim is to make that historic paper more accessible to the reader and to help reading it in context. To this end, we explain Landin‘s control operator J in more contemporary terms, and we recall Burge‘s solution to a technical problem in Landin‘s original account.

The effect of the overproduction of SecF encoded by the tac-secF gene on a plasmid on the synthesis of other Sec proteins was studied in Escherichia coli. SecF overproduction resulted in the simultaneous overproduction of SecD encoded by the tac-secD gene on a plasmid. Deletion of the orf6 gene, located downstream of the secF gene, had no effect on SecD overproduction. A pulse-chase experiment revealed that the overproduction was due to stabilization of SecD with SecF. SecF overproduction also resulted in the overproduction of SecY encoded by the tac-secY gene on a plasmid as well. SecF overproduction also enhanced the level of SecY expressed by the chromosomal secY gene. This SecF effect was not due to its effect on SecD or SecE, since SecF overproduction did not affect the levels of SecD and SecE expressed by the chromosomal secD and secE genes, respectively. SecE-dependent overproduction of SecY has already been demonstrated. It is suggested that SecF interacts with both SecD and SecY. SecE-SecY interaction has been demonstrated. It is likely, therefore, that all Sec proteins in the cytoplasmic membrane interact with each other.

Mutations in secD and secF show impaired protein translocation across the inner membrane of Escherichia coli. We investigated the effect of SecD and SecF (SecD/F) depletion on preprotein translocation into inverted inner membrane vesicles (IMVs). Both IMVs and cells which were depleted of SecD/F were defective in their ability to maintain a proton electrochemical gradient. The translocation of pre-maltose binding protein (preMBP), which is strongly delta microH+ dependent, showed a 5-fold decreased rate with IMVs lacking SecD/F. In contrast, proteolytic processing of preMBP to MBP by leader peptidase was similar in IMVs containing and lacking SecD/F, consistent with earlier findings that only ATP-dependent translocation is required for the initiation of translocation. In the absence of a delta microH+, with ATP as the sole energy source, preMBP translocation into IMVs which contained or were depleted of SecD/F was identical. Translocation of the precursor of outer membrane protein A (proOmpA) in the presence of subsaturating ATP also required a generated delta microH+ and, under these conditions, proOmpA translocation required SecD/F. With saturating concentrations of ATP, where delta microH+ has little effect on in vitro proOmpA translocation, SecD/F also had little effect on translocation. These results explain why SecD/F effects are precursor protein dependent in vitro.

The secD operon of Escherichia coli is required for the efficient export of proteins. We have characterized this operon, and found that, in addition to secD and secF, it contains the upstream gene yajC, but not the genes queA or tgt, in contrast to previous reports. An analysis of yajC mutations constructed in vitro and recombined onto the chromosome indicates that yajC is neither essential nor a sec gene. The secD operon is not induced in response to either secretion defects or temperature changes. TnphoA fusions have been used to analyze the topology of SecD in the inner membrane; the protein contains six transmembrane stretches and a large periplasmic domain. TnphoA fusions to SecD and SecF have also been recombined onto the chromosome and used to determine the level of these proteins within the cell. Our results indicate that there are fewer than 30 SecD and SecF molecules per cell.

Modern type systems for programming languages usually incorporate additional information useful for program analysis, e.g., effects, control flow, non-interference, strictness etc. When designing a typing predicate for such systems, a form of logical derivation rules is normally taken. Despite the expressivity of this approach, the straightforward implementation of an appropriate type checker is usually inefficient in terms of stack consumption and further optimisations. This leads to a significant gap between an analysis and program implementing the analysis. In this paper we demonstrate an application of techniques investigated by Danvy et al. to derive an abstract machine for typing from the traditional recursive descent approach. All used techniques are off-the-shelf and no appropriate correspondence theorems between an initial type system and the derived abstract machine needs to be proven: they are instead corollaries of the correctness of inter-derivation and of the initial specification. Whereas a recursive descent is something straightforward to implement based on declarative typing rules, the derived abstract machine exposes behaviour similar to Landin's SECD machine and gives a solid basis for further optimizations using abstract interpretation. ispartof: pages:1-7 ispartof: LDTA '11 Proceedings of the Eleventh Workshop on Language Descriptions, Tools and Applications pages:1-7 ispartof: LDTA location:Saarbrucken, Germany date:26 Mar - 27 Mar 2011 status: published

In this chapter, we present the main properties of functional programming. In functional programming, computation proceeds by rewriting functions and not by modifying the state. The fundamental characteristic of the languages in this paradigm, at least in their “pure” form, is precisely that of not possessing the concept of memory (and therefore side effect). Once an environment is fixed, an expression always denotes the same value. We will discuss the pure paradigm in the first sections, explaining the fundamental aspects. Functional programming languages, however, merge these “pure” ingredients in a context that adds many other mechanisms; we will review them before touching upon the SECD machine, an abstract machine for higher-order functional languages which constitutes the prototype of many real implementations. We will, at this point, be in a position to discuss the reasons why the functional programming paradigm is interesting with respect to ordinary imperative languages. The chapter concludes with a more theoretical section which provides a succinct introduction to the lambda-calculus, a formal system for computability which inspires all functional languages and which has been a constant model for the design of programming languages.

An abstract machine is designed to support the data environment requirements of BaLinda Lisp, a parallel Lisp dialect which permits speculative processing of conditional modules. Logically, the machine provides multiple stacks connected into an environment tree, with lexically visible sections pointed to by display registers. Physically, stack sections are stored as separate objects and access is established by the use of a dynamic stack recording the chain of function calls, and a set of lexical display registers pointing at visible objects. This arrangement allows parts of the environment of a function to be retained or garbage-collected as appropriate after exit. By making copies of visible ancestral stack sections, side effects of speculative parallel tasks are handled in accordance with language semantics. The architecture is generic and may be realized in a variety of forms, depending on whether BaLinda Lisp is implemented on a conventional machine, stack machine, or dataflow machine.

SecD and SecF proteins were overproduced by means of recombinant DNA technology. Immunoblot and amino-acid sequencing analysis revealed that the overproduced proteins are SecD and SecF. The SecD- or SecF-overproduced membrane fraction was subjected to differential solubilization. The SecD protein was then purified through ion-exchange and size-exclusion chromatographies. The SecF protein was purified through size exclusion chromatography. Proteoliposomes reconstituted from the purified SecD and SecF together with SecE and SecY were used to analyze the translocation activity. SecD and SecF did not exhibit significant effects on the translocation activity of proteoliposomes. The amounts of SecD and SecF in overproducers were determined densitometrically on a stained SDS gel and their overproduction (fold) was determined by means of immunoblot analysis. Then the number of these molecules in one normal cell were estimated. From these numbers, together with those of other Sec proteins, the number of the translocation machinery existing in one Escherichia coli cell was inferred to be around 500.

This technical paper provides an overview of Rome Laboratory's Research & Development Program in the area of System Engineering. In particular, it describes the objectives of an exploratory development effort entitled “System Engineering Concept Demonstration” (SECD), the activities that were pursued under the effort, and its results. It serves as an introduction to other papers [Comer 1992], [Ortiz 1992], and [Pariseau & Stuebing 1992], which provide further detail on the technology and demonstrations that resulted. Rome Laboratory's future plans to develop Systems Engineering technology are also identified.

A concurrent functional language is presented, Parlam, which includes primitives for explicit control of parallel reductions. An abstract machine for Parlam (ParSEC) is derived from Landin's SECD machine by extending it for dealing with parallel computation. Several issues and problems about its implementation on a massively parallel computer are discussed and a specific implementative model for ParSEC under the Connection Machine is described.

We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.

This paper describes a new implementation technique calledpreliminary arrangements of arguments for lazy functional languages. Unlike conventional lazy evaluators, the evaluator with preliminary arrangements partly processes every argument before calling functions. It works in a lazy way with less memory cells than conventional methods. The practical importance of this technique is demonstrated by some benchmark results.

We present a nondeterministic calculus of closures for the evaluation of λ-calculus, which is based, not on symbolic evaluation (β-reduction), but on the paradigm of environments and closures, as in the old SECD machine, or in the more recent Categorical Abstract Machine (CAM). This calculus stands as a suitable abstraction right above those devices: there is no commitment as to the order of evaluation, and no explicit handling of stacks: the calculus is expressed in the style of Structural Operational Semantics, by a set of conditional rewrite rules. The CAM, and a very simple lazy abstract machine, due to J.-L. Krivine, arise naturally by first restricting the calculus to a specific strategy, and then implementing recursive calls by a stack. The Church–Rosser property and termination in presence of types hold in the calculus of closures, and are easier to establish than in the λ-calculus. The calculus of closures has served as a starting point to a more powerful general calculus of substitutions at which we hint shortly, insisting on its category- theoretic significance.

XQuery is a XML query language proposed by W3C and a good many researches are involved for the implementation of XQuery. While many implementations adopt interpret solutions, XQC is a compiler for XQuery 1.0 which can compile XQuery program to the low level binary code - Java bytecode, and provides opportunities for performance improving. XQC has a well-designed architecture which makes various optimization strategies can be introduced into different compilation phases, and consequently, the compiled bytecode turns out to be efficient during execution, especially during repetitive execution. This paper presents XQC solution through an overview of the architecture which is composed of 4 core modules: preprocessor, FXQL code generator, SECD code generator, and bytecode generator, also it covers the tradeoffs in the core modules in detail and the performance of XQC by experiment.

Landin's J operator was the first control operator for functional languages. It was specified with an extension of the SECD machine, which was the first abstract machine for functional languages. We present a family of compositional evaluation functions corresponding to this extension of the SECD machine, using a series of elementary transformations (transformation into continuation-passing style (CPS) and defunctionalization, chiefly) and their left inverses (transformation into direct style and refunctionalization). To this end, we modernize the SECD machine into a bisimilar one that operates in lock step with the original one but that (1) does not use a data stack and (2) uses the caller-save rather than the callee-save convention for environments. We then characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. As a byproduct, we also present a reduction semantics for applicative expressions with the J operator, based on Curien's original calculus of explicit substitutions. This reduction semantics mechanically corresponds to the modernized version of the SECD machine and to the best of our knowledge, it provides the first syntactic theory of applicative expressions with the J operator. The present work is concluded by a motivated wish to see Landin's name added to the list of co-discoverers of continuations. Methodologically, however, it mainly illustrates the value of Reynolds's defunctionalization and of refunctionalization as well as the expressive power of the CPS hierarchy (a) to account for the first control operator and the first abstract machine for functional languages and (b) to connect them to their successors.

Landin's J operator was the first control operator for functional languages, and was specified with an extension of the SECD machine. Through a series of meaning-preserving transformations (transformation into continuation-passing style (CPS) and defunctionalization) and their left inverses (transformation into direct style and refunctionalization), we present a compositional evaluation function corresponding to this extension of the SECD machine. We then characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. Finally, we present a motivated wish to see Landin's name added to the list of co-discoverers of continuations.

We describe the architecture of a virtual machine for executing functional logic programming languages. A distinguishing feature of our machine is that it preserves the operational completeness of non-deterministic programs by concurrently executing a pool of independent computations. Each computation executes only root-needed sequential narrowing steps. We describe the machine's architecture and instruction set, and show how to compile overlapping inductively sequential programs to sequences of machine instructions. The machine has been implemented in Java and in Standard ML.

Landin's SECD machine was the first abstract machine for the λ-calculus viewed as a programming language. Both theoretically as a model of computation and practically as an idealized implementation, it has set the tone for the subsequent development of abstract machines for functional programming languages. However, and even though variants of the SECD machine have been presented, derived, and invented, the precise rationale for its architecture and modus operandi has remained elusive. In this article, we deconstruct the SECD machine into a λ-interpreter, i.e., an evaluation function, and we reconstruct λ-interpreters into a variety of SECD-like machines. The deconstruction and reconstructions are transformational: they are based on equational reasoning and on a combination of simple program transformations—mainly closure conversion, transformation into continuation-passing style, and defunctionalization. The evaluation function underlying the SECD machine provides a precise rationale for its architecture: it is an environment-based eval-apply evaluator with a callee-save strategy for the environment, a data stack of intermediate results, and a control delimiter. Each of the components of the SECD machine (stack, environment, control, and dump) is therefore rationalized and so are its transitions. The deconstruction and reconstruction method also applies to other abstract machines and other evaluation functions.

Machine functions have been introduced by Earley and Sturgis in [6] in order to provide a mathematical foundation of the use of the T-diagrams proposed by Bratman in [5]. Machine functions describe the operation of a machine at a very abstract level. A theory of hardware and software based on machine functions may be called a machine function theory, or alternatively when focusing on inputs and outputs for machine functions a control code algebra (CCA). In this paper we develop some control code algebras from first principles. Machine function types are designed specifically for various application such as program compilation, assembly, interpretation, managed interpretation and just-in-time compilation. Machine function dependent CCA’s are used to formalize the well-known compiler fixed point, the managed execution of JIT compiled text and the concept of a verifying compiler.

The Sec machinery is one mechanism used by bacteria to translocate proteins across their cytoplasmic membrane. Most of the Sec components have been identified within the important gastric pathogen, Helicobacter pylori, however their functionality has not yet been demonstrated. Here we report the existence of putative homologues to the Sec components yajC (HP1450) and yidC (HP1551), and demonstrate the ability of the H. pylori secD (HP1550) and secG (HP1255) homologues to facilitate inner membrane translocation of the maltose-binding protein MalE, by complementation of the respective secretion-deficient Escherichia coli mutants, thus providing evidence of their functionality.

We show how to derive a compiler and a virtual machine from a compositional interpreter. We first illustrate the derivation with two evaluation functions and two normalization functions. We obtain Krivine's machine, Felleisen et al.'s CEK machine, and a generalization of these machines performing strong normalization, which is new. We observe that several existing compilers and virtual machines--e.g., the Categorical Abstract Machine (CAM), Schmidt's VEC machine, and Leroy's Zinc abstract machine--are already in derived form and we present the corresponding interpreter for the CAM and the VEC machine. We also consider Hannan and Miller's CLS machine and Landin's SECD machine. We derived Krivine's machine via a call-by-name CPS transformation and the CEK machine via a call-by-value CPS transformation. These two derivations hold both for an evaluation function and for a normalization function. They provide a non-trivial illustration of Reynolds's warning about the evaluation order of a meta-language.

We bridge the gap between functional evaluators and abstract machines for the lambda-calculus, using closure conversion, transformation into continuation-passing style, and defunctionalization of continuations. We illustrate this bridge by deriving Krivine's abstract machine from an ordinary call-by-name evaluator and by deriving an ordinary call-by-value evaluator from Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in the literature. The second one is new. Together, they show that Krivine's abstract machine and the CEK machine correspond to the call-by-name and call-by-value facets of an ordinary evaluator for the lambda-calculus. We then reveal the denotational content of Hannan and Miller's CLS machine and of Landin's SECD machine. We formally compare the corresponding evaluators and we illustrate some relative degrees of freedom in the design spaces of evaluators and of abstract machines for the lambda-calculus with computational effects. For the purpose of this work, we distinguish between virtual machines, which have an instruction set, and abstract machines, which do not. The Categorical Abstract Machine, for example, has an instruction set, but Krivine's machine, the CEK machine, the CLS machine, and the SECD machine do not; they directly operate on lambda-terms instead. We present the abstract machine that corresponds to the Categorical Abstract Machine.

CASE is an abstract machine which supports applicative programming and is a variation of Landin's classical SECD machine (P.J. Landin, 1964). Its environment is organized in a novel way which makes variable access more efficient by removing the overhead of following a static chain or of setting up a display as in more conventional stack architectures. The CASE machine also has features allowing the execution of code to reflect lazy evaluation semantics. A description is given of the architecture of the machine, its operational semantics and code generated by a typical compiler for some sample programs. Also discussed are some optimizations made to facilitate efficient code generation on real hardware and some measurements of the efficiency of the machine. >

We have designed a functional data-parallel language called BSML for programming bulk-synchronous parallel (BSP) algorithms. The execution time can be estimated and dead-locks and indeterminism are avoided. The BSMLlib library has been implemented for the Objective Caml language. But there is currently no full implementation of such a language and an abstract machine is needed to validate such an implementation. Our approach is based on a bytecode compilation to a parallel abstract machine performing exchange of data and synchronous requests derived from the ZAM, the efficient abstract machine of the Objective Caml language.

Introduction Historical Outline Protein Targeting to the Translocase Signal Peptides Co-translational Protein Targeting Post-translational Protein Targeting Converging Targeting Pathways Translocase: A Multisubunit Integral Membrane Protein Complex SecA SecY SecE SecG SecD, SecF, and YajC Conserved Protein Translocases in Bacteria, Eukaryotes, and Archaea Role of Lipids in Protein Translocation Mechanism of Protein Translocation ATP-driven Translocation Proton Motive Force-driven Translocation Dynamics of the Protein-conducting Channel Regulation of Protein Translocation Outlook and Perspectives Acknowledgments Keywords: translocation; membranes; SecA; SecY; SecE; SecB; SecD; SecF; SRP

We present a simple inter-derivation between lambda-interpreters, i.e., evaluation functions for lambda-terms, and abstract reduction machines for the lambda-calculus, i.e., transition functions. The two key derivation steps are the CPS transformation and Reynolds's defunctionalization. By transforming the interpreter into continuation-passing style (CPS), its flow of control is made manifest as a continuation. By defunctionalizing this continuation, the flow of control is materialized as a first-order data structure. The derivation applies not merely to connect independently known lambda-interpreters and abstract machines, it also applies to construct the abstract machine corresponding to a lambda-interpreter and to construct the lambda-interpreter corresponding to an abstract machine. In this article, we treat in detail the canonical example of Landin's SECD machine and we reveal its denotational content: the meaning of an expression is a partial endo-function from a stack of intermediate results and an environment to a new stack of intermediate results and an environment. The corresponding lambda-interpreter is unconventional because (1) it uses a control delimiter to evaluate the body of each lambda-abstraction and (2) it assumes the environment to be managed in a callee-save fashion instead of in the usual caller-save fashion.

The general secretion (Sec) pathway plays a prominent role in bacterial protein export, and the accessory component SecDF has been shown to improve transportation efficiency. Inspection of Streptomyces coelicolor genome reveals the unexpected presence of two different forms of secDF homologous genes: one in fused form (secDF) and the other in separated form (secD and secF). However, the functional role of two SecDF homologs in S. coelicolor has not yet been determined. Transcriptional analysis of secDF homologs reveals that these genes are constitutively expressed. However, the transcript levels of secD and secF are much higher than that of secDF in S. coelicolor. Deletion of secDF or/and secD/secF in S. coelicolor did result in reduced secretion efficiency of Xylanase A and Amylase C, suggesting that they may have redundant functions for Sec-dependent translocation pathway. Moreover, our results also indicate that SecD/SecF plays a more prominent role than SecDF in protein translocation. Evolutionary analysis suggests that the fused and separated SecDF homologs in Streptomyces may have disparate evolutionary ancestries. SecD/SecF may be originated from vertical transmission of existing components from ancestor of Streptomyces species. However, SecDF may be derived from bacterial ancestors through horizontal gene transfer. Alternately, it is also plausible that SecDF may have arisen through additional gene duplication and fusion events. The acquisition of a second copy may confer a selective benefit to Streptomyces by enhancing protein transport capacity. Taken together, our results provide new insights into the potential biological function and evolutionary aspects of the prokaryotic SecDF complex.

In light of the usual definition of values [18] as terms in weak head normal form (WHNF), a λ-abstraction is regarded as a value, and therefore no expressions under λ-abstraction can get evaluated and the sharing of computation under λ has to be achieved through program transformations such as λ-lifting and supercombinators. In this paper we generalise the notion of head normal form (HNF) and introduce the definition of generalised head normal form (GHNF). We then define values as terms in GHNF with flexible heads, and study a call-by-value λ-calculus λ hd v corresponding to this new notion of values. After establishing a version of the normalisation theorem in λ hd v , we construct an evaluation function evalhd for λ hd v which evaluates under λ-abstraction. We prove that a program can be evaluated in λ hd v to a term in GHNF if and only if it can be evaluated in the usual λ-calculus to a term in HNF. We also present an operational semantics for λ hd v via a SECD machine. We argue that lazy functional programming languages can be implemented through λ hd v and an implementation of λ hd v can significantly enhance the degree of sharing in evaluation. This establishes a solid foundation for implementing run-time code generation through λ hd v

Students usually find formal methods of describing programming languages very difficult because of the cryptic notation, the complexity of the techniques, and the size of the specifications. The SECD abstract machine provides a small but clear description of the operational semantics of the lambda calculus. By implementing the SECD machine in Prolog, we give students a tool for testing specifications and for experimenting with alternate language semantics in an interactive setting.