Both XML and Lisp have demonstrated the utility of generic syntax for expressing tree-structured data. But generic languages do not provide the syntactic richness of custom languages. generic Extensible Language (Gel)...
详细信息
ISBN:
(纸本)9783642030338
Both XML and Lisp have demonstrated the utility of generic syntax for expressing tree-structured data. But generic languages do not provide the syntactic richness of custom languages. generic Extensible Language (Gel) is a rich generic syntax that embodies many of the common syntactic conventions for operators, grouping and lists in widely-used languages. Prefix/infix operators are disambiguated by white-space, so that documents which violate common white-space conventions will not necessarily parse correctly with Gel. With some character replacements and adjusting for mismatch in operator precedence, Gel can extract meaningful structure from typical files in many languages, including Java, Cascading Style Sheets, Smalltalk, and ANTLR grammars. This evaluation shows the expressive power of Gel, not that Gel can be used as a parser for existing languages. Gel is intended to serve as a generic language for creating composable domain-specific languages.
Java is quickly becoming the most popular platform for distributed computing. However, its performance is still subject to concerns in comparison to other programming languages such as C and Fortran. As a consequence,...
详细信息
Two general techniques for implementing a domain-specific language (DSL) with less overhead are the finally-tagless embedding of object programs and the direct-style representation of side effects. We use these techni...
详细信息
ISBN:
(纸本)9783642030338
Two general techniques for implementing a domain-specific language (DSL) with less overhead are the finally-tagless embedding of object programs and the direct-style representation of side effects. We use these techniques to build a DSL for probabilistic programming, for expressing countable probabilistic models and performing exact inference and importance sampling on them. Our language is embedded as an ordinary OCaml library and represents probability distributions as ordinary OCaml programs. We use delimited continuations to reify probabilistic programs as lazy search trees, which inference algorithms may traverse without imposing any interpretive overhead on deterministic parts of a model. We thus take advantage of the existing OCaml implementation to achieve competitive performance and ease of use. Inference algorithms can easily be embedded in probabilistic programs themselves.
Many well-established concepts of object-oriented programming work for individual objects, but do not support object structures. The development of a verifying compiler requires enhancements of programming theory to c...
详细信息
ISBN:
(纸本)9783540691471
Many well-established concepts of object-oriented programming work for individual objects, but do not support object structures. The development of a verifying compiler requires enhancements of programming theory to cope with this deficiency. In this paper, we support this position by showing that classical specification and verification techniques support invariants for individual objects whose fields are primitive values, but are unsound for invariants involving more complex object structures. We have developed an ownership model, which allows one to structure the object store and to restrict reference passing and the operations that can be performed on references. We use this model to generalize classical object invariants to cover such object structures. We summarize the state of our work and identify open research challenges.
The Spec# programming system [4] is a new attempt to increase the quality of general purpose, industrial software. Using old wisdom, we propose the use of specifications to make programmer assumptions explicit. Using ...
详细信息
ISBN:
(纸本)9783540691471
The Spec# programming system [4] is a new attempt to increase the quality of general purpose, industrial software. Using old wisdom, we propose the use of specifications to make programmer assumptions explicit. Using modern technology, we propose the use of tools to enforce the specifications. To increase its chances of having impact, we want to design the system so that it can be widely adopted.
We present a constructive approach to correctness and exemplify it by describing a generator for certified Java Card applets that we are building. A proof of full functional correctness is generated, along with the co...
详细信息
ISBN:
(纸本)9783540691471
We present a constructive approach to correctness and exemplify it by describing a generator for certified Java Card applets that we are building. A proof of full functional correctness is generated, along with the code, from the specification;the proof can be independently checked by a simple proof checker, so that the larger and more complex generator needs not be trusted. We argue that such an approach is a valuable alternative to post-hoc verification, in addressing the Program Verifier Grand Challenge.
How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike?...
详细信息
ISBN:
(纸本)9783540691471
How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. The time has come to bring together the theorem proving and programming language communities to address this problem. We have proposed the POPLMARK challenge as a concrete set of benchmarks intended both for measuring progress in this area and for stimulating discussion and collaboration. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses.
We argue for the importance of tool integration in achieving the Program Verifier Grand Challenge. In particular, we argue for what we call strong integration, i.e. a co-operative style of interaction between tools. W...
详细信息
ISBN:
(纸本)9783540691471
We argue for the importance of tool integration in achieving the Program Verifier Grand Challenge. In particular, we argue for what we call strong integration, i.e. a co-operative style of interaction between tools. We propose the use of an existing planning technique, called proof planning, as a possible basis for achieving strong integration.
In this paper, we consider the Grand Challenge under a very specific perspective: the enabling of application experts without programming knowledge to reliably model their business processes/applications in a fashion ...
详细信息
ISBN:
(纸本)9783540691471
In this paper, we consider the Grand Challenge under a very specific perspective: the enabling of application experts without programming knowledge to reliably model their business processes/applications in a fashion that allows for a subsequent automatic realization on a given platform. This goal, which aims at simplifying the tasks of the many at the cost of ambitious and laborious tasks for the few, adds a new dimension to the techniques and concepts aimed at by the Grand Challenge: the application-specific design of platforms tailored for the intended goal. We are convinced that the outlined perspective provides a realistic and economically important milestone for the Grand Challenge.
A colleague of ours, Dr. Timothy Mattson of Intel, once made the following observation: "Literature professors read literature. Computer Science professors should at least occasionally read code." The point ...
详细信息
暂无评论