[TYPES] Recovering functions from classical disjunction and negation

[Gabriel Scherer]

Yes ! (I would consider it folklore now.)

This is explicitly written out, for example, in Wadler's "Call-by-Value is
Dual to Call-by-Name", 2003 -- propositions 5.2 and 5.3, page 8 of
  https://urldefense.com/v3/__https://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf__;!!IBzWLUs!FW5mQvtua1NFPPztYIIgaWEUxhsni5aYR8rRMELFL1q--cmMQj4e3nlcNlMgr8QUrF_0IfYjOd8$ 


On Sat, Aug 28, 2021 at 11:51 PM Klaus Ostermann <
klaus.ostermann at uni-tuebingen.de> wrote:

> [ 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
>
>
>