In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical treatments of type inference". Jones provided inference and checking algorithms for this syntactic construct, but it's typing rule is not referenced.
As far I know, binding groups is quite differente from usual let bindings. You can have mutual recursion, for example. Also, I don't know if is possible to simulate binding groups only using let expressions.
There is a typing rule for typing binding groups anywhere in the literature? If there is, then maybe the rest of this question is pointless.
This paper also doesn't give us a (in)formal grammar for the syntax, because it's goal is type inference/checking from the data stucture itself. I don't think this is strictly necessary, but a syntactic definition of binding groups may help defining a typing rule. So, I decided to give a sugestion of what this informal grammar may look like. Brackets means finite sequence and curly bracket means no-empty finite sequence.
So, what I'm asking here is a rule for typing binding groups.
It seems that my question is not clear enough. I apologize for that. I'll try to make it more clear...
By typing rule (or type rule) I mean: en.wikipedia.org/wiki/Type_rule and by type checking algorithm I mean something easy to translate to code. I think the difference is more fundamental than just representation style. A rule is closer to a relation and an algorithm is closer to a function. What is missing is a rule, like in the wikipedia page, that could be used for certification of the algorithm.
Certification is the motivation behind my question. I want to certify the algorithms described in this paper.