SwePub - sökning: WFRF:(Taha Walid 1971 )

Numrering	Referens	Omslagsbild	Hitta
1.	Belwal, Chaitanya, et al. (författare) Release Offset Bounds for Response Time Analysis of P-FRP using Exhaustive Enumeration 2011 Ingår i: 2011 IEEE 10th International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom). - Piscataway, N.J. : IEEE Press. - 9781457721359 ; , s. 950-957 Konferensbidrag (refereegranskat)abstract Functional*Reactive Programming (FRP) is a declarative approach to modeling and building reactive systems. Priority-based FRP (P-FRP) is a formalism of FRP that guarantees real-time response. Unlike the classical preemptive model1 of real-time systems, preempted tasks in PFRP are aborted and have to restart when higher priority tasks have completed. Due to this abort-restart of nature of preemption, there is no single critical instant of release that leads to Worst-Case Response Time (WCRT) of lower priority P-FRP tasks. At this time, the only method for determining the WCRT is through an exhaustive enumeration of all release offsets of higher priority tasks between the release and deadline of the lower priority task. This makes the computational cost of WCRT dependent on the deadline of a task, and when such deadlines are large the computational costs of this technique make it infeasible even for small task sets. In this paper, we show that the release offsets of higher priority tasks have a lower and upper bound and present techniques to derive these bounds. By enumerating only those release offsets while lie within our derived bounds the number of release scenarios that have to be enumerated is significantly reduced. This leads to lower computational costs and makes determination of the WCRT in P-FRP a practically feasible proposition. © 2011 IEEE.
2.	Belwal, Chaitanya, et al. (författare) Timing Analysis of the Priority based FRP System 2008 Ingår i: Proceedings Work-In-Progress Session of the 14th Real-Time and Embedded Technology and Applications Symposium. - Lincoln, NE : University of Nebraska–Lincoln, Computer Science and Engineering. ; , s. 89-92 Konferensbidrag (refereegranskat)abstract Kaiabachev, Taha, Zhu [1] have presented a declarative programming paradigm called Functional Reactive Programming, which is based on behaviors and events. An improved system called P-FRP uses fixed priority scheduling for tasks. The system allows for the currently executing lower priority tasks to be rolled back to restoring the original state and allowing a higher priority task to run. These aborted tasks will restart again when no tasks of higher priority are in the queue. Since P-FRP has many applications in the real time domain it is critical to understand the time bound in which the tasks which have been aborted are guaranteed to run, and if the task set is schedulable. In this paper we provide an analysis of the unique execution paradigm of the P-FRP system and study the timing bounds using different constraint variables.1. R. Kaiabachev, W. Taha, A. Zhu, E-FRP with priorities, In the Proceedings of the 7th ACM & IEEE international conference on Embedded software, Pages: 221 - 230, 2007.
3.	Benaissa, Zine El-Abidine, et al. (författare) Logical Modalities and Multi-Stage Programming 1999 Konferensbidrag (refereegranskat)abstract Multi-stage programming is a method for improving the performance of programs through the introduction of controlled program specialization. This paper makes a case for multi-stage programming with open code and closed values. We argue that a simple language exploiting interactions between two logical modalities is well suited for multi-stage programming, and report the results from our study of categorical models for multi-stage languages.
4.	Brauner, Paul, et al. (författare) Globally Parallel, Locally Sequential : A Preliminary Proposal for Acumen Objects 2010 Ingår i: POOSC'10, Proceedings of the 9th Workshop on Parallel/High-Performance Object-Oriented Scientific Computing. - New York, NY : ACM Press. - 9781450305464 Konferensbidrag (refereegranskat)abstract An important and resource-intensive class of computation codes consists of simulators for physical systems. Today, most simulation codes are written in general-purpose imperative languages such as C or FORTRAN. Unfortunately, such languages encourage the programmer to focus her attention on details of how the computation is performed, rather than on the system being modeled.This paper reports the design and implementation of a novel notion of an object for a physical modeling language called Acumen. A key idea underlying the language's design is encouraging a programming style that enables a "globally parallel, locally imperative" view of the world. The language is also being designed to preserve deterministic execution even when the underlying computation is performed on a highly parallel platform. Our main observation with the initial study is that extensive and continual experimental evaluation is crucial for keeping the language design process informed about bottlenecks for parallel execution.
5.	Bruneau, Julien, et al. (författare) Preliminary Results in Virtual Testing for Smart Building 2010 Ingår i: Proceedings of MOBIQUITOUS 2010, 7th International ICST Conference on Mobile and Ubiquitous Systems. ; , s. 2- Konferensbidrag (refereegranskat)abstract Smart buildings promise to revolutionize the way we live. Applications ranging from climate control to fire management can have significant impact on the quality and cost of these services. However, a smart building and any technology with direct effect on the safety of its occupants must undergo extensive testing. Virtual testing by means of computer simulation can significantly reduce the cost of testing and, as a result, accelerate the development of novel applications. Unfortunately, building physically-accurate simulation codes can be labor intensive. To address this problem, we propose a framework for rapid, physically-accurate virtual testing of smart building systems. The proposed framework supports analytical modeling and simulation of both a discrete distributed system as well as the physical environment that hosts it.
6.	Bruneau, Julien, et al. (författare) Preliminary results in virtual testing for smart buildings 2012 Ingår i: Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering. - Heidelberg : Springer Berlin/Heidelberg. - 1867-8211 .- 1867-822X. ; 73, s. 347-349 Tidskriftsartikel (refereegranskat)abstract Smart buildings promise to revolutionize the way we live. Applications ranging from climate control to fire management can have significant impact on the quality and cost of these services. However, a smart building and any technology with direct effect on the safety of its occupants must undergo extensive testing. Virtual testing by means of computer simulation can significantly reduce the cost of testing and, as a result, accelerate the development of novel applications. Unfortunately, building physically-accurate simulation codes can be labor intensive. To address this problem, we propose a framework for rapid, physically-accurate virtual testing of smart building systems. The proposed framework supports analytical modeling and simulation of both a discrete distributed system as well as the physical environment that hosts it. © 2012 Springer-Verlag Berlin Heidelberg.
7.	Bruneau, Julien, et al. (författare) Virtual Testing for Smart Buildings 2012 Ingår i: 2012 Eighth International Conference on Intelligent Environments. - Piscataway, N.J. : IEEE Press. - 9781467320931 - 9780769547411 ; , s. 282-289 Konferensbidrag (refereegranskat)abstract Smart buildings promise to revolutionize the way we live. Applications ranging from climate control to fire management can have significant impact on the quality and cost of these services. However, smart buildings and any technology with direct effect on human safety and life mustundergo extensive testing. Virtual testing by means of computer simulation can significantly reduce the cost of testing and, as a result, accelerate the development of novel applications. Unfortunately, building physically-accurate simulation codes can be labor intensive.To address this problem, we propose a framework for rapid, physically-accurate virtual testing. The proposed framework supports analytical modeling of both a discrete distributed system as well as the physical environment that hosts it. The discrete models supported are accurate enough to allow the automatic generation of a dedicated programming framework that will help the developer in the implementation of these systems. The physical environment models supported are equational specifications that are accurate enough to produce running simulation codes. Combined, these two frameworks enable simulating both active systems and physical environments. These simulations can be used to monitor the behavior and gather statistics about the performance of an application in the context of precise virtual experiments. To illustrate the approach, we present models of Heating, Ventilating and Air-Conditioning (HVAC) systems. Using these models, we construct virtual experiments that illustrate how the approach can be used to optimize energy and cost of climate control for a building. © 2012 IEEE.
8.	Calcagno, Cristiano, et al. (författare) Closed Types as a Simple Approach to Safe Imperative Multi-Stage Programming 2000 Ingår i: Automata, Languages and Programming. - Heidelberg : Springer. - 9783540677154 - 9783540450221 ; , s. 25-36 Konferensbidrag (refereegranskat)abstract Safely adding computational effects to a multi-stage language has been an open problem. In previous work, a closed type constructor was used to provide a safe mechanism for executing dynamically generated code. This paper proposes a general notion of closed type as a simple approach to safely introducing computational effects into multi-stage languages. We demonstrate this approach formally in a core language called Mini-MLref BN. This core language combines safely multi-stage constructs and ML-style references. In addition to incorporating state, Mini-ML ref BN also embodies a number of technical improvements over previously proposed core languages for multi-stage programming.
9.	Calcagno, Cristiano, et al. (författare) Implementing Multi-stage Languages Using ASTs, Gensym, and Reﬂection 2003 Ingår i: Generative Programming and Component Engineering. - Heidelberg : Springer Berlin/Heidelberg. - 9783540201021 - 9783540398158 ; , s. 57-76 Konferensbidrag (refereegranskat)abstract The paper addresses theoretical and practical aspects of implementing multi-stage languages using abstract syntax trees (ASTs), gensym, and reflection. We present an operational account of the correctness of this approach, and report on our experience with a bytecode compiler called MetaOCaml that is based on this strategy. Current performance measurements reveal interesting characteristics of the underlying OCaml compiler, and illustrate why this strategy can be particularly useful for implementing domain-specific languages in a typed, functional setting. © Springer-Verlag Berlin Heidelberg 2003.
10.	Calcagno, Cristiano, et al. (författare) ML-like Inference for Classiﬁers 2004 Ingår i: Programming Languages and Systems. - Heidelberg : Springer Berlin/Heidelberg. - 9783540213130 - 9783540247258 ; , s. 79-93 Konferensbidrag (refereegranskat)abstract Environment classifiers were proposed as a new approach to typing multi-stage languages. Safety was established in the simply-typed and let-polymorphic settings. While the motivation for classifiers was the feasibility of inference, this was in fact not established. This paper starts with the observation that inference for the full classifier-based system fails. We then identify a subset of the original system for which inference is possible. This subset, which uses implicit classifiers, retains significant expressivity (e.g. it can embed the calculi of Davies and Pfenning) and eliminates the need for classifier names in terms. Implicit classifiers were implemented in MetaOCaml, and no changes were needed to make an existing test suite acceptable by the new type checker. © Springer-Verlag 2004.
11.	Chen, Fulong, et al. (författare) Implicitly Heterogeneous Multi-Stage Programming for FPGAs 2011 Ingår i: Journal of Computational Information Systems. - Bethel, USA : Binary Information Press. - 1553-9105. ; 6:14, s. 4915-4922 Tidskriftsartikel (refereegranskat)abstract Previous work on semantics-based multi-state programming language design focused on homogeneous and heterogeneous software designs. In homogenous software design, the source and the target software programming languages are the same. In heterogeneous software design, they are different software languages. This paper proposes a practical means to circuit design by providing specialized offshoring translations from subsets of the source software programming language to subsets of the target hardware description language (HDL). This approach avoids manually writing codes for specifying the circuit of the given algorithm. To illustrate the proposed approach, we design and implement a translation to a subset of Verilog suitable numerical and logical computation. Through the translator, programmers can specify abstract algorithms in high level languages and automatically convert them into circuit descriptions in low level languages.© 2010 Binary Information Press.
12.	Chen, Fulong, et al. (författare) Multi-Stage Programming for High-Level Description of Circuit Families 2010 Ingår i: CISP 2010. - Piscataway, N.J. : IEEE Press. - 9781424465132 ; , s. 3003-3007 Konferensbidrag (refereegranskat)abstract Hardware description languages use a low level of abstraction making the task of hardware designers error-prone and time consuming. The resulting descriptions tend to be lengthy and hard to reason about. This paper presents a minimal functional language for describing hardware circuits. Using multistage programming concepts, Fast Fourier Transform circuit descriptions can be generated in this language from a higher level generic description. It bridges the gap between the generated code and the required low-level hardware description by presenting the translator to automatically convert the generated code into Verilog, a streamline hardware description language.
13.	Czarnecki, Krzysztof, et al. (författare) DSL Implementation in MetaOCaml, Template Haskell, and C+ 2004 Ingår i: Domain-Specific Program Generation. - Berlin : Springer Berlin/Heidelberg. - 9783540221197 - 9783540259350 ; , s. 51-72 Konferensbidrag (refereegranskat)abstract A wide range of domain-specific languages (DSLs) has been implemented successfully by embedding them in general purpose languages. This paper reviews embedding, and summarizes how two alternative techniques - staged interpreters and templates - can be used to overcome the limitations of embedding. Both techniques involve a form of generative programming. The paper reviews and compares three programming languages that have special support for generative programming. Two of these languages (MetaOCaml and Template Haskell) are research languages, while the third (C++) is already in wide industrial use. The paper identifies several dimensions that can serve as a basis for comparing generative languages.
14.	Dillon, Tharam, et al. (författare) Message from U-Science 2014 general chairs 2014 Ingår i: 2014 IEEE 12th International Conference on Dependable, Autonomic and Secure Computing. - Piscataway : IEEE. - 9781479950799 - 9781479950782 Konferensbidrag (populärvet., debatt m.m.)abstract Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.© 2014 IEEE
15.	Duracz, Adam, et al. (författare) A Semantic Account of Rigorous Simulation 2018 Ingår i: Principles of Modeling. - Amsterdam : Springer Berlin/Heidelberg. - 9783319952451 - 9783319952468 ; , s. 223-239 Bokkapitel (refereegranskat)abstract Hybrid systems are a powerful formalism for modeling cyber-physical systems. Reachability analysis is a general method for checking safety properties, especially in the presence of uncertainty and non-determinism. Rigorous simulation is a convenient tool for reachability analysis of hybrid systems. However, to serve as proof tool, a rigorous simulator must be correct w.r.t. a clearly defined notion of reachability, which captures what is intuitively reachable in finite time. As a step towards addressing this challenge, this paper presents a rigorous simulator in the form of an operational semantics and a specification in the form of a denotational semantics. We show that, under certain conditions about the representation of enclosures, the rigorous simulator is correct. We also show that finding a representation satisfying these assumptions is non-trivial. © 2018, Springer International Publishing AG, part of Springer Nature.
16.	Eckhardt, Jason, et al. (författare) Implicitly Heterogeneous Multi-Stage Programming 2005 Ingår i: Generative Programming and Component Engineering. - Heidelberg : Springer. - 3540291385 - 9783540291381 ; , s. 275-292 Konferensbidrag (refereegranskat)abstract Previous work on semantics-based multi-stage programming(MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designssimply add a hygienic quasi-quotation and evaluation mechanism to abase language. An apparent disadvantage of this approach is that theprogrammer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means toavoid this by providing specialized translations from subsets of the baselanguage to diﬀerent target languages. This approach preserves the homogeneous “look” of multi-stage programs, and, more importantly, thestatic guarantees about the generated code. In addition, compared to anexplicitly heterogeneous approach, it promotes reuse of generator sourcecode and systematic exploration of the performance characteristics of thetarget languages.To illustrate the proposed approach, we design and implement a translation to a subset of C suitable for numerical computation, and show thatit preserves static typing. The translation is implemented, and evaluatedwith several benchmarks. The implementation is available in the onlinedistribution of MetaOCaml.
17.	Eckhardt, Jason, et al. (författare) Implicitly Heterogeneous Multi-stage Programming 2007 Ingår i: New generation computing. - Tokyo : Springer-Verlag Tokyo Inc.. - 0288-3635 .- 1882-7055. ; 25:3, s. 305-336 Tidskriftsartikel (refereegranskat)abstract Previous work on semantics-based multi-stage programming (MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designs simply add a hygienic quasi-quotation and evaluation mechanism to a base language. An apparent disadvantage of this approach is that the programmer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means to avoid this by providing specialized translations from subsets of the base language to different target languages. This approach preserves the homogeneous “look” of multi-stage programs, and, more importantly, the static guarantees about the generated code. In addition, compared to an explicitly heterogeneous approach, it promotes reuse of generator source code and systematic exploration of the performance characteristics of the target languages.To illustrate the proposed approach, we design and implement a translation to a subset of C suitable for numerical computation, and show that it preserves static typing. The translation is implemented, and evaluated with several benchmarks. The implementation is available in the online distribution of MetaOCaml.
18.	Ellner, Stephan, et al. (författare) The Semantics of Graphical Languages 2007 Ingår i: PEPM 2007. - New York, NY : ACM Press. - 9781595936202 ; , s. 122-133 Konferensbidrag (refereegranskat)abstract Visual notations are pervasive in circuit design, control systems, and increasingly in mainstream programming environments. Yet many of the foundational advances in programming language theory are taking place in the context of textual notations. In order to map such advances to the graphical world, and to take the concerns of the graphical world into account when working with textual formalisms, there is a need for rigorous connections between textual and graphical expressions of computation. To this end, this paper presents a graphical calculus called Uccello. Our key insight is that Ariola and Blom's work on sharing in the cyclic lambda calculus provides an excellent foundation for formalizing the semantics of graphical languages. As an example of what can be done with this foundation, we use it to extend a graphical language with staging constructs. In doing so, we provide the first formal account of sharing in a multi-stage calculus. Copyright © 2007 ACM.
19.	Fogarty, Seth, et al. (författare) Concoqtion : Indexed Types Now! 2007 Ingår i: PEPM 2007. - New York, NY : ACM Press. - 1595936203 - 9781595936202 ; , s. 112-121 Konferensbidrag (refereegranskat)abstract Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate Fω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.
20.	Ganz, Steven E., et al. (författare) Macros as Multi-Stage Computations : Type-Safe, Generative, Binding Macros in MacroML 2001 Ingår i: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01). - New York, N.Y. : ACM Press. - 1581134150 ; , s. 74-85 Konferensbidrag (refereegranskat)abstract With few exceptions, macros have traditionally been viewed as operations on syntax trees or even on plain strings. This view makes macros seem ad hoc, and is at odds with two desirable features of contemporary typed functional languages: static typing and static scoping. At a deeper level, there is a need for a simple, usable semantics for macros. This paper argues that these problems can be addressed by formally viewing macros as multi-stage computations. This view eliminates the need for freshness conditions and tests on variable names, and provides a compositional interpretation that can serve as a basis for designing a sound type system for languages supporting macros, or even for compilation. To illustrate our approach, we develop and present MacroML, an extension of ML that supports inlining, recursive macros, and the definition of new binding constructs. The latter is subtle, and is the most novel addition in a statically typed setting. The semantics of a core subset of MacroML is given by an interpretation into MetaML, a statically-typed multi-stage programming language. It is then easy to show that MacroML is stage- and type-safe: macro expansion does not depend on runtime evaluation, and both stages do not "go wrong.
21.	Gillenwater, Jennifer, et al. (författare) Synthesizable high level hardware descriptions : using statically typed two-level languages to guarantee verilog synthesizability 2008 Ingår i: PEPM '08. - New York, NY, USA : ACM Press. - 9781595939777 ; , s. 13-20 Konferensbidrag (refereegranskat)abstract Modern hardware description languages support code-generation constructs like generate/endgenerate in Verilog. These constructs are intended to describe regular or parameterized hardware designs and, when used effectively, can make hardware descriptions shorter, more understandable, and more reusable. In practice, however, designers avoid these constructs because it is difficult to understand and predict the properties of the generated code. Is the generated code even type safe? Is it synthesizable? What physical resources (e.g. combinatorial gates and flip-flops) does it require? It is often impossible to answer these questions without first generating the fully-expanded code. In the Verilog and VHDL communities, this generation process is referred to as elaboration.This paper proposes a disciplined approach to elaboration in Verilog. By viewing Verilog as a statically typed two-level language, we are able to reflect the distinction between values that are known at elaboration time and values that are part of the circuit computation. This distinction is crucial for determining whether abstractions such as iteration and module parameters are used in a synthesizable manner. To illustrate this idea, we develop a core calculus for Verilog that we call Featherweight Verilog (FV) and an associated static type system. We formally define a preprocessing step analogous to the elaboration phase of Verilog, and the kinds of errors that can occur during this phase. Finally, we show that a well-typed design cannot cause preprocessing errors, and that the result of its expansion is always a synthesizable circuit.
22.	Kaiabachev, Roumen, et al. (författare) E-FRP with Priorities 2007 Ingår i: EMSOFT '07. - New York, NY : ACM Press. - 9781595938251 ; , s. 221-230 Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract E-FRP is declarative language for programming resourcebounded,event-driven systems. The original high-level semanticsof E-FRP requires that each event handler executeatomically. This requirement facilitates reasoning about EFRPprograms, and therefore it is a desirable feature of thelanguage. But the original compilation strategy requiresthat each handler complete execution before another eventcan occur. This implementation choice treats all eventsequally, in that it forces the upper bound on the time neededto respond to any event to be the same. While this is acceptablefor many applications, it is often the case that someevents are more urgent than others.In this paper, we show that we can improve the compilationstrategy without altering the high-level semantics.With this new compilation strategy, we give the programmermore control over responsiveness without taking awaythe ability to reason about programs at a high level. Theprogrammer controls responsiveness by declaring prioritiesfor events, and the compilation strategy produces code thatuses preemption to enforce these priorities. We show thatthe compilation strategy enjoys the same properties as theoriginal strategy, with the only change being that the programmerreasons modulo permutations on the order of eventarrivals.
23.	Kiselyov, Oleg, et al. (författare) A Methodology for Generating Veriﬁed Combinatorial Circuits 2004 Ingår i: EMSOFT '04. - New York, NY : ACM Press. - 1581138601 ; , s. 249-258 Konferensbidrag (refereegranskat)abstract High-level programming languages offer significant expressivity but provide little or no guarantees about resource use. Resource-bounded languages --- such as hardware-description languages --- provide strong guarantees about the runtime behavior of computations but often lack mechanisms that allow programmers to write more structured, modular, and reusable programs. To overcome this basic tension in language design, recent work advocated the use of Resource-aware Programming (RAP) languages, which take into account the natural distinction between the development platform and the deployment platform for resource-constrained software.This paper investigates the use of RAP languages for the generation of combinatorial circuits. The key challenge that we encounter is that the RAP approach does not safely admit a mechanism to express a posteriori (post-generation) optimizations. The paper proposes and studies the use of abstract interpretation to overcome this problem. The approach is illustrated using an in-depth analysis of the Fast Fourier Transform (FFT). The generated computations are comparable to those generated by FFTW.
24.	Kiselyov, Oleg, et al. (författare) Relating FFTW and Split-Radix 2004 Ingår i: Embedded Software and Systems. - Berlin : Springer Berlin/Heidelberg. - 9783540281283 - 9783540318231 ; , s. 488-493 Konferensbidrag (refereegranskat)abstract Recent work showed that staging and abstract interpretation can be used to derive correct families of combinatorial circuits, and illustrated this technique with an in-depth analysis of the Fast Fourier Transform (FFT) for sizes 2n. While the quality of the generated code was promising, it used more floating-point operations than the well-known FFTW codelets and split-radix algorithm. This paper shows that staging and abstract interpretation can in fact be used to produce circuits with the same number of floating-point operations as each of split-radix and FFTW. In addition, choosing between two standard implementations of complex multiplication produces results that match each of the two algorithms. Thus, we provide a constructive method for deriving the two distinct algorithms. © Springer-Verlag Berlin Heidelberg 2005.
25.	Lengauer, Christian, et al. (författare) Preface 2006 Ingår i: Science of Computer Programming. - Amsterdam : Elsevier. - 0167-6423 .- 1872-7964. ; 62:1, s. 1-2 Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
26.	Moggi, Eugenio, et al. (författare) An Idealized MetaML : Simpler, and More Expressive 1999 Ingår i: Programming Languages and Systems. - Berlin : Springer Berlin/Heidelberg. - 3540656995 ; , s. 193-207 Konferensbidrag (refereegranskat)abstract MetaML is a multi-stage functional programming language featuring three constructs that can be viewed as statically-typed refinements of the back-quote, comma, and eval of Scheme. Thus it provides special support for writing code generators and serves as a semanticallysound basis for systems involving multiple interdependent computational stages. In previous work, we reported on an implementation of MetaML, and on a reduction semantics and type-system for MetaML. In this paper, we present An Idealized MetaML (AIM) that is the result of our study of a categorical model for MetaML. An important outstanding problem is finding a type system that provides the user with a means for manipulating both open and closed code. This problem has eluded efforts by us and other researchers for over three years. AIM solves the issue by providing two type constructors, one classifies closed code and the other open code, and exploiting the way they interact. We point out that AIM can be verbose, and outline a possible remedy relating to the strictness of the closed code type. © Springer International Publishing AG, Part of Springer Science+Business Media 1999
27.	Moggi, E., et al. (författare) Safe & robust reachability analysis of hybrid systems 2018 Ingår i: Theoretical Computer Science. - Amsterdam : Elsevier. - 0304-3975 .- 1879-2294. ; 747, s. 75-99 Tidskriftsartikel (refereegranskat)abstract Hybrid systems—more precisely, their mathematical models—can exhibit behaviors, like Zeno behaviors, that are absent in purely discrete or purely continuous systems. First, we observe that, in this context, the usual definition of reachability—namely, the reflexive and transitive closure of a transition relation—can be unsafe, i.e., it may compute a proper subset of the set of states reachable in finite time from a set of initial states. Therefore, we propose safe reachability, which always computes a superset of the set of reachable states. Second, in safety analysis of hybrid and continuous systems, it is important to ensure that a reachability analysis is also robust w.r.t. small perturbations to the set of initial states and to the system itself, since discrepancies between a system and its mathematical models are unavoidable. We show that, under certain conditions, the best Scott continuous approximation of an analysis A is also its best robust approximation. Finally, we exemplify the gap between the set of reachable states and the supersets computed by safe reachability and its best robust approximation. © 2018 The Authors
28.	Ostrovsky, Karol, 1975, et al. (författare) Towards a Primitive Higher Order Calculus of Broadcasting Systems 2002 Ingår i: PPDP '02. - New York, NY : ACM Press. - 1581135289 ; , s. 2-13 Konferensbidrag (refereegranskat)abstract Ethernet-style broadcast is a pervasive style of computer communication. In this style, the medium is a single nameless channel. Previous work on modelling such systems proposed a first order process calculus called CBS. In this paper, we propose a fundamentally different calculus called HOBS. Compared to CBS, HOBS 1) is higher order rather than first order, 2) supports dynamic subsystem encapsulation rather than static, and 3) does not require an "underlying language" to be Turing-complete. Moving to a higher order calculus is key to increasing the expressivity of the primitive calculus and alleviating the need for an underlying language. The move, however, raises the need for significantly more machinery to establish the basic properties of the new calculus. This paper develops the basic theory for HOBS and presents two example programs that illustrate programming in this language. The key technical underpinning is an adaptation of Howe's method to HOBS to prove that bisimulation is a congruence. From this result, HOBS is shown to embed the lazy λ-calculus.
29.	Pašalić, Emir, et al. (författare) Tagless Staged Interpreters for Typed Languages 2002 Ingår i: ICFP '02. - New York, NY : ACM Press. - 1581134878 ; , s. 218-229 Konferensbidrag (refereegranskat)abstract Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an untyped setting, staging an interpreter "removes a complete layer of interpretive overhead", just like partial evaluation. In a typed setting however, Hindley-Milner type systems do not allow us to exploit typing information in the language being interpreted. In practice, this can mean a slowdown cost by a factor of three or more. Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experience with the issues that arise in writing such an interpreter and in designing such a language. To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (called Meta-D) and prove its type safety. To formalize Meta-D, we extend Shao, Saha, Trifonov and Papaspyrou's λH language to a multilevel setting. Building on λH allows us to demonstrate type safety in a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work needed for establishing the soundness of that system.
30.	Semantics, applications, and implementation of program generation : second international workshop, SAIG 2001, Florence, Italy, September 6, 2001 00 : proceedings 2001 Proceedings (redaktörskap) (övrigt vetenskapligt/konstnärligt)abstract This book constitutes the refereed proceedings of the Second International Workshop on Semantics, Applications, and Implementation of Program Generation, SAIG 2001, held in Florence, Italy in September 2001. The seven revised full papers and two position papers presented together with an invited survey paper and two abstracts of invited talks were carefully reviewed and selected for inclusion in the book. Among the topics covered are generative programming, meta-programming, aspect-oriented programming, transition compression, goal-directed evaluation, partial evaluation, functional programming, meta-computation, and program optimization.
31.	Semantics, Applications and Implementation of Program Generation : International Workshop, SAIG 2000 Montreal, Canada, September 20, 2000 Proceedings 2000 Proceedings (redaktörskap) (övrigt vetenskapligt/konstnärligt)abstract This book constitutes the refereed proceedings of the International Workshop on Semantics Applications, and Implementation of Program Generation, SAIG 2000, held in Montreal, Canada in September 2000. The seven revised full papers and four position papers presented together with four invited abstracts were carefully reviewed and selected from 20 submissions. Among the topics addressed are multi-stage programming languages, compilation of domain-specific languages and module systems, program transformation, low-level program generation, formal specification, termination analysis, and type-based analysis. ©Springer
32.	Siek, Jeremy, et al. (författare) A Semantic Analysis of C++ Templates 2006 Ingår i: ECOOP 2006 - Object-Oriented Programming. - Heidelberg : Springer. - 3540357262 - 9783540357261 ; , s. 304-327 Konferensbidrag (refereegranskat)abstract Templates are a powerful but poorly understood feature ofthe C++ language. Their syntax resembles the parameterized classes ofother languages (e.g., of Java). But because C++ supports template specialization, their semantics is quite diﬀerent from that of parameterizedclasses. Template specialization provides a Turing-complete sub-languagewithin C++ that executes at compile-time. Programmers put this powerto many uses. For example, templates are a popular tool for writingprogram generators.The C++ Standard deﬁnes the semantics of templates using natural language, so it is prone to misinterpretation. The meta-theoretic propertiesof C++ templates have not been studied, so the semantics of templateshas not been systematically checked for errors. In this paper we presentthe ﬁrst formal account of C++ templates including some of the morecomplex aspects, such as template partial specialization. We validate oursemantics by proving type safety and verify the proof with the Isabelleproof assistant. Our formalization reveals two interesting issues in theC++ Standard: the ﬁrst is a problem with member instantiation and thesecond concerns the generation of unnecessary template specializations.
33.	Siek, Jeremy, et al. (författare) Exploring the Design Space of Higher-Order Casts 2009 Ingår i: Programming languages and systems. - Berlin : Springer Berlin/Heidelberg. - 9783642005893 ; , s. 17-31 Konferensbidrag (refereegranskat)abstract This paper explores the surprisingly rich design space for the simplytyped lambda calculus with casts and a dynamic type. Such a calculus is the targetintermediate language of the gradually typed lambda calculus but it is alsointeresting in its own right. In light of diverse requirements for casts, we developa modular semantic framework, based on Henglein’s Coercion Calculus, that instantiatesa number of space-efficient, blame-tracking calculi, varying in whaterrors they detect and how they assign blame. Several of the resulting calculi extendwork from the literature with either blame tracking or space efficiency, andin doing so reveal previously unknown connections. Furthermore, we introduce anew strategy for assigning blame under which casts that respect traditional subtypingare statically guaranteed to never fail. One particularly appealing outcomeof this work is a novel cast calculus that is well-suited to gradual typing.
34.	Siek, Jeremy, et al. (författare) Gradual Typing for Functional Languages 2007 Konferensbidrag (refereegranskat)abstract Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed a gradual type system for a functional calculus named $\lambda^?_\to$. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops $\mathbf{Ob}^{?}_{<:}$, a gradual type system for object-based languages, extending the Ob < : calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.
35.	Siek, Jeremy, et al. (författare) Gradual typing for objects 2007 Ingår i: ECOOP 2007 – Object-Oriented Programming. - Berlin : Springer Berlin/Heidelberg. - 9783540735885 - 9783540735892 ; , s. 2-27 Konferensbidrag (refereegranskat)abstract Static and dynamic type systems have well-known strengthsand weaknesses. In previous work we developed a gradual type system fora functional calculus named λ?→. Gradual typing provides the beneﬁts ofboth static and dynamic checking in a single language by allowing theprogrammer to control whether a portion of the program is type checkedat compile-time or run-time by adding or removing type annotations onvariables. Several object-oriented scripting languages are preparing toadd static checking. To support that work this paper develops Ob?<:,a gradual type system for object-based languages, extending the Ob<:calculus of Abadi and Cardelli. Our primary contribution is to show thatgradual typing and subtyping are orthogonal and can be combined in aprincipled fashion. We also develop a small-step semantics, provide amachine-checked proof of type safety, and improve the space eﬃciencyof higher-order casts.
36.	Swadi, Kedar, et al. (författare) A Monadic Approach for Avoiding Code Duplication when Staging Memoized Functions 2006 Ingår i: PEPM '06 Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. - New York, NY : ACM Press. - 1595931961 - 9781595931962 ; , s. 160-169 Konferensbidrag (refereegranskat)abstract Building program generators that do not duplicate generated code can be challenging. At the same time, code duplication can easily increase both generation time and runtime of generated programs by an exponential factor. We identify an instance of this problem that can arise when memoized functions are staged. Without addressing this problem, it would be impossible to effectively stage dynamic programming algorithms. Intuitively, direct staging undoesthe effect of memoization. To solve this problem once and for all, and for any function that uses memoization, we propose a staged monadic combinator library. Experimental results confirm that the library works as expected. Preliminary results also indicate that the library is useful even when memoization is not used.
37.	Taha, Walid, 1971-, et al. (författare) A Core Language for Executable Models of Cyber Physical Systems : work in progress report 2011 Konferensbidrag (refereegranskat)abstract Recently we showed that an expressive class of mathemat-ical equations can be automatically translated into simula-tion codes. Focusing on the expressivity of equations oncontinuous functions, this work considered only minimal in-teraction with discrete behaviors and only a static numberof statically connected components. However, the interac-tion between continuous and hybrid components in manycyber physical domains is highly coupled, and such systemsare often highly dynamic in both respects. This paper givesan overview of a proposed core language for capturing ex-ecutable hybrid models of highly dynamic cyber physicalsystems.
38.	Taha, Walid, 1971-, et al. (författare) A Core Language for Executable Models of Cyber-Physical Systems (Preliminary Report) 2012 Konferensbidrag (refereegranskat)abstract Recently we showed that an expressive class of mathematical equations can be automatically translated into simulation codes. By focusing on the expressivity of equations formed from continuous functions, this work did not accommodate a wide range of discrete behaviors or a dynamic collection of components. However, the interaction between continuous and hybrid components in many cyber-physical domains is highly coupled, and such systems are often highly dynamic in both respects. This paper gives an overview of a proposed core language for capturing executable hybrid models of highly dynamic cyber-physical systems. © 2012 IEEE.
39.	Taha, Walid, 1971- (författare) A Gentle Introduction to Multi-stage Programming, Part II 2008 Ingår i: Generative and Transformational Techniques in Software Engineering II. - Berlin : Springer Berlin/Heidelberg. - 9783540886426 - 3540886427 ; , s. 260-290 Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract As domain-specific languages (DSLs) permeate into mainstream software engineering, there is a need for economic methods for implementing languages. Following up on a paper with a similar title, this paper focuses on dynamically typed languages, covering issues ranging from parsing to defining and staging an interpreter for an interesting subset of Dr. Scheme. Preliminary experimental results indicate that the speedups reported in previous work for smaller languages and with smaller benchmarks are maintained. © 2008 Springer Berlin Heidelberg.
40.	Taha, Walid, 1971-, et al. (författare) A New Approach to Data Mining for Software Design 2004 Ingår i: Proceedings of the International Conference on Computer Science, Software Engineering, Information Technology, e-Business, and Applications (CSITeA-04). Konferensbidrag (refereegranskat)abstract We propose Exact Software Design Mining (ESDM) as a new approach to managing large software systems. ESDM is concerned with automatically extracting a program generator capable of exactly reconstructing the full code base. To illustrate the potential effectiveness of this approach, we propose, implement, and test a basic algorithm extracting such generators. Experimental results on various benchmarks (including the Linux kernel) are encouraging.
41.	Taha, Walid, 1971- (författare) A Sound Reduction Semantics for Untyped CBN Multi-Stage Computation : Or, the Theory of MetaML is Non-trivial (Extended Abstract) 2000 Ingår i: PEPM '00. - New York, NY : ACM Press. - 1581132018 ; , s. 34-43 Konferensbidrag (refereegranskat)abstract A multi-stage computation is one involving more than one stage of execution. MetaML is a language for programming multi-stage computations. Previous studies presented big-step semantics, categorical semantics, and sound type systems for MetaML. In this paper, we report on a confluent and sound reduction semantics for untyped call-by name (CBN) MetaML. The reduction semantics can be used to formally justify some optimization performed by a CBN MetaML implementation. The reduction semantics demonstrates that non-trivial equalities hold for object-code, even in the untyped setting. The paper also emphasizes that adding intensional analysis (that is, taking-apart object programs) to MetaML remains an interesting open problem. © 2000 ACM, Inc.
42.	Taha, Walid, 1971-, et al. (författare) Accurate Programming : Thinking about programs in terms of properties 2011 Ingår i: Proceedings IFIP Working Conference on Domain-Specific Languages. - : Open Publishing Association. ; , s. 236-260 Konferensbidrag (refereegranskat)abstract Accurate programming is a practical approach to producing high quality programs. It combines ideas from test-automation, test-driven development, agile programming, and other state of the art software development methods. In addition to building on approaches that have proven effective in practice, it emphasizes concepts that help programmers sharpen their understanding of both the problems they are solving and the solutions they come up with. This is achieved by encouraging programmers to think about programs in terms of properties.
43.	Taha, Walid, 1971-, et al. (författare) Developing a first course on cyber-physical systems 2016 Ingår i: ACM SIGBED Review. - New York, NY : Association for Computing Machinery (ACM). - 1551-3688. ; 14:1, s. 44-52 Tidskriftsartikel (refereegranskat)abstract Effective and creative Cyber-Physical Systems (CPS) development requires expertise in disparate fields that have traditionally been taught in several distinct disciplines. At the same time, students seeking a CPS education generally come from diverse educational backgrounds. In this paper, we report on our recent experience of developing and teaching a course on CPS. The course addresses the following three questions: What are the core elements of CPS? How should these core concepts be integrated in the CPS design process? What types of modeling tools can assist in the design of Cyber-Physical Systems? Our experience with the first four offerings of the course has been positive overall. We also discuss the lessons we learned from some issues that were not handled well. All material including lecture notes and software used for the course are openly available online.
44.	Taha, Walid, 1971-, et al. (författare) Directions in Functional Programming for Real(-Time) Applications 2001 Ingår i: Embedded software. - Berlin : Springer Berlin/Heidelberg. - 3540426736 - 9783540426738 ; , s. 185-203 Konferensbidrag (refereegranskat)abstract We review the basics of functional programming, and give a brief introduction to emerging techniques and approaches relevant to building real-time software. In doingso we attempt to explain the relevance of functional programming concepts to the real-time applications domain. In particular, we address the use of types to classify properties of real-time computations.
45.	Taha, Walid, 1971- (författare) Domain-Speciﬁc Languages 2008 Ingår i: The 2008 International Conference on Computer Engineering & Systems (ICCES '08). - Piscataway, NJ : IEEE Press. - 9781424421152 - 9781424421169 ; , s. XXV-XXVIII Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract Recently, there has been a growing interest in what have come to be known as domain-specific languages (DSLs). This paper introduces a definition for DSLs, explains how DSLs can have a far-reaching impact on our lives, and discusses why DSLs are here to stay. © 2008 IEEE.
46.	Taha, Walid, 1971-, et al. (författare) Environment Classiﬁers 2003 Ingår i: POPL '03. - New York, NY : ACM Press. - 1581136285 ; , s. 26-37 Konferensbidrag (refereegranskat)abstract This paper proposes and develops the basic theory for a new approach to typing multi-stage languages based a notion of environment classifiers. This approach involves explicit but lightweight tracking - at type-checking time - of the origination environment for future-stage computations. Classification is less restrictive than the previously proposed notions of closedness, and allows for both a more expressive typing of the "run" construct and for a unifying account of typed multi-stage programming. The proposed approach to typing requires making cross-stage persistence (CSP) explicit in the language. At the same time, it offers concrete new insights into the notion of levels and in turn into CSP itself. Type safety is established in the simply-typed setting. As a first step toward introducing classifiers to the Hindley-Milner setting, we propose an approach to integrating the two, and prove type preservation in this setting.
47.	Taha, Walid, 1971-, et al. (författare) Generating Heap-bounded Programs in a Functional Setting 2003 Ingår i: Embedded Software. - Berlin : Springer Berlin/Heidelberg. - 9783540202233 - 9783540452126 ; , s. 340-355 Konferensbidrag (refereegranskat)abstract High-level programming languages offer significant expressivity but provide little or no guarantees about resource utilization. Resource-bounded languages provide strong guarantees about the runtime behavior of programs but often lack mechanisms that allow programmers to write more structured, modular, and reusable programs. To overcome this basic tension in language design, this paper advocates taking into account the natural distinction between the development platform and the deployment platform for resource-sensitive software.To illustrate this approach, we develop the meta-theory for GeHB, a two-level language in which first stage computations can involve arbitrary resource consumption, but the second stage can only involve functional programs that do not require new heap allocations. As an example of a such a second-stage language we use the recently proposed first-order functional language LFPL. LFPL can be compiled directly to malloc-free, imperative C code. We show that all generated programs in GeHB can be transformed into well-typed LFPL programs, thus ensuring that the results established for LFPL are directly applicable to GeHB. © Springer-Verlag Berlin Heidelberg 2003.
48.	Taha, Walid, 1971-, et al. (författare) MetaML and multi-stage programming with explicit annotations 2000 Ingår i: Theoretical Computer Science. - Amsterdam : Elsevier. - 0304-3975 .- 1879-2294. ; 248:1-2, s. 211-242 Tidskriftsartikel (refereegranskat)abstract We introduce MetaML, a practically motivated, statically typed multi-stage programming language. MetaML is a “real” language. We have built an implementation and used it to solve multi-stage problems. MetaML allows the programmer to construct, combine, and execute code fragments in a type-safe manner. Code fragments can contain free variables, but they obey the static-scoping principle. MetaML performs type-checking for all stages once and for all before the execution of the first stage. Certain anomalies with our first MetaML implementation led us to formalize an illustrative subset of the MetaML implementation. We present both a big-step semantics and type system for this subset, and prove the type system's soundness with respect to a big-step semantics. From a software engineering point of view, this means that generators written in the MetaML subset never generate unsafe programs. A type system and semantics for full MetaML is still ongoing work. We argue that multi-stage languages are useful as programming languages in their own right, that they supply a sound basis for high-level program generation technology, and that they should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. To illustrate this we provide a simple three-stage example elaborating a number of practical issues. The design of MetaML was based on two main principles that we identified as fundamental for high-level program generation, namely, cross-stage persistence and cross-stage safety. We present these principles, explain the technical problems they give rise to, and how we address with these problems in our implementation.
49.	Taha, Walid, 1971-, et al. (författare) Multi-Stage Programming : Axiomatization and Type-Safety 1998 Ingår i: Automata, Languages and Programming. - Berlin : Springer Berlin/Heidelberg. - 9783540647812 - 9783540686811 ; , s. 918-929 Konferensbidrag (refereegranskat)abstract Multi-stage programming provides a new paradigm for constructing efficient solutions to complex problems. Techniques such as program generation, multi-level partial evaluation, and run-time code generation respond to the need for general purpose solutions which do not pay run-time interpretive overheads. This paper provides a foundation for the formal analysis of one such system.We introduce a multi-stage language and present its axiomatic and reduction semantics. Our axiomatic semantics is an extension of the call-by-value λ-calculus with staging constructs. We show that staged-languages can “go Wrong” in new ways, and devise a type system that screens out such programs. Finally, we present a proof of the soundness of this type system with respect to the reduction semantics. © Springer 1998
50.	Taha, Walid, 1971- (författare) Multi-Stage Programming : Its Theory and Applications 1999 Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract MetaML is a statically typed functional programming language with special support for programgeneration. In addition to providing the standard features of contemporary programminglanguages such as Standard ML, MetaML provides three staging annotations. These staging annotationsallow the construction, combination, and execution of object-programs.Our thesis is that MetaML's three staging annotations provide a useful, theoretically soundbasis for building program generators. This dissertation reports on our study of MetaML's stagingconstructs, their use, their implementation, and their formal semantics. Our results include anextended example of where MetaML allows us to produce ecient programs, an explanation ofwhy implementing these constructs in traditional ways can be challenging, two formulations ofMetaML's semantics, a type system for MetaML, and a proposal for extending MetaML with atype construct for closedness.The dissertation consolidates a number of previous publications by the author, includingMetaML's type systems and big-step semantics. The presentation is new. The proposed solutionto an implementation problem and the reduction semantics for MetaML's three staging constructsare also new.

Skapa referenser, mejla, bekava och länka

Länka till träfflistan

Träfflista för sökning "WFRF:(Taha Walid 1971 ) "

Avgränsa träffmängd

År