> Automatically generating monoids such as the stack monoid from their corresponding simple sequential programs seems like an extremely promising area for research.

I was interested in this problem a while back and the papers I remembered being useful were:

"Automatic Inversion Generates Divide-and-Conquer Parallel Programs": https://core.ac.uk/download/pdf/192663016.pdf

which is based on "The Third Homomorphism Theorem": http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/th...

The motivating example is whether you can generate a mergesort (where the monoid is combine two sorted lists) given an implementation of an insertion sort (where the sequential program is inserting one element by one into a sorted list).

I remember being disappointed by the answer after reading these papers but in the citation graph there are a bunch of relatively recent program synthesis papers. Maybe there's something better now.