José Espírito Santo
CMAT - University of Minho
A natural deduction system  is presented for polarized, intuitionistic, propositional logic with several interesting properties : it has a privileged relationship with a standard focused sequent calculus ; it enjoys the subformula property; polarity decides whether the elimination rules are generalized or not ; there are no commutative conversions; and even atomic formulas have introduction, elimination and normalization rules. In the corresponding polarized lambda-calculus, reduction follows a paradigm that subsumes both call-by-name and call-by-value .
 Dag Prawitz. Natural Deduction. A Proof-Theoretical Study. Almquist and Wiksell, Stockholm, 1965.
 José Espírito Santo. The polarized λ-calculus. Electronic Notes in Theoretical Computer Science 332: 149–168, 2017
 Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747–4768, 2009.
 Jan von Plato. Natural deduction with general elimination rules. Archive for Mathematical Logic, 40(7):541–567, 2001.
 Paul B. Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher Order and Symbolic Computation, 19(4): 377–414, 2006
Zoom link: https://videoconf-colibri.zoom.us/j/86389857315