[antlr-interest] Determine / check validity of type

[Mark Wright]

Hi Martin,

The type system in the example you described can be modelled with
the Simply Typed Lambda Calculus, which is described in detail in
the standard text on type systems "Types and Programming Languages"
by Benjamin Pierce.  It assumes knowledge of logic, set theory,
relations and proof by induction.  The text I recommend for the necessary
mathematical background is "The Haskell Road to Logic, Maths and
Programming" by Doets and Eijck.  Although it mentions a programming
language in the title, this is primarilly a maths text.  The occassional
programming language examples help to reinforce understanding of the
maths.

Regards, Mark