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.

(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).

Staphylococcus aureus causes many infections and its drug resistance is a worrying challenge for medical care. The SecD subunit of Sec secretion system in methicillin‐resistant S. aureus is an attractive target because SecD dysfunction leads to the death of bacteria and SecD as a target is more efficient than SecA and SecF. Evolution could have made SecD to become insensitive to antibacterial agents although the drugs directly against SecD have yet to develop. So far, no detailed information on SecD evolution has been available, thus 2686 SecD sequences with full taxonomic information from kingdom to species were analyzed. First, the variance of pairwise p‐distance was evaluated for each taxonomic group. Second, the variance was further partitioned into intergroup and intragroup variances for quantification of horizontal and vertical gene transfer. Third, phylogenetic tree was built to trace the evolutionary pathway. The results showed that overall evolution of SecDs appears to have undergone horizontal and vertical gene transfer. Only 0.5% horizontal transfers were found between any two SecDs in S. aureus, 6.8% and 8.8% horizontal transfers were found between any two Staphylococcus SecDs from different and the same species, and only one SecD from S. aureus was located far away from its sister cluster. Thus, statistic and evolutionary analyses demonstrate that the SecDs from staphylococcus species have a small chance of mutating, and provide taxonomic evidence to use the SecD as a potential target for new generation of antibacterial agents against S. aureus.

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 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.

The activation of human epidermal growth factor receptor (hEGFR) involves a large conformational change in its soluble extracellular domains (sECD, residues 1-620), from a tethered to an extended conformation upon binding of ligands, such as EGF. It has been reported that this dynamic process is pH-dependent, that is, hEGFR can be activated by EGF at high pH to form an extended dimer but remains as an inactive monomer at low pH. In this paper, we perform all-atom molecular dynamics (MD) simulations starting from the tethered conformation of sECD:EGF complex, at pH 5.0 and 8.5, respectively. Simulation results indicate that sECD:EGF shows different dynamic properties between the two pHs, and the complex may have a higher tendency of activation at pH 8.5. Twenty residues, including 13 histidines, in sECD:EGF have different protonation states between the two pHs (calculated by the H++ server). The charge distribution at pH 8.5 is more favorable for forming an extended conformation toward the active state of sECD than that at pH 5.0. Our study may shed light on the mechanism of pH dependence of hEGFR activation. Graphical abstract pH dependence of ligand-induced human epidermal growth factor receptor activation.

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.

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.

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

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 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.

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.

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.

Landin's SECD machine was the first abstract machine for the lambda-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 lambda-interpreter, i.e., an evaluation function, and we reconstruct lambda-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. It makes it possible to systematically extract the denotational content of an abstract machine in the form of a compositional evaluation function, and the (small-step) operational content of an evaluation function in the form of an abstract machine.

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.

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.

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.

We show here that the rate of protein translocation in the bacterium Escherichia coli depends on the levels of the SecD and SecF proteins in the cell. Overexpression of SecD and SecF stimulates translocation in wild type cells and improves export of proteins with mutant signal sequences. Depletion of SecD and SecF from the cell greatly reduces but does not abolish protein translocation. A secDF::kan null mutant deleted for the genes encoding both proteins is cold-sensitive for growth and protein export, has a severe export defect at 37 degrees C and is barely viable. The phenotypes of a secD null mutant and a secF null mutant are identical to the secDF::kan double null mutant. These results partially resolve the conflict between genetic studies and results from in vitro translocation systems which do not require SecD and SecF for activity, affirm the importance of these proteins to the export process, and suggest that SecD and SecF function together to stimulate protein export in a role fundamentally different from other Sec proteins. Our results provide additional support for the notion that an early step in protein export is cold-sensitive.

Summary Genetic approaches can address the question of how integral membrane Sec factors interact with each other and facilitate protein translocation across the cytoplasmic membrane of E. coli. This review summarizes genetic analyses of SecY, SecE and some other protein translocation factors, utilizing ‘prl’ mutations,‘sec’ mutations, ‘suppressor-directed inactivation’, ‘Sec titration’, dominant negative mutations and their suppressors. Evidence suggests that coordinate participation of SecY, SecE, SecD, SecF, and probably some other factors, is crucial for the process.

Abstract #3146 Background: Although serum extracellular domain (sECD) HER2 levels can be easily measured by enzyme immunoassays, the potential clinical utility of HER2 extracellular domain protein shed in the serum is not established. High serum protein levels may be indicative of metastatic disease to the liver or perhaps greater tumor burden. EGF30008 is a double-blind, placebo-controlled phase III trial evaluating the effect of letrozole with/without lapatinib in previously untreated postmenopausal women with hormone receptor-positive metastatic breast cancer. Levels of sECD HER2 were collected on all 1,286 women at baseline and every 4 weeks on study including at disease progression. Methods: Baseline serum levels and tumor characteristics were collated in blinded fashion for all 1,286 patients in the trial (data cut off 12May08). Patients with baseline serum protein levels ≥ 15 ng/mL were defined as sECD HER2+. Correlations were assessed between baseline serum protein levels and baseline liver disease and bone-only disease and total tumor burden (as defined by number of metastatic sites). Chi-square test was applied to assess the correlation between serum protein levels and liver disease or bone-only disease. Wilcoxon rank-sum test using normal approximation was used to compare total tumor burden and baseline protein levels. Results: Among sECD HER2+ patients, 42% had at least one liver metastasis, whereas 20% of sECD HER2-negative patients had at least one liver metastasis (P < 0.0001). No correlation exists between baseline serum protein level and bone-only disease (P = 0.64). Patients who were sECD HER2+ had a greater total tumor burden (mean metastatic sites = 5.4; standard deviation = 3.2; median = 5) compared with patients who were sECD HER2-negative (mean metastatic sites = 4.4; standard deviation = 3.1; and median = 4; P < 0.0001). Conclusion: High baseline sECD HER2 strongly correlates with tumor burden. There was also a significant correlation between sECD and liver metastases, but no correlation at all with bone-only disease. These analyses will be repeated after the database is finalized and unblinded. Our analysis is limited to detection of the number of metastatic sites and is not sensitive to the individual sizes of metastases. In addition, another potential explanation for the low sensitivity of HER2 detection by sECD is that small metastatic deposits that are HER2+ in situ do not shed enough sECD into the serum to be detected by the assay. Conversely, some very large HER2-negative tumors do in fact shed measurable sECD if the tumor bulk is very high, even though in situ they may be nonamplified. A future analysis will take the sum of the longest diameters of all known lesions and compare it to sECD HER2 levels. Citation Information: Cancer Res 2009;69(2 Suppl):Abstract nr 3146.

The operational semantics of functional programming languages is frequently presented using inference rules within simple meta-logics. Such presentations of semantics can be high-level and perspicuous since meta-logics often handle numerous syntactic details in a declarative fashion. This is particularly true of the meta-logic we consider here, which includes simply typed l-terms, quantification at higher types, and b-conversion. Evaluation of functional programming languages is also often presented using low-level descriptions based on abstract machines: simple term rewriting systems in which few high-level features are present. In this paper, we illustrate how a high-level description of evaluation using inference rules can be systematically transformed into a low-level abstract machine by removing dependencies on high-level features of the meta-logic until the resulting inference rules are so simple that they can be immediately identified as specifying an abstract machine. In particular, we present in detail the transformation of two inference rules specifying call-by-name evaluation of the untyped l-calculus into the Krivine machine, a stack-based abstract machine that implements such evaluation. The initial specification uses the meta-logic's b-conversion to perform substitutions. The resulting machine uses de Bruijn numerals and closures instead of formal substitution. We also comment on a similar construction of a simplified SECD machine implementing call-by-value evaluation. This approach to abstract machine construction provides a semantics-directed method for motivating, proving correct, and extending such abstract machines.

Cold-sensitive mutations in the secD locus of Escherichia coli result in severe defects in protein export at the non-permissive temperature of 23 degrees C. DNA sequence of a cloned fragment that includes the secD locus reveals open reading frames for seven polypeptide chains. Both deletions and TnphoA insertions in this clone have been used in maxicell and complementation studies to define the secD locus and its products. The secD mutations fall into two complementation groups, defining genes we have named secD and secF. These two genes comprise an operon, the first case of two genes involved in the export process being co-transcribed. The DNA sequence of the two genes along with alkaline phosphatase fusion analysis indicates that they code for integral proteins of the cytoplasmic membrane. We suggest that these two proteins may form a complex in the membrane which acts at late steps in the export process.

This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.

New mutants of Escherichia coli altered in protein export were identified in phoA-lacZ and lamB-lacZ gene fusion strains by searching for mutants that showed an altered lactose phenotype. Several mutations mapped in a new gene, secD. These mutants were, in general, cold sensitive for growth, and the mutations led to an accumulation of precursor of exported proteins. The secD gene is closely linked to tsx on the E. coli chromosome, but separable from another gene proposed to be involved in export, ssaD, which maps nearby. A plasmid carrying secD+ was identified and used to show that the mutations are recessive. The secD gene may code for a component of the cellular export machinery.

The design of an abstract machine with a recursive function programming language which avoids the predicate type of conditional is described. It is shown that trough the adoption of list processing techniques it has been possible to construct a simple simulator for the machine in FORTRAN. A program for the machine which causes it to perform symbolic differentiation with some algebraic manipulation of the expressions concerned is given as an example of the type of computations which may be performed.

The Cartesian closed categories have been shown by several authors to provide the right framework of the model theory of λ-calculus. The second author developed this as a syntactic equivalence between two calculi, giving rise to a new kind of combinatory logic: the categorical combinatory logic, where computations can be done through simple rewrite rules, and, as usual with combinators, avoiding problems with variable name clashes. This paper goes further (though not requiring a previous knowledge of categorical combinatory logic) and describes a very simple machine where categorical terms can be considered as code acting on a graph of values (the essential actions are LISP's “cons” and “cdr”, as well as “rplacd” to implement recursion). The only saving mechanism is a stack containing pointers on code or on the graph. Abstractions are handled in the very same way as in P. Landin's SECD machine, using closures. The machine is called categorical abstract machine or CAM. The CAM is easier to grasp and prove than the SECD machine. The paper discusses the implementation of a real functional programming language, ML, through the CAM. A basic acquintance with λ-calculus is required.