Find out more about rewriting theory and its applications

The first International School of Rewriting , or ISR, took place in Nancy in 2006. Coordinated by the International Federation for Information Processing (IFIP), this summer school has since been hosted by various different countries in Europe and Latin America. The school will finally be returning to France in 2019, coming to Paris thanks to the work of Olivier Hermant (MINES ParisTech) and Frédéric Blanqui (Inria Deducteam, a joint undertaking with the Laboratoire Spécification et Vérification - LSV- and ENS Paris-Saclay). Highly familiar with the field, these two individuals shared logistics, funding and programme building tasks between them in order to offer a 2019 programme full of new additions.

What is the ISR?

The ISR is a short, week-long training course covering rewriting theory , a computational model that is particularly important for programming or theorem proving . By replacing the terms of an expression in accordance with predetermined transformation rules, rewriting can be used to reformulate a problem until a solution can be found. We are all familiar with this type of approach when it is used in relation to simple algebraic expressions, (a+b)²= a²+2ab+b² for example, but rewriting is applicable to all types of mathematical objects, meaning it has applications in a range of different fields , from organic chemistry to the rail transport industry, right through to software verification.

For the 2019 edition of the ISR, the programme has been extended by one day. Although targeted primarily at doctoral students, the course is also open to masters students, who this year will have access to a preferential tariff. Any researchers - whether young or experienced - who may be curious about the applications to be presented will also be more than welcome.

 

The two-track system means the training course can be split up over two years.

 

 

Frédéric Blanqui.

Two tracks to choose from

Following the school's standard format, the fifty or so participants expected to attend in Paris will be offered two different tracks:

• Are you a beginner? The basic track is the track for you, and indeed for anyone looking to learn the fundamentals of rewriting . Three contributors will alternate between lessons and exercises in order to introduce you to the basic techniques of this system. Any students who may have ECTS credits to validate can choose to sit an optional exam at the end of the week. As a new addition for this year, a day and a half will be set aside for λ-calculus, which is used by programming languages.
• Are you already familiar with rewriting? The “advanced” track will give you the opportunity to expand your knowledge and to discover new applications . Comprised of twelve sessions each lasting 1h30, the aim of the programme is to introduce theoretical and practical approaches, in addition to case studies.

The following are some of the main themes selected by Olivier Hermant and Frédéric Blanqui for the renewal of this advanced course:

• molecular interaction modelling
• representations of quantum processes
• Musicology applications through IT and rhythm transcription.

Sign up before 17th May to get a 20% discount.

Deducteam team

• Foundation of the team : in 2013, Frédéric Blanqui joined Gilles Dowek, Inria's research director, who was conducting exploratory work on the verification of formal evidence.
• Location: Inria Saclay research centre - Île-de-France since 1 January 2016
• Research topic : Deducteam works in the world of formal evidence and verification. The objective is to develop a standard to be able to verify unambiguously the correction of a mathematical program or theorem. In particular in the railway and aeronautical fields, where error-free software is an essential prerequisite for ensuring the safety and security of these critical applications.
• Main achievement : Dedukti, a tool with a simple and modular architecture, which seeks to reproduce in the field of proof what assembler software does in programming: solve interoperability problems between different proof systems to allow these various languages to be combined with each other.
• Ongoing project : Logipedia, a project that aims to translate the libraries of formal evidence developed by different teams into a European e-infrastructure. The launch meeting was held at the end of January 2019, at the Specification and Verification Laboratory (LSV) in Inria.