اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدLightweight compilation of (C)LP to JavaScript
149
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We present and evaluate a compiler from Prolog (and extensions) to JavaScript which makes it possible to use (constraint) logic programming to develop the client side of web applications while being compliant with current industry standards. Targeting JavaScript makes (C)LP programs executable in virtually every modern computing device with no additional software requirements from the point of view of the user. In turn, the use of a very high-level language facilitates the development of high-quality, complex software. The compiler is a back end of the Ciao system and supports most of its features, including its module system and its rich language extension mechanism based on packages. We present an overview of the compilation process and a detailed description of the run-time system, including the support for modular compilation into separate JavaScript code. We demonstrate the maturity of the compiler by testing it with complex code such as a CLP(FD) library written in Prolog with attributed variables. Finally, we validate our proposal by measuring the performance of some LP and CLP(FD) benchmarks running on top of major JavaScript engines.
قيم البحث
اقرأ أيضاً
We present a set of rules for compiling a Dalvik bytecode program into a logic program with array constraints. Non-termination of the resulting program entails that of the original one, hence the techniques we have presented before for proving non-te
rmination of constraint logic programs can be used for proving non-termination of Dalvik programs.
Researchers have developed various techniques for static analysis of JavaScript to improve analysis precision. To develop such techniques, they first identify causes of the precision losses for unproven properties. While most of the existing work has
diagnosed main causes of imprecision in static analysis by manual investigation, manually tracing the imprecision causes is challenging because it requires detailed knowledge of analyzer internals. Recently, several studies proposed to localize the analysis imprecision causes automatically, but these localization techniques work for only specific analysis techniques. In this paper, we present an automatic technique that can trace analysis imprecision causes of JavaScript applications starting from user-selected variables. Given a set of program variables, our technique stops an analysis when any of the variables gets imprecise analysis values. It then traces the imprecise analysis values using intermediate analysis results back to program points where the imprecision first started. Our technique shows the trace information with a new representation called tracing graphs, whose nodes and edges together represent traces from imprecise points to precise points. In order to detect major causes of analysis imprecision automatically, we present four node/edge patterns in tracing graphs for common imprecision causes. We formalized the technique of generating tracing graphs and identifying patterns, and implemented them on SAFE, a state-of-the-art JavaScript static analyzer with various analysis configurations, such as context-sensitivity, loop-sensitivity, and heap cloning. Our evaluation demonstrates that the technique can easily find 96 % of the major causes of the imprecision problems in 17 applications by only automatic detection in tracing graphs using the patterns, and selectively adopting various advanced techniques can eliminate the found causes of imprecision.
We argue that the implementation and verification of compilers for functional programming languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying idea of HOAS
is to use a meta-language that provides a built-in and logical treatment of binding related notions. By embedding the meta-language within a larger programming or reasoning framework, it is possible to absorb the treatment of binding structure in the object language into the meta-theory of the system, thereby greatly simplifying the overall implementation and reasoning processes. We develop the above argument in this thesis by presenting and demonstrating the effectiveness of an approach to the verified implementation of compiler transformations for functional programs that exploits HOAS. In this approach, transformations on functional programs are first articulated in the form of rule-based relational specifications. These specifications are rendered into programs in the language lambda Prolog. On the one hand, these programs serve directly as implementations. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. Both lambda Prolog and Abella support the use of the HOAS approach. Thus, they constitute a framework that can be used to test out the benefits of the HOAS approach in verified compilation. We use them to implement and verify a compiler for a representative functional programming language that embodies the transformations that form the core of many compilers for such languages. In both the programming and the reasoning phases, we show how the use of the HOAS approach significantly simplifies the representation, manipulation, analysis and reasoning of binding structure.
The current demands for seamless connections with the surrounding environment make software more reactive. For example, such demands are evident in systems consisting of the Internet of Things. Such systems include a set of reactive values that are p
eriodically updated in response to external or internal events to form a dataflow in the sense that such updates are propagated to other reactive values. Two effective approaches for realizing such reactive values have been proposed: the event mechanisms in event-based programming and the signals in functional-reactive programming. These two approaches are now becoming mixed in several languages such as Flapjax and REScala, which makes these languages notably expressive for modularizing the implementation of reactive software. For example, REScala provides a rich API that consists of functions converting events to signals and vice versa. In this paper, we explore another, simpler approach in the design space of reactive programming languages: the event mechanism is harmonized with signals, resulting in a simplified programming interface that is mostly based on signals. Based on this approach, we realize SignalJ, a simple extension of Java with events and signals. Our notable findings are (1) an event can be represented as an update of a signal and (2) such an effectful signal can be represented using annotations instead of introducing types and constructors for signals to further simplify the language. Another contribution of this paper is the formal model of SignalJ. As both mechanisms of events and signals may interfere with each other, this mixing sometimes results in surprising behavior. For example, the functional behavior of signals is affected by the imperative features of events. Thus, understanding the formal model of this mixing is actually important. The core calculus, Featherweight SignalJ (FSJ), was developed as an extension of Featherweight Java, and proofs are provided to ensure the soundness of FSJ.
The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC c
alculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
