[TYPES] Recovering functions from classical disjunction and negation

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

In classical logic, implication A -> B can be encoded as (not A \/ B).

Is there any work on how that encoding works on the term side of things, 
that is, how
to encode lambda abstraction and application in terms of these logical 
connectives.
For instance, there are variants of Parigot's lambda mu calculus with 
primitive disjunction
and negation (such as by Pym, Ritter and Wallen or de Groote (2001) ). 
Shouldn't it
be possible to remove implication / lambda from such calculi and encode 
them as macros?
Has this been done?

Regards,

Klaus