4 ms·

Insofar as the pull quotes that don't have plausible deniability are по-русски, I'm pretty sure the author knew what he was doing. (aiming at deliberate* impopu

• 082349872349872 3y ago
  eg completely SFW, the references for the design doc: Cardelli L. A Polymorphic [lambda]-calculus with Type: Type. – Digital Systems Research Center, 1986. ↩ ↩2 ↩3 John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (April 1960), 184–195. https://doi.org/10.1145/367177.367199 https://doi.org/10.1145/367177.367199 ↩ Turchin, Valentin F.. “A dialogue on Metasystem transition.” World Futures 45 (1995): 5-57. ↩ Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (June 2022), 38 pages. https://doi.org/10.1145/3450952 https://doi.org/10.1145/3450952 ↩ Gundry, Adam and Conor McBride. “A tutorial implementation of dynamic pattern unification A dependently typed programming language implementation pearl.” (2012). ↩ Kovács, András. “Elaboration with first-class implicit function types.” Proceedings of the ACM on Programming Languages 4 (2020): 1 - 29. ↩ Meven Lennon-Bertrand. (2021). Complete Bidirectional Typing for the Calculus of Inductive Constructions. ↩ Luca Cardelli. 1996. Type systems. ACM Comput. Surv. 28, 1 (March 1996), 263–264. https://doi.org/10.1145/234313.234418 https://doi.org/10.1145/234313.234418 ↩ Augustsson, L. (1999). Cayenne — A Language with Dependent Types. In: Swierstra, S.D., Oliveira, J.N., Henriques, P.R. (eds) Advanced Functional Programming. AFP 1998. Lecture Notes in Computer Science, vol 1608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10704973_6 https://doi.org/10.1007/10704973_6 ↩ ↩2 White, L., Bour, F., & Yallop, J. (2015). Modular implicits. Electronic Proceedings in Theoretical Computer Science, 198, 22–63. ↩ ↩2 Yang, Y., Bi, X., Oliveira, B.C.d.S. (2016). Unified Syntax with Iso-types. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_14 https://doi.org/10.1007/978-3-319-47958-3_14 ↩ ↩2 ↩3 Yang, Y., Bi, X., Oliveira, B.C.d.S.: Unified syntax with iso-types. Extended ver- sion available from https://bitbucket.org/ypyang/aplas16 https://bitbucket.org/ypyang/aplas16 (2016) ↩ Adam Chlipala. 2008. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN international conference on Functional programming (ICFP '08). Association for Computing Machinery, New York, NY, USA, 143–156. https://doi.org/10.1145/1411204.1411226 https://doi.org/10.1145/1411204.1411226 ↩ Gibbons, Jeremy & Wu, Nicolas. (2014). Folding domain-specific languages: Deep and shallow embeddings (functional Pearl). Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP. 49. 10.1145/2628136.2628138. ↩ Carette, J., Kiselyov, O., Shan, Cc. (2007). Finally Tagless, Partially Evaluated. In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_15 https://doi.org/10.1007/978-3-540-76637-7_15 ↩ ↩2 ↩3 ↩4 Kiselyov, O. (2012). Typed Tagless Final Interpreters. In: Gibbons, J. (eds) Generic and Indexed Programming. Lecture Notes in Computer Science, vol 7470. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32202-0_3 https://doi.org/10.1007/978-3-642-32202-0_3 ↩ ↩2 Coquand, Thierry & Kinoshita, Yoshiki & Nordstrom, Bengt & Takeyama, Makoto. (2009). A simple type-theoretic language: Mini-TT. From Semantics to Computer Science: Essays in Honour of Gilles Kahn. 10.1017/CBO9780511770524.007. ↩ ↩2 Altenkirch, T., Danielsson, N.A., Löh, A., Oury, N. (2010). ΠΣ: Dependent Types without the Sugar. In: Blume, M., Kobayashi, N., Vidal, G. (eds) Functional and Logic Programming. FLOPS 2010. Lecture Notes in Computer Science, vol 6009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12251-4_5 https://doi.org/10.1007/978-3-642-12251-4_5 ↩ Fu, P., Stump, A. (2014). Self Types for Dependently Typed Lambda Encodings. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_16 https://doi.org/10.1007/978-3-319-08918-8_16 ↩ KISELYOV O, MU S-C, SABRY A. Not by equations alone: Reasoning with extensible effects. Journal of Functional Programming. 2021;31:e2. doi:10.1017/S0956796820000271 ↩ Wadler, P. (1993). Monads for functional programming. In: Broy, M. (eds) Program Design Calculi. NATO ASI Series, vol 118. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-02880-3_8 https://doi.org/10.1007/978-3-662-02880-3_8 ↩ Pretnar, Matija. (2015). An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. Electronic Notes in Theoretical Computer Science. 319. 19-35. 10.1016/j.entcs.2015.12.003. ↩ P. Wadler and S. Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '89). Association for Computing Machinery, New York, NY, USA, 60–76. https://doi.org/10.1145/75277.75283 https://doi.org/10.1145/75277.75283 ↩ Meijer, E., Hughes, J. (Ed.), Fokkinga, M. M., & Paterson, R. (1991). Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. 124-144. Paper presented at 5th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA 1991). https://doi.org/10.1007/3540543961_7 https://doi.org/10.1007/3540543961_7 ↩ Peyton Jones, Simon. (2002). Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. ↩ Turchin V., Nemytykh, A. Metavariables: Their implementation and use in Program Transformation, CCNY Technical Report CSc TR-95-012, 1995. ↩ ↩2 Turchin V., Refal-5, Programming Guide and Reference Manual, New England Publishing Co., 1989. ↩ Nemytykh, A.P., Pinchuk, V.A., Turchin, V.F. (1996). A Self-Applicable supercompiler. In: Danvy, O., Glück, R., Thiemann, P. (eds) Partial Evaluation. Lecture Notes in Computer Science, vol 1110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61580-6_16 https://doi.org/10.1007/3-540-61580-6_16 ↩ Turchin, Valentin F.. “Program transformation with metasystem transitions.” Journal of Functional Programming 3 (1993): 283 - 313. ↩ Robert Glück and Morten Heine Sørensen. 1996. A Roadmap to Metacomputation by Supercompilation. In Selected Papers from the International Seminar on Partial Evaluation. Springer-Verlag, Berlin, Heidelberg, 137–160. ↩ Futamura, Y. (1983). Partial computation of programs. In: Goto, E., Furukawa, K., Nakajima, R., Nakata, I., Yonezawa, A. (eds) RIMS Symposia on Software Science and Engineering. Lecture Notes in Computer Science, vol 147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11980-9_13 https://doi.org/10.1007/3-540-11980-9_13 ↩ A.V. Klimov and S.A. Romanenko. Metavychislitel' dlja jazyka Refal. Osnovnye ponjatija i primery. (A metaevaluator for the language Refal. Basic concepts and examples). Preprint 71, Keldysh Institute of Applied Mathematics, Academy of Sciences of the USSR, Moscow, 1987. ↩ John Lamping. 1989. An algorithm for optimal lambda calculus reduction. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 16–30. https://doi.org/10.1145/96709.96711 https://doi.org/10.1145/96709.96711 ↩ Yves Lafont. 1989. Interaction nets. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 95–108. https://doi.org/10.1145/96709.96718 https://doi.org/10.1145/96709.96718 ↩ Yves Lafont. 1997. Interaction Combinators. Inf. Comput. 137, 1 (Aug. 25, 1997), 69–101. https://doi.org/10.1006/inco.1997.2643 https://doi.org/10.1006/inco.1997.2643 ↩ Andrea Asperti. (2017). About the efficient reduction of lambda terms. ↩ Cas van der Rest, Jaro Reinders, & Casper Bach Poulsen. (2022). Handling Higher-Order Effects. ↩ Thierry Coquand, & Gérard Huet (1988). The calculus of constructions. Information and Computation, 76(2), 95-120. ↩ 1948, Human Knowledge: Its Scope and Limits by Bertrand Russell, Section: Part II: Language, Chapter I: The Uses of Language Quote Page 60, Simon and Schuster, New York. ↩ Turchin, Valentin F. "Equivalent transformations of Refal programs." Avtomatizirovannaja Sistema upravlenija stroitel'stvom. Trudy CNIPIASS 6 (1974): 36-68. ↩ Dijkstra, Edsger W.. “A Discipline of Programming.” (1976). ↩ Perlis, Alan J.. “Epigrams on Programming.” Sigplan Notices 17 (1982): 7-13. ↩ Edsger W. Dijkstra. 1972. The humble programmer. Commun. ACM 15, 10 (Oct. 1972), 859–866. https://doi.org/10.1145/355604.361591 https://doi.org/10.1145/355604.361591 ↩