Type systems and syntactic sugar are both valuable to programmers, but sometimes at odds. While sugar is a valuable mechanism for implementing realistic languages, the expansion process obscures program source structu...
详细信息
ISBN:
(纸本)9781450356985
Type systems and syntactic sugar are both valuable to programmers, but sometimes at odds. While sugar is a valuable mechanism for implementing realistic languages, the expansion process obscures program source structure. As a result, type errors can reference terms the programmers did not write (and even constructs they do not know), baffling them. The language developer must also manually construct type rules for the sugars, to give a typed account of the surface language. We address these problems by presenting a process for automatically reconstructing type rules for the surface language using rules for the core. We have implemented this theory, and show several interesting case studies.
For decades, the design and implementation of programminglanguages has been based on phrase structure grammars, which divide a program recursively into phrases (represented by nonterminals), leaving the words of the ...
详细信息
ISBN:
(纸本)9781450355308
For decades, the design and implementation of programminglanguages has been based on phrase structure grammars, which divide a program recursively into phrases (represented by nonterminals), leaving the words of the program (the terminals) as the atoms of this division. By contrast, dependency grammar suggests that dependency between words, not constituency between phrases, is the primary grammatical relationship, and that a grammar capturing this relationship is basically a lexicon. In this paper, I suggest the use of dependency grammar for the design and implementation of programminglanguages. This allows me to unify the dictionaries populated by programs (with variables, procedures, functions, etc.) written in a programminglanguage with the grammar of this language. I call the compilation of a programminglanguage and its programs into a lexicon a langram and, using the example of the while language, show how langrams serve the "growing of languages".
Self-representation - the ability to represent programs in their own language - has important applications in reflective languages and many other domains of programminglanguagedesign. Although approaches to designin...
详细信息
ISBN:
(纸本)9781605583921
Self-representation - the ability to represent programs in their own language - has important applications in reflective languages and many other domains of programminglanguagedesign. Although approaches to designing typed program representations for sublanguages of some base language have become quite popular recently, the question whether a fully metacircular typed self-representation is possible is still open. This paper makes a big step towards this aim by defining the F(omega)* calculus, an extension of the higher-order polymorphic lambda calculus F. that allows type self-representations. While the usability of these representations for metaprogramming is still limited, we believe that our approach makes a significant step towards a new generation of reflective languages that are both safe and efficient.
Functional Reactive programming, or FRP. is a general framework for programming hybrid systems in a high-level, declarative manner. The key ideas in FRP are its notions of behaviors and events. Behaviors are time-vary...
详细信息
ISBN:
(纸本)9781581131994
Functional Reactive programming, or FRP. is a general framework for programming hybrid systems in a high-level, declarative manner. The key ideas in FRP are its notions of behaviors and events. Behaviors are time-varying, reactive value while events are time-ordered sequences of discrete-time event occurrences. FRP is the essence of Fran, a domain-specific language embedded in Haskell for programming reactive animations, but FRP is now also being used in vision, robotics and other control systems applications. In this paper we explore the formal semantics of FRP and how it relates to an implementation based on streams that represent (and therefore only approximate) continuous behaviors. We show that, in the limit as the sampling interval goes to zero, the implementation is faithful to the formal, continuous semantics, but only when certain constraints on behaviors are observed. We explore the nature of these constraints, which vary amongst the FRP primitives. Our results show both the pou er and limitations of this approach to languagedesign and implementation. As an example of a limitation, we show that streams are incapable of representing instantaneous predicate events over behaviors.
The maturation of the Web platform has given rise to sophisticated and demanding Web applications such as interactive 3D visualization, audio and video software, and games. With that, efficiency and security of code o...
详细信息
ISBN:
(纸本)9781450349888
The maturation of the Web platform has given rise to sophisticated and demanding Web applications such as interactive 3D visualization, audio and video software, and games. With that, efficiency and security of code on the Web has become more important than ever. Yet JavaScript as the only built-in language of the Web is not well-equipped to meet these requirements, especially as a compilation target. Engineers from the four major browser vendors have risen to the challenge and collaboratively designed a portable low-level bytecode called WebAssembly. It offers compact representation, efficient validation and compilation, and safe low to no-overhead execution. Rather than committing to a specific programming model, WebAssembly is an abstraction over modern hardware, making it language-, hardware-, and platform-independent, with use cases beyond just the Web. WebAssembly has been designed with a formal semantics from the start. We describe the motivation, design and formal semantics of WebAssembly and provide some preliminary experience with implementations.
Partial redundancy elimination (PRE), the most important component of global optimizers, generalizes the removal of common subexpressions and loop-invariant computations. Achieving a complete PRE while incurring an ac...
详细信息
ISBN:
(纸本)9780897919876
Partial redundancy elimination (PRE), the most important component of global optimizers, generalizes the removal of common subexpressions and loop-invariant computations. Achieving a complete PRE while incurring an acceptable code growth is the main focus of the study. An algorithm for complete removal of partial redundancies, based on the integration of code motion and control flow restructuring is presented. In contrast to existing complete techniques, resort to restructuring merely to remove obstacles to code motion, rather than to carry out the actual optimization.
A general class of program analyses are a combination of context-free and regular language reachability. We define regularly annotated set constraints, a constraint formalism that captures this class. Our results exte...
详细信息
ISBN:
(纸本)9781595936332
A general class of program analyses are a combination of context-free and regular language reachability. We define regularly annotated set constraints, a constraint formalism that captures this class. Our results extend the class of reachability problems expressible naturally in a single constraint formalism, including such diverse applications as interprocedural dataflow analysis, precise type-based flow analysis, and pushdown model checking.
This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune...
详细信息
ISBN:
(纸本)9781450334686
This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.
暂无评论