Grammatical Framework

Grammatical Framework is a type-theoretic grammar formalism based on Martin-Löf type theory. GF particularly addresses four aspects of grammars: multilinguality, semantics, modularity and grammar engineering, and reuse of grammars in different formats and as software components.

See http://www.grammaticalframework.org/