Arithmetical proofs of strong normalization results for the symmetric $λμ$-calculus
| dc.creator | David, René | |
| dc.creator | Nour, Karim | |
| dc.date | 2009-05-07 | |
| dc.date.accessioned | 2026-07-07T13:12:40Z | |
| dc.date.available | 2026-07-07T13:12:40Z | |
| dc.description | The symmetric $λμ$-calculus is the $λμ$-calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of $μ$, is added. We give arithmetical proofs of some strong normalization results for this calculus. We show (this is a new result) that the $μμ'$-reduction is strongly normalizing for the un-typed calculus. We also show the strong normalization of the $βμμ'$-reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical. | |
| dc.identifier | https://arxiv.org/abs/0905.1034 | |
| dc.identifier | http://arxiv.org/abs/0905.1034 | |
| dc.identifier | Typed Lambda Calculi and Applications, Nara : Japon (2005) | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/229647 | |
| dc.subject | Logic | |
| dc.title | Arithmetical proofs of strong normalization results for the symmetric $λμ$-calculus | |
| dc.type | text |