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