For any , and for any {{ 1 , ? , } , there exists an equivalent command derived from smaller commands of type 1 , ? , by application of a rule in Fig ,
The result follows from Lemma 42 by mapping each inversion as follows ,
Up to equivalence, one can assume R -normal: indeed, the normal form exists by Theorem 55, its derivation is equivalent by Lemma 42, and it has the same size by definition. Then one has either = () or = () as observed in Proposition 32, with and R -normal. We sort them into one of three cases: either +, or ! + , derived as in the above statement ,
Categorical and Kripke Semantics for Constructive S4 Modal Logic, Proc. CSL, pp.292-307, 2001. ,
DOI : 10.1007/3-540-44802-0_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.6306
Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992. ,
DOI : 10.1093/logcom/2.3.297
Infinitary proof theory: the multiplicative additive case, Proc. CSL, p.48, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01339037
10 [BNG15] Taus Brock-Nannestad and Nicolas Guenot, Focused linear logic and the -calculus, Proc. TLCA, pp.78-93, 1995. ,
Computation in focused intuitionistic logic, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP '15, pp.43-54, 2015. ,
DOI : 10.1007/10721975_10
URL : https://hal.archives-ouvertes.fr/hal-01249216
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proc. POPL, p.47, 2006. ,
URL : https://hal.archives-ouvertes.fr/hal-01256092
The duality of computation, ACM SIGPLAN Notices, vol.35, issue.9, pp.233-243, 2000. ,
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377
A multi-focused proof system isomorphic to expansion proofs, Journal of Logic and Computation, vol.26, issue.2, p.47, 2014. ,
DOI : 10.1093/logcom/exu030
URL : https://hal.archives-ouvertes.fr/hal-00937056
The Duality of Computation under Focus, Proc. IFIP TCS, p.46, 2010. ,
DOI : 10.1007/978-3-642-15240-5_13
URL : https://hal.archives-ouvertes.fr/inria-00491236
Canonical sequent proofs via multifocusing , Fifth Ifip International Conference On Theoretical Computer Science?Tcs, pp.383-396, 2008. ,
On closed categories of functors, Lecture Notes in Mathematics, issue.137, pp.1-38, 1970. ,
DOI : 10.1007/bfb0060438
A New Deconstructive Logic: Linear Logic, Limits of small functors, pp.755-807, 1997. ,
The enriched effect calculus: syntax and semantics, Journal of Logic and Computation, vol.24, issue.3, pp.615-654, 2012. ,
DOI : 10.1093/logcom/exs025
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.997
On the expressive power of programming languages, Science of Computer Programming, vol.17, issue.1-3, pp.35-75, 1991. ,
DOI : 10.1016/0167-6423(91)90036-W
Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Gir91] _ , A new constructive logic: Classical logic II: Vers l'imperfection, Visions des Sciences, pp.37-38, 1972. ,
Lectures on Logic 10 [Kri93] Jean-Louis Krivine, Lambda-calculus, types and models, Has16] Masahito Hasegawa, Linear exponential comonads without symmetry, Fourth International Workshop on Linearity Classical Logic, Panoramas et Synthèses, pp.50-87, 1701. ,
A proof of the focalization property of linear logic, lecture notes, p.46, 2004. ,
Adjunction models for call-by-push-value with stacks, Theory and Application of Categories, pp.75-110, 2005. ,
Focusing and Polarization in Intuitionistic Logic, CSL Focusing and polarization in linear, intuitionistic, and classical logics, Theor. Comput. Sci, vol.410, issue.42, pp.451-465, 2007. ,
DOI : 10.1016/j.tcs.2009.07.041
URL : http://doi.org/10.1016/j.tcs.2009.07.041
Categorical semantics of linear logic, Panoramas et Synthèses, Maccagnoni, Focalisation and Classical Realisability Proc. CSL, pp.10-15, 2009. ,
Polarised Intermediate Representation of Lambda Calculus with Sums, Proc. LICS 2015, p.47, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01160579
Whats is a categorical model of linear logic, p.10, 2004. ,
Multi-focusing on extensional rewriting with sums, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 LIPIcs Schloss Dagstuhl -Leibniz- Zentrum fuer Informatik, pp.317-331, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01235372
Structural Focalization, ACM Transactions on Computational Logic, vol.15, issue.3, pp.1-21, 2014. ,
DOI : 10.1007/s10990-011-9071-2
URL : http://arxiv.org/abs/1109.6273
Weak Orthogonality Implies Confluence: The Higher Order Case, Proc. LFCS Femke van Raamsdonk, Higher-order Rewriting, Proc. Rewrit. Tech. App, pp.379-392, 1994. ,
Call-by-value is dual to call-by-name, SIGPLAN Not, pp.189-201, 2003. ,
DOI : 10.1145/944705.944723