Диссертация (1150902), страница 17
Текст из файла (страница 17)
В частности, применяя вторую проекцию Футамуры–Ершова–Турчина (специализируя специализатор на алгоритм трассирующей нормализации) становится возможной генерациякомпиляторов для языков программирования.В качестве перспектив дальнейшей разработки тематики может быть отмечено следующее: (1) описание известных языковых конструкций и программных трансформаций с помощью подхода трассирующей нормализации; (2) разработка, на основе предложенного подхода, универсального языка промежуточногопредставления, который может служить базой для описания семантик широкогокласса языков программирования, позволяя автоматически генерировать компиляторы соответствующих языков, а также (3) исследование свойств вычислимостии сложности программ в рамках подхода трассирующей нормализации.98Литература1.
Мартыненко, Б. К. Языки и трансляции / Б. К. Мартыненко. — Изд-во С.Петерб. ун-та СПб., 2004.2. Jones, N. D. Computability and complexity - from a programming perspective /N. D. Jones. Foundations of computing series. — MIT Press, 1997.3. Michaelson, G. J. An introduction to functional programming through lambdacalculus / G. J. Michaelson. International computer science series. — AddisonWesley, 1989.4. Church, A. A Formulation of the Simple Theory of Types / A.
Church // J. Symb.Log. — 1940. — Vol. 5, no. 2. — P. 56–68.5. Plotkin, G. D. LCF Considered as a Programming Language / G. D. Plotkin //Theor. Comput. Sci. — 1977. — Vol. 5, no. 3. — P. 223–255.6. Ong, C.-H. L. Normalisation by Traversals / C.-H. L. Ong // CoRR. — 2015.— Т. abs/1511.02629. — URL: http://arxiv.org/abs/1511.02629(дата обращения: 07.12.2017).7. Blum, W. The safe lambda calculus / W.
Blum // Ph.D. thesis, University of Oxford, UK. — 2009.8. Danos, V. Head linear reduction / V. Danos, L. Regnier // unpublished.—2004. —URL: https://pdfs.semanticscholar.org/e2ce/424ff63ac58b7b1737b13166fda9a96f3dda.pdf (дата обращения:07.12.2017).9. Danos, V. Game Semantics & Abstract Machines / V. Danos, H. Herbelin, L. Regnier // Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science,99New Brunswick, New Jersey, USA, July 27-30, 1996. — IEEE Computer Society,1996. — P. 394–405.10. Fredriksson, O. Abstract Machines for Game Semantics, Revisited / O.
Fredriksson, D. R. Ghica // 28th Annual ACM/IEEE Symposium on Logic in ComputerScience, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. — IEEE Computer Society, 2013. — P. 560–569.11. Ong, C.-H. L. On Model-Checking Trees Generated by Higher-Order RecursionSchemes / C.-H. L. Ong // 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings. — IEEEComputer Society, 2006. — P. 81–90.12.
Neatherway, R. P. A traversal-based algorithm for higher-order model checking / R. P. Neatherway, S. J. Ramsay, C.-H. L. Ong // ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark,September 9-15, 2012 / Ed. by P. Thiemann, R. B. Findler. — ACM, 2012. —P. 353–364.13. Lévy, J.-J.
Optimal reductions in the lambda-calculus / J.-J. Lévy // In To H.B.Curry: Essays on Combinatory Logic, Lambda Caclulus and Formalism. — Academic Press, 1980.14. Lamping, J. An Algorithm for Optimal Lambda Calculus Reduction / J. Lamping //Conference Record of the Seventeenth Annual ACM Symposium on Principlesof Programming Languages, San Francisco, California, USA, January 1990. —1990.
— P. 16–30.15. Shivers, O. Bottom-Up beta-Reduction: Uplinks and lambda-DAGs / O. Shivers,M. Wand // Lecture Notes in Computer Science, Programming Languages andSystems, 14th European Symposium on Programming,ESOP 2005, Held as Part ofthe Joint European Conferences on Theory and Practice of Software, ETAPS 2005,Edinburgh, UK, April 4-8, 2005, Proceedings / Ed. by S.
Sagiv. — Vol. 3444. —Springer, 2005. — P. 217–232.10016. van Oostrom, V. Lambdascope another optimal implementation of the lambdacalculus / V. van Oostrom, K.-J. van de Looij, M. Zwitserlood // In Workshop onAlgebra and Logic on Programming Systems (ALPS). — 2004.17. Baillot, P. Elementary Complexity and Geometry of Interaction / P. Baillot,M. Pedicini // Fundam. Inform. — 2001. — Vol. 45, no. 1-2. — P. 1–31.18. Lafont, Y. Interaction Nets / Y.
Lafont // Conference Record of the SeventeenthAnnual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990. — 1990. — P. 95–108.19. Mascari, G. Head Linear Reduction and Pure Proof Net Extraction / G. Mascari,M. Pedicini // Theor. Comput. Sci. — 1994. — Vol.
135, no. 1. — P. 111–137.20. Heijltjes, W. Proof Nets for Additive Linear Logic with Units / W. Heijltjes //Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science,LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada. — 2011. — P. 207–216.21. Church, A. Correction to A Note on the Entscheidungsproblem / A. Church // J.Symb. Log. — 1936. — Vol. 1, no. 3.
— P. 101–102.22. Church, A. A Note on the Entscheidungsproblem / A. Church // J. Symb. Log. —1936. — Vol. 1, no. 1. — P. 40–41.23. Newman, M. H. A. A Formal Theorem in Church’s Theory of Types /M. H. A. Newman, A. M. Turing // J. Symb. Log. — 1942. — Vol. 7, no. 1.— P. 28–33.24.
Turing, A. M. Computability and λ-Definability / A. M. Turing // J. Symb. Log.— 1937. — Vol. 2, no. 4. — P. 153–163.25. Turing, A. M. The p-Function in λ-K-Conversion / A. M. Turing // J. Symb. Log.— 1937. — Vol. 2, no. 4. — P. 164.26. Curry, H. B. Consistency and Completeness of the Theory of Combinators /H. B. Curry // J. Symb. Log.
— 1941. — Vol. 6, no. 2. — P. 54–61.27. Curry, H. B. The Inconsistency of Certain Formal Logic / H. B. Curry // J. Symb.Log. — 1942. — Vol. 7, no. 3. — P. 115–117.10128. Curry, H. B. The Combinatory Foundations of Mathematical Logic / H. B. Curry //J. Symb. Log. — 1942. — Vol. 7, no. 2. — P. 49–64.29. Curry, H. B. The Permutability of Rules in the Classical Inferential Calculus /H. B. Curry // J. Symb. Log. — 1952. — Vol. 17, no.
4. — P. 245–248.30. Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics / H.P. Barendregt. Studies in Logic and the Foundations of Mathematics. — Elsevier Science,2013.31. Pierce, B. C. Advanced Topics in Types and Programming Languages /B. C. Pierce. — The MIT Press, 2004.32. Scott, D. S. Domains for Denotational Semantics / D.
S. Scott // Lecture Notesin Computer Science, Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings / Ed. by M. Nielsen,E. M. Schmidt. — Vol. 140. — Springer, 1982. — P. 577–613.33. Scott, D. S. Logic and Programming Languages / D. S. Scott // Commun. ACM.— 1977. — Vol. 20, no. 9. — P. 634–641.34. Scott, D.
S. Data Types as Lattices / D. S. Scott // SIAM J. Comput. — 1976. —Vol. 5, no. 3. — P. 522–587.35. Scott, D. S. Combinators and classes / D. S. Scott // Lecture Notes in Computer Science, Lambda-Calculus and Computer Science Theory, Proceedings of theSymposium Held in Rome, March 25-27, 1975 / Ed. by C. Böhm. — Vol. 37. —Springer, 1975.
— P. 1–26.36. Hennessy, M. Full Abstraction for a Simple Parallel Programming Language /M. Hennessy, G. D. Plotkin // Lecture Notes in Computer Science, MathematicalFoundations of Computer Science 1979, Proceedings, 8th Symposium, Olomouc,Czechoslovakia, September 3-7, 1979 / Ed. by J. Becvár. — Vol. 74. — Springer,1979.
— P. 108–120.37. Lorenzen, P. Algebraische und Logistische Untersuchungen Über Freie Verbände /P. Lorenzen // J. Symb. Log. — 1951. — Vol. 16, no. 2. — P. 81–106.10238. Lorenz, K. Rules versus theorems / K. Lorenz // J. Philosophical Logic. — 1973.— Vol. 2, no. 3. — P. 352–369.39. Hyland, J. M. E. On Full Abstraction for PCF: I, II, and III / J.
M. E. Hyland,C.-H. L. Ong // Inf. Comput. — 2000. — Vol. 163, no. 2. — P. 285–408.40. Abramsky, S. Full Abstraction for PCF / S. Abramsky, P. Malacaria, R. Jagadeesan // Lecture Notes in Computer Science, Theoretical Aspects of ComputerSoftware, International Conference TACS ’94, Sendai, Japan, April 19-22, 1994,Proceedings / Ed. by M. H., J. C. Mitchell. — Vol. 789. — Springer, 1994. —P. 1–15.41.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
