  We present a generic framework that facilitates object level reasoning with
logics that are encoded within the Higher Order Logic theorem proving
environment of HOL Light. This involves proving statements in any logic using
intuitive forward and backward chaining in a sequent calculus style. It is made
possible by automated machinery that take care of the necessary structural
reasoning and term matching automatically. Our framework can also handle type
theoretic correspondences of proofs, effectively allowing the type checking and
construction of computational processes via proof. We demonstrate our
implementation using a simple propositional logic and its Curry-Howard
correspondence to the lambda-calculus, and argue its use with linear logic and
its various correspondences to session types.
