Catálogo de publicaciones - libros

For at least 25 years, the most effective way to retarget systems software has been by using machine descriptions. But “machine description” doesn’t mean what you think. A traditional machine description does contain information about the machine, but its utility is compromised in one of two ways:

Increasingly, we see a trend where programmeable processors are incorporated into a wide variety of everyday devices, ranging from “smart badges,” copy and fax machines, phones, and automobiles to traffic lights and wireless sensor networks. At the same time, the functionality expected of the software deployed on such processors becomes increasingly complex (e.g., general-purpose operating systems such as Linux on cell phones, intrusion-detection and related security security measures on wireless sensor devices). The increasing complexity of such software, and the reliability expected of them, suggest a plausible application of declarative languages. However, programs in declarative languages very often experience a significant increase in code size when they are compiled down to native code. This can be a problem in situations where the amount of memory available is limited. This talk discusses a number of different techniques for reducing the memory footprint of executables.

We present an application of functional programming in the domain of sound generation and processing. We use the lazy language Clean to define purely functional stream generators, filters and other processors, such as reverberators. Audio signals are represented (before the final output to arrays processed by the system primitives) as co-recursive lazy streams, and the processing algorithms have a strong dataflow taste. This formalism seems particularly appropriate to implement the ‘waveguide’, or ‘physically-oriented’ sound models. Lazy programming allocates the dynamical memory quite heavily, so we do not propose a real-time, industrial strength package, but rather a pedagogical library, offering natural, easy to understand coding tools. We believe that, thanks to their simplicity and clearness, such functional tools can be also taught to students interested in audio processing, but with a limited competence in programming.

An important property of strategies used to solve goals in functional logic programming (FLP) languages is the complete exploration of the solution space. Integrating constraints into FLP proved to be useful in many cases, as the resulting constraint functional logic programming (CFLP) offers more facilities and more efficient operational semantics. CFLP can be achieved by means of conditional rewrite systems with a narrowing-based operational semantics. A common idea to improve the efficiency of such operational semantics is to use specific algorithms from operations research as constraint solvers. If the algorithm does not return a complete set of solutions, the property of completeness might be lost. We present a real world timetabling problem illustrating this approach. We propose an algorithm, obtained as an integration of three known optimization algorithms for the linear assignment problem (LAP), enumerating solutions to the LAP in order of increasing weight, such that resolution of goals is complete again. We show, how the narrowing process can be tailored to use this algorithm and provide an efficient way to solve the timetable generation problem.

We describe the reconstruction of a phylogeny for a set of taxa, with a character-based cladistics approach, in a declarative knowledge representation formalism, and show how to use computational methods of answer set programming to generate conjectures about the evolution of the given taxa. We have applied this computational method in two domains: to historical analysis of languages, and to historical analysis of parasite-host systems. In particular, using this method, we have computed some plausible phylogenies for Chinese dialects, for Indo-European language groups, and for species. Some of these plausible phylogenies are different from the ones computed by other software. Using this method, we can easily describe domain specific information (e.g. temporal and geographical constraints), and thus prevent the reconstruction of some phylogenies that are not plausible.

In this paper we address the problem of encoding complex concurrency control in reconfigurable systems. Such systems can be often reconfigured, either statically, or dynamically, in order to adapt to new requirements and a changing environment. We therefore take a declarative approach and introduce a set of high-level programming abstractions which allow the programmer to easily express complex synchronization constraints in multithreaded programs. The constructs are based on our model of which assumes attaching roles to concurrent threads and expressing a synchronization policy between the roles. The model is illustrated by describing an experimental implementation of our language as a design pattern library in OCaml. Finally, we also sketch a small application of a web access server that we have implemented using the RBS design pattern.

The hybrid probabilistic programs framework [1] allows the user to explicitly encode both logical and statistical knowledge available about the dependency among the events in the program. In this paper, we extend the language of hybrid probabilistic programs by allowing to be associated with heads of clauses, and we modify its semantics to make it more suitable to encode real-world applications. The new semantics is a natural extension of standard logic programming semantics. The new semantics of hybrid probabilistic programs also subsumes the implication-based probabilistic approach proposed by Lakshmanan and Sadri [12]. We provide also a sound and complete algorithm to compute the least fixpoint of hybrid probabilistic programs with annotated atomic formulas as rule heads.

The need for direct memory manipulation through pointers is essential in many applications. However, it is also commonly understood that the use (or probably misuse) of pointers is often a rich source of program errors. Therefore, approaches that can effectively enforce safe use of pointers in programming are highly sought after. ATS is a programming language with a type system rooted in a recently developed framework , and a novel and desirable feature in ATS lies in its support for safe programming with pointers through a novel notion of . In particular, even pointer arithmetic is allowed in ATS and guaranteed to be safe by the type system of ATS. In this paper, we give an overview of this feature in ATS, presenting some interesting examples based on a prototype implementation of ATS to demonstrate the practicality of safe programming with pointer through stateful views.

Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we explore approaches to provably correct code generation based on programming language semantics, particularly , and partial evaluation. We show that the notation can be used for specifying both the syntax and semantics of imperative languages. We next show that continuation semantics can also be expressed in the Horn logical framework.

We present an optimizing compiler for the -calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the -calculus handles names by representing -calculus names in MMC as Prolog , with distinct names represented by distinct variables. Given a -calculus process , our compiler for MMC produces an extremely compact representation of ’s symbolic state space as a set of . It also uses AC unification to recognize states that are equivalent due to symmetry.