**José Espírito Santo**

*Centro de Matemática da Universidade do Minho*

**A generalization of modus ponens and the theory of call-by-value**

In Logic, a recent development proposed that natural deduction should be formulated with generalized elimination rules, in order to implement the principle: whatever follows from the immediate grounds for deriving a proposition should also follow from the proposition. This means that, in particular, one has to change nothing less than the inference rule of *modus ponens*. In this talk it will be shown how such move can be used in Computer Science. Since the seminal paper by Plotkin in 1975, computer scientists propose variants of the lambda-calculus that can serve as a theoretical model of call-by-value functional programming. One such lambda-calculus can be obtained from the mentioned deductive system - provided one goes even further and also redefines the concept of substitution. As a result, a dogma lasting since Plotkin's paper falls: call-by-name and call-by-value can simulate each other without the need for cps-translations.

(See http://www.wld.cipsh.international/wld.html for more on the World Logic Day)

https://videoconf-colibri.zoom.us/j/9301932415