Higher-order unification is a unification process that takes beta-reduction into account of value equality which is known to be undecidable due to its flexibility. Pattern unification is an incomplete but decidable variant of higher-order unification proposed by Miller at 1990. In this problem session we explore the possibilities of finding a “modernised” version of the algorithm that works better in the type system work we have nowadays as a formal system.