  We present an extension of System F with higher-order context-free session
types. The mixture of functional types with session types has proven to be a
challenge for type equivalence formalization: whereas functional type
equivalence is often rule-based, session type equivalence usually follows a
semantic approach based on bisimulations. We propose a unifying approach that
handles the equivalence of functional and session types together. We present
three notions of type equivalence: a syntactic rule-based version, a semantic
bisimulation-based version, and an algorithmic version by reduction to the
problem of bisimulation of simple grammars. We prove that the three notions
coincide and derive a decidability result for the type equivalence problem of
higher-order context-free session types.
