DPLs have formalized key notions such as assumption scope and eigenvariable scope in novel ways (most notably, without reducing them to variable scope in the typed lambda calculus, as is done in Curry-Howard systems via higher-order abstract syntax). In addition, type-omega DPLs have introduced a notion of teasing apart the syntax of computation and deduction in a way that allows the two to be integrated seamlessly and soundly. One of the main contribution of DPLs is the introduction of assumption-base semantics.
An assumption base is just a set of premises: a set of propositions that we take for granted for the purposes of a given stretch of logical discourse. This is traditionally known in logic as a "context," a notion that has been around for a while, particularly in connection with sequent systems, where the basic unit of inference is a pair consisting of a context and a conclusion. What is novel about DPLs is how assumption bases are used to give formal semantics to proofs: the idea that the formal meaning of a proof is a function over assumption bases . That is, the meaning of a proof is specified relative to a given assumption base, in the same way that in denotational semantics the formal meaning of an imperative program is a function over stores. Unlike sequent systems, where the manipulation of the context is explicit and falls on the user, the manipulation and threading of the context in DPLs is implicit and relegated to the underlying semantics---again, much as the manipulation and threading of the store in imperative languages is hidden from the user.
This turns out to be an apt viewpoint that is particularly conducive to giving a rigorous semantics to Fitch-style natural deduction. In general, the introduction of assumption bases as a fundamental semantic abstraction on a par with lexical environments, stores, and continuations allows for an elegant treatment of proof theory, even for logics that have been difficult to formalize in a non-graphical manner. The approach is different from that of systems based on higher-order constructive type theory, such as LF, Coq, or Nuprl. It is more similar to systems of the LCF variety (HOL, Isabelle, etc.), but again, the introduction of assumption bases and the syntactic separation of deduction and computation bring several advantages, e.g. sequents are no longer necessary, and proof abstraction is facilitated.
Moreover, assumption-base semantics enable a rich theory of observational equivalence for proofs, facilitating the formulation---and answering---of questions such as the following: