Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAquarium: Cassiopea and Alewife Languages
91
0
0.0
(
0
)
Added by
Jingmei Hu
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
This technical report describes two of the domain-specific languages used in the Aquarium kernel code synthesis project. It presents the language cores in terms of abstract syntax. Cassiopea is a machine description language for describing the semantics of processor instruction sets. Alewife is a specification language that can be used to write machine-independent specifications for assembly-level instruction blocks. An Alewife specification can be used to verify and synthesize code for any machine described in Cassiopea, given a machine-specific translation for abstractions used in the specification. This article does not include an introduction to either the Aquarium system or the use of the languages. In addition to this version of the article being a draft, the Aquarium project and the languages are work in progress. This article cannot currently be considered either final or complete.
rate research
Read More
Specifying the semantics of a programming language formally can have many benefits. However, it can also require a huge effort. The effort can be significantly reduced by translating language syntax to so-called fundamental constructs (funcons). A translation to funcons is easy to update when the language evolves, and it exposes relationships between individual language constructs. The PLanCompS project has developed an initial collection of funcons (primarily for translation of functional and imperative languages). The behaviour of each funcon is defined, once and for all, using a modular variant of structural operational semantics. The definitions are available online. This paper introduces and motivates funcons. It illustrates translation of language constructs to funcons, and how funcons are defined. It also relates funcons to notation used in previous frameworks, including monadic semantics and action semantics.
XML database query languages such as XQuery employ regular expression types with structural subtyping. Subtyping systems typically have two presentations, which should be equivalent: a declarative version in which the subsumption rule may be used anywhere, and an algorithmic version in which the use of subsumption is limited in order to make typechecking syntax-directed and decidable. However, the XQuery standard type system circumvents this issue by using imprecise typing rules for iteration constructs and defining only algorithmic typechecking, and another extant proposal provides more precise types for iteration constructs but ignores subtyping. In this paper, we consider a core XQuery-like language with a subsumption rule and prove the completeness of algorithmic typechecking; this is straightforward for XQuery proper but requires some care in the presence of more precise iteration typing disciplines. We extend this result to an XML update language we have introduced in earlier work.
Domain-specific languages are becoming increasingly important. Almost every application touches multiple domains. But how to define, use, and combine multiple DSLs within the same application? The most common approach is to split the project along the domain boundaries into multiple pieces and files. Each file is then compiled separately. Alternatively, multiple languages can be embedded in a flexible host language: within the same syntax a new domain semantic is provided. In this paper we follow a less explored route of metamorphic languages. These languages are able to modify their own syntax and semantics on the fly, thus becoming a more flexible host for DSLs. Our language allows for dynamic creation of grammars and switching languages where needed. We achieve this through a novel concept of Syntax-Directed Execution. A language grammar includes semantic actions that are pieces of functional code executed immediately during parsing. By avoiding additional intermediate representation, connecting actions from different languages and domains is greatly simplified. Still, actions can generate highly specialized code though lambda encapsulation and Dynamic Staging.
Rust represents a major advancement in production programming languages because of its success in bridging the gap between high-level application programming and low-level systems programming. At the heart of its design lies a novel approach to ownership that remains highly programmable. In this talk, we will describe our ongoing work on designing a formal semantics for Rust that captures ownership and borrowing without the details of lifetime analysis. This semantics models a high-level understanding of ownership and as a result is close to source-level Rust (but with full type annotations) which differs from the recent RustBelt effort that essentially models MIR, a CPS-style IR used in the Rust compiler. Further, while RustBelt aims to verify the safety of unsafe code in Rusts standard library, we model standard library APIs as primitives, which is sufficient to reason about their behavior. This yields a simpler model of Rust and its type system that we think researchers will find easier to use as a starting point for investigating Rust extensions. Unlike RustBelt, we aim to prove type soundness using progress and preservation instead of a Kripke logical relation. Finally, our semantics is a family of languages of increasing expressive power, where subsequent levels have features that are impossible to define in previous levels. Following Felleisen, expressive power is defined in terms of observational equivalence. Separating the language into different levels of expressive power should provide a framework for future work on Rust verification and compiler optimization.
This EPTCS volume contains the proceedings of the 16th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2019) held in Prague, Czech Republic, on Sunday 7 April 2019. QAPL 2019 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019). QAPL focuses on quantitative aspects of computations, which may refer to the use of physical quantities (time, bandwidth, etc.) as well as mathematical quantities (e.g., probabilities) for the characterisation of the behaviour and for determining the properties of systems. Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of the QAPL workshop series is to discuss the explicit use of time and probability and general quantities either directly in the model or as a tool for the analysis or synthesis of systems. The 16th edition of QAPL also focuses on discussing the developments, challenges and results in this area covered by our workshop in its nearly 20-year history.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
