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)