A nonstandard standardization theorem. (English) Zbl 1284.68121
Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 659-670 (2014).
MSC:
| 68N18 | Functional programming and lambda calculus |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q42 | Grammars and rewriting systems |
| 03B70 | Logic in computer science |
References:
| [1] | M. Abadi, L. Cardelli, P. L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 4(1):375-416, 1991. · Zbl 0941.68542 |
| [2] | B. Accattoli. An abstract factorization theorem for explicit substitutions. In RTA, pages 6-21, 2012. · Zbl 1437.68038 |
| [3] | B. Accattoli. Evaluating functions as processes. In TERMGRAPH, pages 41-55, 2013. · Zbl 1464.68219 |
| [4] | B. Accattoli. Jumping around the box: graphical and operational studies on λ-calculus and Linear Logic. PhD thesis, La Sapienza University of Rome, february 2011. |
| [5] | B. Accattoli and U. Dal Lago. On the invariance of the unitary cost model for head reduction. In RTA, pages 22-37, 2012. · Zbl 1437.68039 |
| [6] | B. Accattoli and D. Kesner. The structural λ-calculus. In CSL, pages 381-395, 2010. |
| [7] | B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines. Submitted, 2013. https://sites.google.com/site/beniaminoaccattoli/machines.pdf?attredirects=0. |
| [8] | H. P. Barendregt, R. Kennaway, J. W. Klop, and M. R. Sleep. Needed reduction and spine strategies for the lambda calculus. Information and Computation, 75(3):191-231, 1987. 10.1016/0890-5401(87)90001-0 · Zbl 0635.03009 |
| [9] | R. Bloo and K. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In Computing Science in the Netherlands, pages 62-72. Netherlands Computer Science Research Foundation, 1995. |
| [10] | G. Boudol. Computational semantics of term rewriting systems. In Algebraic methods in semantics, pages 169-236. Cambridge University Press, 1986. |
| [11] | H. S. Bruggink. Equivalence of reductions in higher-order rewriting. PhD thesis, Utrecht University, 2008. |
| [12] | D. Clark and R. Kennaway. Some properties of non-orthogonal term graph rewriting systems. In SEGRAGRA, volume 2 of ENTCS, pages 36-45, 1995. |
| [13] | H. Curry and R. Feys. Combinatory Logic. Number Vol. 1 in Studies in logic and the foundations of mathematics. North-Holland, 1958. · Zbl 0081.24104 |
| [14] | V. Danos and L. Regnier. Head linear reduction, 2003. http://iml.univ-mrs.fr/ regnier/articles/pam.ps.gz. |
| [15] | V. Danos, H. Herbelin, and L. Regnier. Game semantics & abstract machines. In LICS, pages 394-405, 1996. |
| [16] | D. de Carvalho, M. Pagani, and L. Tortora de Falco. A semantic measure of the execution time in linear logic. Theor. Comput. Sci., 412(20):1884-1902, 2011. 10.1016/j.tcs.2010.12.017 · Zbl 1222.03070 |
| [17] | T. Ehrhard and L. Regnier. Böhm trees, krivine’s machine and the taylor expansion of lambda-terms. In CiE, pages 186-197, 2006. 10.1007/11780342_20 · Zbl 1130.68054 |
| [18] | J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037 |
| [19] | G. Gonthier, J.-J. Lévy, and P.-A. Melli‘es. An abstract standardisation theorem. In LICS, pages 72-81, 1992. |
| [20] | G. Huet. Residual theory in λ-calculus: A formal development. Journal of Functional Programming, 4(3):371-394, 1994. · Zbl 0826.03008 |
| [21] | G. Huet and J.-J. Lévy. Computations in orthogonal rewriting systems, I and II. In Computational Logic - Essays in Honor of Alan Robinson, pages 395-414, 1991. |
| [22] | G. Huet and J.-J. Lévy. Call by Need computations in non ambiguous linear term rewriting systems. Technical Report 359, INRIA, 1979. |
| [23] | D. Kesner and S. Lengrand. Resource operators for lambda-calculus. Information and Computation, 205(4):419-473, 2007. 10.1016/j.ic.2006.08.008 · Zbl 1111.68018 |
| [24] | D. Kesner and S. O’Conchúir. Milner’s lambda calculus with partial substitutions, 2008. http://www.pps.univ-paris-diderot.fr/ kesner/papers/shortpartial.pdf. |
| [25] | Z. Khasidashvili and J. R. W. Glauert. Discrete normalization and standardization in deterministic residual structures. In ALP, pages 135-149, 1996. · Zbl 1355.68139 |
| [26] | J. W. Klop. Combinatory Reduction Systems. Phd thesis, Utrecht University, 1980. · Zbl 0466.03006 |
| [27] | J.-J. Lévy. Réductions correctes et optimales dans le lambda calcul. Thése d’Etat, Univ. Paris VII, France, 1978. |
| [28] | L. Maranget. Optimal derivations in weak lambda-calculi and in orthogonal terms rewriting systems. In POPL, pages 255-269, 1991. 10.1145/99583.99618 |
| [29] | G. Mascari and M. Pedicini. Head linear reduction and pure proof net extraction. Theoretical Computer Science, 135(1):111-137, 1994. 10.1016/0304-3975(94)90263-1 · Zbl 0834.68104 |
| [30] | P.-A. Melliès. Axiomatic rewriting theory I: A diagrammatic standardization theorem. In Processes, Terms and Cycles: Steps on the Road to Infinity, volume 3838 of LNCS, pages 554-638. Springer, 2005. · Zbl 1171.68515 |
| [31] | P.-A. Melliès. Axiomatic rewriting theory VI: Residual theory revisited. In RTA, pages 24-50, 2002. · Zbl 1045.68075 |
| [32] | P.-A. Melliès. Description Abstraite de système de réécriture. PhD thesis, Paris 7 University, 1996. |
| [33] | R. Milner. Local bigraphs and confluence: Two conjectures. ENTCS, 175(3):65-73, 2007. 10.1016/j.entcs.2006.07.035 · Zbl 1277.68197 |
| [34] | L. Paolini and S. Ronchi Della Rocca. Parametric parameter passing lambda-calculus. Information and Computation, 189(1):87-106, 2004. 10.1016/j.ic.2003.08.003 · Zbl 1082.68015 |
| [35] | G. D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975. · Zbl 0325.68006 |
| [36] | L. Regnier. Une équivalence sur les lambda-termes. Theoretical Computer Science, 2(126):281-292, 1994. 10.1016/0304-3975(94)90012-4 · Zbl 0801.03013 |
| [37] | M. Takahashi. Parallel reductions in λ-calculus. Inf. Comput., 118(1): 120-127, 1995. 10.1006/inco.1995.1057 · Zbl 0827.68060 |
| [38] | Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. |
| [39] | V. van Oostrom. Normalisation in weakly orthogonal rewriting. In RTA, pages 60-74, 1999. |
| [40] | V. van Oostrom and R. C. de Vrijer. Four equivalent equivalences of reductions. ENTCS, 70(6):21-61, 2002. · Zbl 1270.68142 |
| [41] | H. Xi. Upper bounds for standardizations and an application. Journal of Symbolic Logic, 64(1):291-303, 1999. · Zbl 0938.03027 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
