The language L over a fixed vocabulary K is an (applied) typed λ-calculus with additional constructs for acyclic recursion and attitudinal application, an extension of Montague’s Language of Intensional Logic LIL as formulated by Daniel Gallin. It is denotationally interpretable in the classical typed λ-calculus over K, but intensionally richer: in particular, it can define the referential intension of each term A, an abstract algorithm which computes the denotation of A and provides a plausible explication of its meaning.

The key mathematical construction of L is an effective reduction calculus which compiles each term A into an (essentially) unique canonical form cf(A), a denotational term which explicates the logical form of A and from which the referential intension of A can be read off. The central open problem about L (over a finite, interpreted vocabulary) is the decidability of global synonymy - and it is a problem about the classical, interpreted typed λ-calculus.