Arithmetical proofs of strong normalization results for symmetric lambda calculi
| dc.creator | David, René | |
| dc.creator | Nour, Karim | |
| dc.date | 2009-05-06 | |
| dc.date.accessioned | 2026-07-07T13:12:13Z | |
| dc.date.available | 2026-07-07T13:12:13Z | |
| dc.description | We give arithmetical proofs of the strong normalization of two symmetric $λ$-calculi corresponding to classical logic. The first one is the $\barλμ\tildeμ$-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric $λμ$-calculus. It is the $λμ$-calculus introduced by Parigot in which the reduction rule $μ'$, which is the symmetric of $μ$, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical. | |
| dc.identifier | https://arxiv.org/abs/0905.0762 | |
| dc.identifier | http://arxiv.org/abs/0905.0762 | |
| dc.identifier | Fundamenta Informaticae 77, 4 (2007) 489-510 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/229516 | |
| dc.subject | Logic | |
| dc.title | Arithmetical proofs of strong normalization results for symmetric lambda calculi | |
| dc.type | text |