Time: 1:00 - 2:00pm Venue: QMUL campus - ITL top floor
Julian Nagele who just joined our group from the University of Innsbruck and we are delighted that he will be speaking at this seminar.
Rewriting is a simple yet Turing complete model of computation. It is the process of transforming objects in a step-wise fashion, replacing equals by equals. Typically the objects are expressions in some formal language, and the transformations are given by a set of directed equations.A fundamental notion in rewriting is confluence, which guarantees uniqueness of results, i.e., that the set of equations in question specifies a partial function. Generalising confluence to multiple sets of equations yields the related notion of commutation, which can be used to study correctness of program transformations.Although undecidable in general, much work has been spent on confluence analysis, with automatic tools under active development. The achievements in confluence research have enabled the annual confluence competition where these tools try to establish/refute confluence.In this talk I will provide an overview of automated confluence analysis of rewriting, discussing key concepts in the underlying theory, and the current state of tool support.
More information on seminars and events in the Theory research group