We present an ongoing implementation of a dependent-type the- ory (∆-framework) based on the Edinburgh Logical Framework LF, extended with Proof-functional logical connectives such as in- tersection, union, and strong (or minimal relevant) implication. Their combination opens up new possibilities of formal reasoning on proof-theoretic semantics. We provide some examples in the extended type theory and we outline a type checker. The theory of the system is under investigation. Once validated in vitro, the proof-functional type theory could be successfully plugged into existing truth-functional proof-systems.