## MAP-PDMA

**José Espírito Santo**

*CMAT - University of Minho*

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

**Abstract ::**

A natural deduction system [1] is presented for polarized, intuitionistic, propositional logic with several interesting properties [2]: it has a privileged relationship with a standard focused sequent calculus [3]; it enjoys the subformula property; polarity decides whether the elimination rules are generalized or not [4]; 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 [5].

**References**

[1] Dag Prawitz. Natural Deduction. A Proof-Theoretical Study. Almquist and Wiksell, Stockholm, 1965.

[2] José Espírito Santo. The polarized λ-calculus. Electronic Notes in Theoretical Computer Science 332: 149–168, 2017

[3] Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747–4768, 2009.

[4] Jan von Plato. Natural deduction with general elimination rules. Archive for Mathematical Logic, 40(7):541–567, 2001.

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

Seminar for the Doctoral Program in Applied Mathematics (MAP-PDMA Seminar)