Certified normalization of generalized traces

Hendrik Maarand*, Tarmo Uustalu

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


Mazurkiewicz traces are a generalization of strings where an independence relation on the alphabet for commutability of letters induces an equivalence relation on strings. The equivalence relation can be made more expressive by allowing the commutability of two adjacent letters in a string to depend on their left context. We generalize two classical normal forms and the corresponding normalization algorithms for Mazurkiewicz traces for Sassone et al.’s context-dependent generalization of traces, formalize this development in the dependently typed programming language Agda, and show generalized traces in action on an example from relaxed shared-memory concurrency (local reads in TSO).

Original languageEnglish
Pages (from-to)253-265
JournalInnovations in Systems and Software Engineering
Issue number3-4
Early online date18 Jun 2019
Publication statusPublished - Sept 2019

Bibliographical note

Funding Information:
This work was supported by the ERDF funded Estonian national centre of excellence Project EXCITE (2014-2020.4.01.15-0018) and the Estonian Ministry of Education and Research institutional research Grant IUT33-13.

Publisher Copyright:
© 2019, Springer-Verlag London Ltd., part of Springer Nature.

Other keywords

  • concurrency
  • Mazurkiewicz traces
  • normal forms
  • relaxed memory


Dive into the research topics of 'Certified normalization of generalized traces'. Together they form a unique fingerprint.

Cite this