Li Wei

A Logical Framework for System revision
Abstract:
A logical inference system named R-calculus is defined to derive all maximal contractions of a base of belief set for its given refutations .The R-calculus consists of the structural rules an axiom , a cut rule, and the rules for logical connectives and quantifiers. Some examples are given to demonstrate how to use the R-calculus. Furthermore, the properties regarding reachability, soundness and completeness of the R-calculus are formally defined and proved.

Biographic information:
Wei Li is a professor in computer science and engineering at Beihang University since 1986 and he is the president of the university since 2002. He obtained his Bachelor degree in mathematics from Peking University and Ph.D in computer science from the University of Edinburgh. He is a Member of the Chinese Academy of Sciences since 1997 and the director of the State Key Laboratory of Software Development Environment since 1990. His research interests are the logical foundations of computer science and artificial intelligence, and currently the massive information system under the Internet. He has published more than 100 research papers with 85 of them in English.

Rachid Guerraoui

The Return of Transactions
Abstract:
Major chip manufacturers have recently shifted their focus from speeding individual processors to multiplying them on the same chip and shipping multicore architectures. Boosting the performance of programs will thus necessarily go through parallelizing them. This is not trivial and the average programmer will badly need abstractions for synchronizing concurrent accesses to the same memory. The transaction abstraction looks promising and there is a lot of interest around its use in modern parallel programming.The idea is quite old and has been explored for the last two decades by the research community. This talk will address the question whether the "old transaction idea" is exactly the same as the one that seems now to be conquering the world of parallel programming. The answer to the question might have a big impact on the distributed computing research community.

Biographic information:
Rachid Guerraoui is professor of computer science since 1999 at EPFL (Ecole Polytechnique Fédérale de Lausanne) where he leads the distributed programming laboratory. He has also been affiliated in the past with HP Labs in Palo Alto and MIT. He contributed to the ideas of indulgent algorithms and e-Transactions, and developed the first type based publish-subscribe system. He also co-authored a book on transactions and a book on reliable distributed programming.

Jifeng He

Transaction Calculus
Abstract:
Transaction-based services are increasingly being applied in solving many universal interoperability problems. Compensation is one of the typical features of long-running transactions. This talk presents a design matrix model for specifying behaviour of transactions and provides new healthiness conditions to capture the new programming features. The new model for handling failure and compensation is built as a conservative extension of the standard relational model in the sense that the algebraic laws presented in the UTP (Unifying Theories of Programming) remain valid. This talk also shows that transactions as an programming unit with multiple entry and exit ports are closed under the conventional programming combinators.

Biographic information:
HE Jifeng, Computer Software Specialist, now serves as Professor of Computer Science at East China Normal University, and is the Dean of the Software Engineering Institute as well as director of Shanghai Embedded Systems Institute. He gained the China National Nature Science Award in 2002 and was elected Academician of Chinese Academy of Sciences in 2005. Since 1980, Prof. He's research interests have been concentrated on the programming theories and their application. In company with C.A.R. Hoare, he suggested the concept of the program decomposition operator, and treated both the standard language and programmatic language as the same type of mathematic objects. Before long, he put forward the adoption of relational algebra as the unified mathematic model for the programs and software standards, so that the relational algebra is to be used to describe a program's process of dissolution or combination in a bid to support the development of new software. In the field of data refinement, he gave a complete method for treating the language of nondeterministic programs. Based on his success in integrating various theories of semantics and software development methodologies on many programming languages, he, in company with C.A.R. Hoare, proposed a unified theory and mathematic framework for linking several programming languages in 1995. Recently, he is working on high dependability of software systems.