[1][2] This approach has been used successfully for (interactive) automated theorem proving.
Several more recent proof tools like Isabelle are based on this idea.
[3] A logical framework is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus.
Syntax is treated in a style similar to, but more general than Per Martin-Löf's system of arities.
This is inspired by Per Martin-Löf's development of Kant's notion of judgement, in the 1983 Siena Lectures.
The methodology of judgements-as-types is that judgements are represented as the types of their proofs.
An implementation of the LF logical framework is provided by the Twelf system at Carnegie Mellon University.