Reversing Algebraic Process Calculi
Reversible computation has a growing number of promising application areas such as the modelling of biochemical systems, program debugging and testing, and even programming languages for quantum computing. We formulate a procedure for converting operators of standard algebraic process calculi such as CCS, ACP and CSP into reversible operators, while preserving their operational semantics. We define a forward-reverse bisimulation and prove that it is a congruence for all reversible operators.
This is joint work with Iain Phillips.
XQuery Around the Corner: Compilation and Optimization Techniques for Advanced XML Applications
As XQuery is reaching maturity, more complex applications are emerging that exploit the full expressiveness of the language and the flexibility of XML. This fuels competition between software vendors implementing XQuery, and the intense research activity on XML processing. In first part of this talk, I will draw a panorama of emerging advanced XQuery applications. In the second part of this talk I will present a complete architecture, algebra and novel optimization techniques designed to address the needs of those advanced applications. This work is based on our experience with developers using XQuery for complex XML applications, and in implementing the language in the Galax system.
This is joint work with Mary Fernandez, Christopher Re, and Philippe Michiels.
Systematic search for functional programs
This presentation is about a system for inductive synthesis of small functional programs by trial and error, or just by generating a stream of all the type-correct programs in a systematic and exhaustive manner and evaluating them. Although the main goal of this line of research is to ease functional programming, it also provides an axis to evaluate heuristic approaches to inductive program synthesis such as genetic programming, by investigating the best performance possible by exhaustive search algorithms.
Object Containment in Object-Z
In object systems, it is often the case that an object will have an attribute whose value identifies (points or refers to) some other object in the system so that the identified object can be sent messages. The association between objects determined by the object references in a system will generally result in a complex structure whose design and specification is a crucial part of the development and implementation of the system. We look at ways of capturing formally object reference structures that occur frequently in object systems. For example, consider a system consisting of car and wheel objects where each car has attributes referencing its wheel objects. If wheels are not shared between cars, distinct car objects will reference distinct wheel objects. We distinguish such object references by saying that a car object (directly) $contains$ the wheel objects it references. The nature of the contained object references as suggested by this example is captured within a formal framework and incorporated into the Object-Z specification language. Object containment is then compared with related ideas found in object-oriented programming languages. The distinction between object containment and the notion of object ownership (control) is also discussed. Finally, a generalised notion of object containment is investigated.
Stiff systems of ODEs and sparse matrix techniques
Sparse matrix techniques have played a prominent role in the solution algorithms for stiff systems of ODEs for many years. In this talk it is described how classical techniques for reordering sparse matrices into block-triangular matrices can be used to partition systems of ODEs into loosely coupled subsystems.
The objective of the partitioning is to permit the numerical integration of one time step to be performed as the solution of a sequence of small subsystems. This reduces the computational complexity compared to solving one large system and permits efficient parallel execution under appropriate conditions. The subsystems are integrated using methods based on low order backward differentiation formulas [1].
As an example is chosen the chemical reaction kinetics equations from air pollution models, since the solution of these equations is a substantial fraction of the total computational effort [2].
[1] S. Skelboe, Accuracy of decoupled implicit integration formulas, SIAM Journal on Scientific Computing, Volume 21, Number 6, 2000, pp. 2206-2224.
[2] S. Skelboe and Z. Zlatev, Exploiting the natural partitioning in the numerical solution of ODE systems arising in atmospheric chemistry, Springer Lecture Notes in Computer Science 1196 Springer 1997, Proceedings of the First Workshop on Numerical Analysis and Applications (WNNA-96), Rousse, Bulgaria, June 24-27, 1996.
Recursive Coalgebras from Comonads
The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this talk, we motivate the use of recursive coalgebras as a paradigm of structured recursion in programming semantics, list some basic facts about recursive coalgebras and give new conditions for the recursiveness of a coalgebra based on comonads, comonad-coalgebras and distributive laws of functors over comonads.
Software Verification for Object-Based Programs
Many software properties can be analysed through a relational size analysis on each functions inputs and outputs. Such relational analysis (through a form of dependent typing) has been successfully applied to declarative programs, and to restricted imperative programs; but it has been elusive for object-based programs. The main challenge is that objects may mutate and they may be aliased. In this paper, we show how safety policies of programs can be analysed by tracking size properties of objects and be enforced by objects invariants and the preconditions of methods. We propose several new ideas to allow both mutability and sharing of objects, whilst aiming for precision in our analysis. We introduce the concept of size-immutability to facilitate sharing, and also a set of alias controls to track unaliased objects whose size properties may change. We formalise our results through a set of advance type checking rules for an object-based imperative language. We re-affirm the utility of the proposed type system by showing how a variety of software properties can be automatically verified according to size-inspired safety policies.
Reference: Wei-Ngan Chin, Siau-Cheng Khoo, Shengchao Qin, Corneliu Popeea, Huu Hai Nguyen, Verifying Safety Policies with Size Properties and Alias Controls, in ICSE 2005, St Louis, May 2005.
Bi-directional Transformation language for XML
Many formats of the same purpose are defined with the growth of using XML. Their formats are mutually imcompatible generally. However, we want to use them seemlessly because they are for the same purpose. So, we propose the language that converts XML docuemnts bi-directionally. In this language, the corresponding part between the structures of the XML document is described as restriction conditions. This restriction condition is called 'relation'. The structure of XML document is shown by using the pattern used in XDuce. The corresponding relations between the structures are expressed by burying the variables in the patterns. And, we convert XML document to another format based on the relations.
About Systematic Parallelization
Region Inference for an Object Oriented Language
Region-based memory management offers several important potential advantages over garbage collection, including real-time performance, better data locality, and more efficient use of limited memory. Researchers have advocated the use of regions for functional, imperative, and object-oriented languages. Lexically scoped regions are now a core feature of the Real-Time Specification for Java. Recent research in region-based programming for Java has focused on region checking, which requires manual effort to augment the program with region annotations. In this paper, we propose an automatic region inference system for a core subset of Java. To provide an inference method that is both precise and practical, we support classes and methods that are region-polymorphic, with region-polymorphic recursion for methods. One challenging aspect is to ensure region safety in the presence of features such as class subtyping, method overriding, and downcast operations. Our region inference rules can handle these object-oriented features safely without creating dangling references.
Reference: Wei-Ngan Chin, Florin Craciun, Shengchao Qin, Martin Rinard, Region Inference for an Object-Oriented Language. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI04) , Washington DC, USA, June 2004.
The User Environment as an Active Document
In an "active document" relationships between parts of the document may be governed by constraints, which are dynamically maintained. When a user edits one part, another part may then be automatically updated. A typical, fairly complex example is an index section, automatically sorted on entries and with automatically adjusted references when an indexed term is moved to another place. It is generally accepted that this provides desirable functionality that can be generalized to cover many other meaningful uses.
It is less generally realized that, in fact, many applications, and perhaps the complete user's operating environment, can be modelled as active documents. This can be used as a design paradigm: applications designed this way tend to be easier to use. It can also be used as a specification paradigm, making application specifications simpler and easier to understand. Finally, it can also be used to generate applications, or even complete operating environments.
Back to ToPS's Home Page