(Downloads - 0)
For more info about our services contact : help@bestpfe.com
Table of contents
Introduction
1 Normalization properties of the λμμ′-calculus
1.1 The Parigot-style λμμ′-calculus
1.1.1 The θ-rule can be postponed
1.1.2 The ρ-rule can be postponed
1.1.3 The Parigot-style λμμ′-calculus strongly normalizes
1.2 The de Groote-style λμμ′-calculus
1.2.1 A strong normalization proof for the μμ′-calculus
1.2.2 The μμ′ρ-calculus is not strongly normalizing
1.2.3 The μμ′ρ-calculus is weakly normalizing
1.2.4 The λμμ′ρ-calculus is weakly normalizing
1.2.5 The λμμ′ρθ-calculus
1.2.6 Standardization for the λμμ′ρθ-calculus
1.2.7 Concluding remarks
2 An estimation for the lengths of reduction sequences of the λμρθ- calculus
2.0.8 Standardization in the λμρθ-calculus
2.0.9 On the lengths of standard reduction sequences
2.0.10 The estimation for the λμρθI-calculus
2.0.11 The general case
2.1 Concluding remarks
2.1.1 A possible attempt to calculate an upper bound for the λμρ- calculus
2.1.2 A translation of the λμ-calculus into the λ∗c -calculus
3 Strong normalization of the λ Sym Prop-calculus
3.1 The λ-calculus is strongly normalizing
3.2 The cases of the η- and η⊥-reductions
3.3 The λ Sym Prop-calculus is strongly normalizing
4 Translations between the λ Sym Prop-calculus and the λμ˜μ∗-calculus
4.1 Relating the λ Sym Prop-calculus to the λμ˜μ∗-calculus
4.1.1 The λμ˜μ∗-calculus
4.1.2 A translation of the λμ˜μ∗-calculus into the λ Sym Prop-calculus
4.1.3 A translation of the λ Sym Prop-calculus into the λμ˜μ∗-calculus
4.1.4 The connection between the two translations
4.2 Concluding remarks
4.2.1 The strong normalization of the μ˜μ-calculus
4.2.2 The strong normalization of the λμ˜μ∗-calculus
Conclusions
Overview
Open questions
Bibliography
