Por José Espírito Santo (Centro de Matemática - Universidade do Minho).

In the context of polarized, intuitionistic propositional logic, starting from a fairly standard focused sequent calculus, a bidirectional natural deduction system is derived by an equally standard process. The result is a very disciplined and interesting syntax: the subformula property holds, polarity decides the style of the elimination rules, 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.

Zoom | ID da reunião: 890 8479 3299 - senha de acesso: 409604