Program

The program includes invited and contributed talks. The related extended abstracts can be found in the electronic informal proceedings.

(Tentative) Schedule:

09:00 – 10:00 Session 1 (Invited Talk). Chair: Veena Ravishankar/Christophe Ringeissen

10:00 – 10:30 Coffee Break

10:30 – 12:30 Session 2. Chair: David Cerna

12:30 – 14:00 Lunch Break

14:00 – 15:30 Session 3. Chair: Andrew Marshall

15:30 – 16:00 Coffee Break

16:00 – 17:00 Session 4 (Invited Talk). Chair: Temur Kutsia

17:00 – 18:00 Session 5. Chair: Daniele Nantes-Sobrinho

  • (17:00) Andrés Felipe González Barragán, David Cerna, Mauricio Ayala-Rincón and Temur Kutsia. On Anti-unification in Absorption Theories (slides)
  • (17:30) Andrew Pulver. The conjugacy problem and the uniform common term problem in dwindling string rewriting systems. Abstract: In this paper we investigate the conjugacy problem and the uniform common term problem in the context of “dwindling” string rewriting systems. The conjugacy problem is shown to be solvable in polynomial time, and the uniform common term problem is shown to be undecidable. Several basic properties of dwindling string rewriting systems are demonstrated (extended abstract to appear in the informal proceedings).

Invited Talks:

  • Mauricio Ayala-Rincón (Universidade de Brasília). Formalisation of Nominal Equational Reasoning. Abstract: In contrast to other methods to bind variables, the nominal approach uses atoms and the algebra of atom permutations bringing enlightening implications. This talk will discuss the lessons learned from our experience towards formalising nominal matching and nominal unification modulo C and AC using the proof assistant PVS (Prototype Verification System). Furthermore, the talk will dissect exciting issues that appear during the formalisation of nominal equational reasoning giving rise to surprises regarding the well-known properties of first-order unification and unification modulo C and AC.
  • Deepak Kapur (UNM, Albuquerque). Invariant Generation as Semantic Unification: A New Perspective. Abstract: Unification is the problem of finding instantiations of variables in a finite set of equations constructed using function symbols such that both sides of the instantiated equations are equal. In semantic unification, also called E-unification, function symbols can have properties specified typically by an equational theory; a unifier then makes the two instantiated sides of each equation, equivalent modulo the equation theory. By generalizing the unification problem to a first-order theory in which variables in the problem stand for formulas in the theory, the invariant generation problem in software, hardware, and cyber-physical system can be formulated as a unification problem. Finding a nontrivial unifier in this case amounts to finding an invariant which is a formula in the theory. Similarly, finding a most general unifier in that theory amounts to finding the strongest invariant. Instantiation of variables can be further restricted to formulas with certain shapes/properties. A number of examples from the literature of the automatic generation of loop invariants in software will be used to illustrate this new perspective.

Accepted Contributions:

  • João Barbosa, Mário Florido and Vitor Santos-Costa. Typed Unification: when failure may not be wrong
  • Aleksy Schubert. Second-order unification and functional arity
  • Stéphane P. Desarzens. One-Variable Unification in K
  • Sam van Gool and Johannes Marti. Modal unification step by step
  • Andrés Felipe González Barragán, David Cerna, Mauricio Ayala-Rincón and Temur Kutsia. On Anti-unification in Absorption Theories
  • Wei Du, Paliath Narendran and Michael Rusinowitch. Inferring RPO Symbol Ordering
  • Georg Ehling and Temur Kutsia. Matching in Quantitative Equational Theories
  • Nikolai Kudasov. Generalising Huet-style Projections in E-unification for Second-Order Abstract Syntax
  • Andrew Pulver. The conjugacy problem and the uniform common term problem in dwindling string rewriting systems

Comments are closed.