From natural semantics to C: A formal derivation of two STG machines

2009 ◽  
Vol 19 (1) ◽  
pp. 47-94 ◽  
Author(s):  
ALBERTO DE LA ENCINA ◽  
RICARDO PEÑA
Keyword(s):  
Functional Programming ◽  
Functional Language ◽  
Levels Of Abstraction ◽  
Additional Information ◽  
Formal Derivation ◽  
Derivation Step ◽  
Starting Point ◽  
Efficient Code ◽  
Lazy Semantics ◽  
High Level

AbstractThe Spineless Tag-less G-machine (STG machine) was defined as the target abstract machine for compiling the lazy functional language Haskell. It is at the heart of the Glasgow Haskell Compiler (GHC) which is claimed to be the Haskell compiler that generates the most efficient code. A high-level description of the STG machine can be found in Peyton Jones (In Journal of Functional programming, 2(2), 127–202, 1992), Marlow & Peyton Jones (In Sigplan Not., 39(9), 4–5, 2004), and Marlow & Peyton Jones (In Journal of Functional Programming, 16(4–5), 415–449, 2006). Should the reader be interested in a more detailed view, then the only additional information available is the Haskell code of GHC and the C code of its runtime system.It is hard to prove that this machine correctly implements the lazy semantics of Haskell. Part of the problem lies in the fact that the STG machine executes a bare-bones functional language, called STGL, much lower level than Haskell. Therefore, part of the correctness should be—and it is—established by showing that the translation from Haskell to STGL preserves Haskell's semantics.The other part involves showing that the STG machine correctly implements the lazy semantics of STGL. In this paper we provide a step-by-step formal derivation of the STG machine and of its compilation to C, starting from a natural semantics of STGL. Thus, our starting point is higher level than the descriptions found Peyton Jones (In Journal of Functional programming, 2(2), 127–202, 1992) and Marlow & Peyton Jones (In Sigplan Not., 39(9), 4–5, 2004), and our arrival point is lower level than those works. Additionally, there has been substantial changes between the so-called push/enter model of the STG machine described in Peyton Jones (In Journal of Functional programming, 2(2), 127–202, 1992), and the eval/apply model of the STG machine described in Marlow & Peyton Jones (In Sigplan Not., 39(9), 4–5, 2004). So, in fact, we derive two machines instead of one, starting from the same initial semantics.At each step we provide enough intuitions and explanations in order to understand the refinement, and then the formal definitions and statements proving that the derivation step is sound and complete. The main contribution of the paper is to show that an efficient machine such as the STG can be presented, understood, and formally reasoned about at different levels of abstraction.

Hybrid-Data Approach for Estimating Trip Purposes

2021 ◽  
pp. 036119812110184
Author(s):  
Xiaoling Luo ◽  
Adrian Cottam ◽  
Yao-Jan Wu ◽  
Yangsheng Jiang
Keyword(s):  
Transportation Systems ◽  
Data Driven ◽  
Trip Purpose ◽  
Additional Information ◽  
Point Of Interest ◽  
Average Accuracy ◽  
Hybrid Data ◽  
Added Benefit ◽  
Data Source ◽  
High Level

Trip purpose information plays a significant role in transportation systems. Existing trip purpose information is traditionally collected through human observation. This manual process requires many personnel and a large amount of resources. Because of this high cost, automated trip purpose estimation is more attractive from a data-driven perspective, as it could improve the efficiency of processes and save time. Therefore, a hybrid-data approach using taxi operations data and point-of-interest (POI) data to estimate trip purposes was developed in this research. POI data, an emerging data source, was incorporated because it provides a wealth of additional information for trip purpose estimation. POI data, an open dataset, has the added benefit of being readily accessible from online platforms. Several techniques were developed and compared to incorporate this POI data into the hybrid-data approach to achieve a high level of accuracy. To evaluate the performance of the approach, data from Chengdu, China, were used. The results show that the incorporation of POI information increases the average accuracy of trip purpose estimation by 28% compared with trip purpose estimation not using the POI data. These results indicate that the additional trip attributes provided by POI data can increase the accuracy of trip purpose estimation.

scholarly journals Establishing a consensus for the hallmarks of cancer based on gene ontology and pathway annotations

2021 ◽  
Vol 22 (1) ◽  
Author(s):  
Yi Chen ◽  
Fons. J. Verbeek ◽  
Katherine Wolstencroft
Keyword(s):  
Gene Ontology ◽  
Enrichment Analysis ◽  
Biological Data ◽  
Hallmarks Of Cancer ◽  
High Throughput Analysis ◽  
Knowledge Resources ◽  
Gene Set ◽  
Cancer Hallmarks ◽  
Starting Point ◽  
High Level

Abstract Background The hallmarks of cancer provide a highly cited and well-used conceptual framework for describing the processes involved in cancer cell development and tumourigenesis. However, methods for translating these high-level concepts into data-level associations between hallmarks and genes (for high throughput analysis), vary widely between studies. The examination of different strategies to associate and map cancer hallmarks reveals significant differences, but also consensus. Results Here we present the results of a comparative analysis of cancer hallmark mapping strategies, based on Gene Ontology and biological pathway annotation, from different studies. By analysing the semantic similarity between annotations, and the resulting gene set overlap, we identify emerging consensus knowledge. In addition, we analyse the differences between hallmark and gene set associations using Weighted Gene Co-expression Network Analysis and enrichment analysis. Conclusions Reaching a community-wide consensus on how to identify cancer hallmark activity from research data would enable more systematic data integration and comparison between studies. These results highlight the current state of the consensus and offer a starting point for further convergence. In addition, we show how a lack of consensus can lead to large differences in the biological interpretation of downstream analyses and discuss the challenges of annotating changing and accumulating biological data, using intermediate knowledge resources that are also changing over time.

scholarly journals Model-Driven Architectural Framework towards Safe and Secure Nuclear Power Reactors

Sensors ◽  
2021 ◽  
Vol 21 (15) ◽  
pp. 5136
Author(s):  
Bassem Ouni ◽  
Christophe Aussagues ◽  
Saadia Dhouib ◽  
Chokri Mraidha
Keyword(s):  
Nuclear Power ◽  
Nuclear Reactors ◽  
System Development ◽  
Levels Of Abstraction ◽  
Model Driven ◽  
Case System ◽  
Architectural Framework ◽  
Performance Check ◽  
High Level ◽  
Different Levels

Sensor-based digital systems for Instrumentation and Control (I&C) of nuclear reactors are quite complex in terms of architecture and functionalities. A high-level framework is highly required to pre-evaluate the system’s performance, check the consistency between different levels of abstraction and address the concerns of various stakeholders. In this work, we integrate the development process of I&C systems and the involvement of stakeholders within a model-driven methodology. The proposed approach introduces a new architectural framework that defines various concepts, allowing system implementations and encompassing different development phases, all actors, and system concerns. In addition, we define a new I&C Modeling Language (ICML) and a set of methodological rules needed to build different architectural framework views. To illustrate this methodology, we extend the specific use of an open-source system engineering tool, named Eclipse Papyrus, to carry out many automation and verification steps at different levels of abstraction. The architectural framework modeling capabilities will be validated using a realistic use case system for the protection of nuclear reactors. The proposed framework is able to reduce the overall system development cost by improving links between different specification tasks and providing a high abstraction level of system components.

scholarly journals Evidence for Inhibition of Topoisomerase 1A by Gold(III) Macrocycles and Chelates TargetingMycobacterium tuberculosisandMycobacterium abscessus

2018 ◽  
Vol 62 (5) ◽  
Author(s):  
Rashmi Gupta ◽  
Carolina Rodrigues Felix ◽  
Matthew P. Akerman ◽  
Kate J. Akerman ◽  
Cathryn A. Slabber ◽  
...  
Keyword(s):  
Mycobacterium Abscessus ◽  
Cross Resistance ◽  
Human Pathogens ◽  
Intrinsic Resistance ◽  
Content Type ◽  
Starting Point ◽  
Scalable Synthesis ◽  
High Level ◽  
Novel Drug

ABSTRACTMycobacterium tuberculosisand the fast-growing speciesMycobacterium abscessusare two important human pathogens causing persistent pulmonary infections that are difficult to cure and require long treatment times. The emergence of drug-resistantM. tuberculosisstrains and the high level of intrinsic resistance ofM. abscessuscall for novel drug scaffolds that effectively target both pathogens. In this study, we evaluated the activity of bis(pyrrolide-imine) gold(III) macrocycles and chelates, originally designed as DNA intercalators capable of targeting human topoisomerase types I and II (Topo1 and Topo2), againstM. abscessusandM. tuberculosis. We identified a total of 5 noncytotoxic compounds active against both mycobacterial pathogens under replicatingin vitroconditions. We chose one of these hits, compound 14, for detailed analysis due to its potent bactericidal mode of inhibition and scalable synthesis. The clinical relevance of this compound was demonstrated by its ability to inhibit a panel of diverseM. tuberculosisandM. abscessusclinical isolates. Prompted by previous data suggesting that compound 14 may target topoisomerase/gyrase enzymes, we demonstrated that it lacked cross-resistance with fluoroquinolones, which target theM. tuberculosisgyrase.In vitroenzyme assays confirmed the potent activity of compound 14 against bacterial topoisomerase 1A (Topo1) enzymes but not gyrase. Novel scaffolds like compound 14 with potent, selective bactericidal activity againstM. tuberculosisandM. abscessusthat act on validated but underexploited targets like Topo1 represent a promising starting point for the development of novel therapeutics for infections by pathogenic mycobacteria.

scholarly journals Den glatte musikken og muligheten for en erfaring

2020 ◽  
pp. 79-94
Author(s):  
Bendik Fredriksen
Keyword(s):  
Work Of Art ◽  
Negative Term ◽  
Starting Point ◽  
Physical Objects ◽  
High Level

A word often used to describe music is “smooth”. It is mostly meant as a negative term, used to label music as commercial, light, superficial and easily forgotten. However, smooth music is also well-made, with a high level of professionality. In this chapter I take as a starting point the criticism of beauty as smoothness found in Byung-Chul Han’s book Die Errettung des Schönen [Saving beauty], and investigate how this criticism applies to music. Furthermore, I try to define what makes music smooth. While smoothness can easily be defined when speaking about physical objects, music is evasive. Hence, smoothness is defined metaphorically, and according to what it is not, e.g. a work of art, or something that can lead to an experience, a concept I discuss in light of Gadamer, Heidegger, Adorno and Vetlesen. I claim that due to the elusive character of music almost any music can lead to an experience, but it is not a product of the subject’s efforts alone. Moreover, smoothness as a characteristic of music seems to have a liminal quality to it, as it cannot be defined in light of its opposite, but is trapped in its own perfection.

VoDKA: Developing a Video-on-Demand Server using Distributed Functional Programming

2005 ◽  
Vol 15 (3) ◽  
pp. 403-430 ◽  
Author(s):  
VICTOR M. GULIAS ◽  
MIGUEL BARREIRO ◽  
JOSE L. FREIRE
Keyword(s):  
Real World ◽  
Functional Programming ◽  
Building Blocks ◽  
Video On Demand ◽  
Functional Language ◽  
Control Software ◽  
On Demand ◽  
System Requirements ◽  
Cable Company ◽  
Process Composition

In this paper, we present some experience of using the concurrent functional language Erlang to implement a distributed video-on-demand server. For performance reasons, the server is deployed in a cheap cluster made from off-the-shelf components. The demanding system requirements, in addition to the complex and ever-changing domain, suggested a highly flexible and scalable architecture as well as a quite sophisticated control software. Functional programming played a key role in the development, allowing us to identify functional abstractions throughout the system. Using these building blocks, large configurations can be defined using functional and process composition, reducing the effort spent on adapting the system to the frequent changes in requirements. The server evolved from a prototype that was the result of a project supported by a regional cable company, and it is currently being used to provide services for real-world users. Despite our initial concerns, efficiency has not been a major issue.

Anxiety in cardiology. The use of pregabalin in the treatment of anxiety disorders in patients with cardiovascular diseases

2021 ◽  
Vol 14 (4) ◽  
pp. 428-432
Author(s):  
Anna Antosik-Wójcińska
Keyword(s):  
Cardiovascular Diseases ◽  
Early Diagnosis ◽  
Anxiety Disorders ◽  
Pharmacological Treatment ◽  
Anxiety Symptoms ◽  
Health Consequences ◽  
Cardiovascular Patients ◽  
Starting Point ◽  
Patient Prognosis ◽  
High Level

The paper discusses two issues: the multidirectional relationship between the occurrence of anxiety symptoms and cardiovascular diseases, and the influence of the persistently high level of anxiety on the course of cardiological diseases and patient prognosis. In the discussion on the negative health consequences of anxiety disorders, there is emphasized importance of early diagnosis of these disorders and implementation of its treatment. As a starting point there were presented clinical cases of cardiovascular patients in whom developed anxiety disorders. The following sections discuss various aspects of the pharmacological treatment of anxiety disorders, focusing on the possible use of pregabalin in this.

scholarly journals Prognostic Metrics Associated with Inflammation and Atherosclerosis Signaling Evaluate the Burden of Adverse Clinical Outcomes in Ischemic Stroke Patients

2020 ◽  
Vol 66 (11) ◽  
pp. 1434-1443
Author(s):  
Daoxia Guo ◽  
Zhengbao Zhu ◽  
Chongke Zhong ◽  
Aili Wang ◽  
Xuewei Xie ◽  
...  
Keyword(s):  
Ischemic Stroke ◽  
Clinical Outcomes ◽  
Pathway Analysis ◽  
Primary Outcome ◽  
Extreme Case ◽  
High Sensitivity ◽  
Additional Information ◽  
Reactive Protein ◽  
Significant Enrichment ◽  
High Level

Abstract Background Conventional prognostic risk factors can only partly explain the adverse clinical outcomes after ischemic stroke. We aimed to establish a set of prognostic metrics and evaluate its public health significance on the burden of adverse clinical outcomes of ischemic stroke. Methods All patients were from the China Antihypertensive Trial in Acute Ischemic Stroke (CATIS). We established prognostic metrics of ischemic stroke from 20 potential biomarkers in a propensity-score-matched extreme case sample (n = 146). Pathway analysis was conducted using Ingenuity Pathway Analysis. In the whole CATIS population (n = 3575), we evaluated effectiveness of these prognostic metrics and estimated their population-attributable fractions (PAFs) related to the risk of clinical outcomes. The primary outcome was a composite outcome of death or major disability (modified Rankin Scale score ≥3) at 3 months after stroke. Results Matrix metalloproteinase-9 (MMP-9), S100A8/A9, high-sensitivity C-reactive protein (hsCRP), and growth differentiation factor-15 (GDF-15) were selected as prognostic metrics for ischemic stroke. Pathway analysis showed significant enrichment in inflammation and atherosclerosis signaling. All 4 prognostic metrics were independently associated with poor prognosis of ischemic stroke. Compared with patients having 1 or 0 high-level prognostic metrics, those with 4 had higher risk of primary outcome (OR: 3.84, 95%CI: 2.67–5.51; PAF: 37.4%, 95%CI: 19.5%–52.9%). Conclusion The set of prognostic metrics, enriching in inflammation and atherosclerosis signaling, could effectively predict the prognosis at 3 months after ischemic stroke and would provide additional information for the burden of adverse clinical outcomes among patients with ischemic stroke.

A Context-Based Approach for Supporting Knowledge Work with Semantic Portals

2009 ◽  
pp. 231-253
Author(s):  
Thomas Hädrich ◽  
Torsten Priebe
Keyword(s):  
Knowledge Management ◽  
Business Processes ◽  
Knowledge Work ◽  
Semantic Web Technologies ◽  
Semantic Level ◽  
Starting Point ◽  
Knowledge Intensive ◽  
Communication Needs ◽  
High Level ◽  
High Degree

Knowledge work can be characterized by a high degree of variety and exceptions, strong communication needs, weakly structured processes, networks and communities, and as requiring a high level of skill and expertise as well as a number of specific practices. Process-oriented knowledge management suggests to focus on enhancing efficiency of knowledge work in the context of business processes. Portals are an enabling technology for knowledge management by providing users with a consolidated, personalized interface that allows accessing various types of structured and unstructured information. However, the design of portals still needs concepts and frameworks to guide their alignment with the context of persons consigned with knowledge-intensive tasks. In this context the concept of knowledge stance is a promising starting point. This paper discusses how knowledge stances can be applied and detailed to model knowledge work and support to support it with semantic context-based portals. We present the results from implementing a portal prototype that deploys Semantic Web technologies to integrate various information sources and applications on a semantic level and discuss extensions to this portal for the support of knowledge stances.

Sign in / Sign up

Export Citation Format

Share Document