Incorporating quotation and evaluation into Church’s type theory. (English) Zbl 1390.68168
Summary: ctt\(_{\mathrm{qe}}\) is a version of Church’s type theory that includes quotation and evaluation operators that are similar to quote and eval in the Lisp programming language. With quotation and evaluation it is possible to reason in ctt\(_{\mathrm{qe}}\) about the interplay of the syntax and semantics of expressions and, as a result, to formalize syntax-based mathematical algorithms. We present the syntax and semantics of ctt\(_{\mathrm{qe}}\) as well as a proof system for ctt\(_{\mathrm{qe}}\). The proof system is shown to be sound for all formulas and complete for formulas that do not contain evaluations. We give several examples that illustrate the usefulness of having quotation and evaluation in ctt\(_{\mathrm{qe}}\).
Keywords:
Church’s type theory; simple type theory; metareasoning; reflection; quotation; evaluation; quasiquotation; reasoning about syntax; schemas; symbolic computation; meaning formulas; substitutionSoftware:
ML; Theorema; Coq; ACL2; IMPS; ETPS; MetaPRL; Agda; HOL; MetaOCaml; NQTHM; Nuprl; MathScheme; HOL Light; MiniML; Idris; reFLect; HOL Light QEReferences:
| [1] | Abadi, M.; Cardelli, L.; Curien, P.-L.; Lévy, J.-J., Explicit substitution, J. Funct. Program., 1, 375-416 (1991) · Zbl 0941.68542 |
| [2] | Allen, S. F.; Constable, R. L.; Howe, D. J.; Aitken, W. E., The semantics of reflected proof, (Proceedings of the Fifth Annual Symposium on Logic in Computer Science. Proceedings of the Fifth Annual Symposium on Logic in Computer Science, LICS ’90 (1990), IEEE Computer Society), 95-105 · Zbl 0825.68599 |
| [3] | Andrews, P. B., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2002), Kluwer · Zbl 1002.03002 |
| [4] | Atkey, R., Syntax for free: representing syntax with binding using parametricity, (International Conference on Typed Lambda Calculi and Applications (2009), Springer), 35-49 · Zbl 1246.68084 |
| [5] | Atkey, R.; Lindley, S.; Yallop, J., Unembedding domain-specific languages, (Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell (2009), ACM), 37-48 |
| [6] | Barendregt, H., The impact of the lambda calculus in logic and computer science, Bull. Symb. Log., 3, 181-215 (1997) · Zbl 0887.03008 |
| [7] | Barzilay, E., Implementing Reflection in Nuprl (2005), Cornell University, Ph.D. thesis |
| [8] | Bawden, A., Quasiquotation in Lisp, (Danvy, O., Proceedings of the 1999 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (1999), University of Aarhus), 4-12, Technical Report BRICS-NS-99-1 |
| [9] | Berarducci, A.; Böhm, C., A self-interpreter of lambda calculus having a normal form, (Börger, E.; Jäger, G.; Büning, H. K.; Martini, S.; Richter, M. M., Computer Science Logic. Computer Science Logic, Lecture Notes in Computer Science, vol. 702 (1993), Springer), 85-99 · Zbl 0796.03023 |
| [10] | Berger, M.; Tratt, L.; Urban, C., Modelling homogeneous generative meta-programming (2016), Computing Research Repository (CoRR) |
| [11] | Böhm, C.; Berarducci, A., Automatic synthesis of typed lambda-programs on term algebras, Theor. Comput. Sci., 39, 135-154 (1985) · Zbl 0597.68017 |
| [12] | Böhm, C.; Piperno, A.; Guerrini, S., Lambda-definition of function(al)s by normal forms, (Sannella, D., Programming Languages and Systems — ESOP’94. Programming Languages and Systems — ESOP’94, Lecture Notes in Computer Science, vol. 788 (1994), Springer), 135-149 |
| [13] | Boulton, R.; Gordon, A.; Gordon, M.; Harrison, J.; Herbert, J.; Tassel, J. V., Experience with embedding hardware description languages in HOL, (Stavridou, V.; Melham, T. F.; Boute, R. T., Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience. Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, IFIP Transactions A: Computer Science and Technology, vol. A-10 (1993), North-Holland), 129-156 |
| [14] | Boutin, S., Using reflection to build efficient and certified decision procedures, (Abadi, M.; Ito, T., Theoretical Aspects of Computer Software. Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, vol. 1281 (1997), Springer), 515-529 |
| [15] | Boyer, R.; Moore, J., Metafunctions: proving them correct and using them efficiently as new proof procedures, (Boyer, R.; Moore, J., The Correctness Problem in Computer Science (1981), Academic Press), 103-185 · Zbl 0476.68009 |
| [16] | Boyer, R.; Moore, J., A Computational Logic Handbook (1988), Academic Press · Zbl 0655.68117 |
| [17] | Braibant, T.; Pous, D., Tactics for reasoning modulo AC in Coq, (Jouannaud, J.; Shao, Z., Certified Programs and Proofs. Certified Programs and Proofs, CPP 2011. Certified Programs and Proofs. Certified Programs and Proofs, CPP 2011, Lecture Notes in Computer Science, vol. 7086 (2011), Springer), 167-182 · Zbl 1350.68227 |
| [18] | Brown, M.; Palsberg, J., Self-representation in girard’s system u, ACM SIGPLAN Not., 50, 1, 471-484 (2015) · Zbl 1345.68039 |
| [19] | Brown, M.; Palsberg, J., Breaking through the normalization barrier: a self-interpreter for F-omega, (Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 (2016), ACM), 5-17 · Zbl 1347.68046 |
| [20] | Brown, M.; Palsberg, J., Typed self-evaluation via intensional type functions, (Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. (2017)), 415-428 · Zbl 1380.68090 |
| [21] | Brown, M.; Palsberg, J., Jones-optimal partial evaluation by specialization-safe normalization, Proc. ACM Program. Lang., 2, POPL, Article 14 pp. (2018) |
| [22] | Buchberger, B.; Craciun, A.; Jebelean, T.; Kovacs, L.; Kutsia, T.; Nakagawa, K.; Piroi, F.; Popov, N.; Robu, J.; Rosenkranz, M.; Windsteiger, W., Theorema: towards computer-aided mathematical theory exploration, J. Appl. Log., 4, 470-504 (2006) · Zbl 1107.68095 |
| [23] | Calcagno, C.; Taha, W.; Huang, L.; Leroy, X., Implementing multi-stage languages using ASTs, gensym, and reflection, (Pfenning, F.; Smaragdakis, Y., Generative Programming and Component Engineering. Generative Programming and Component Engineering, GPCE 2003. Generative Programming and Component Engineering. Generative Programming and Component Engineering, GPCE 2003, Lecture Notes in Computer Science, vol. 2830 (2003), Springer), 57-76 |
| [24] | Cappelen, H.; LePore, E., Quotation, (Zalta, E. N., The Stanford Encyclopedia of Philosophy (2012)) |
| [25] | Carette, J.; Farmer, W. M., High-level theories, (Autexier, A.; Campbell, J.; Rubio, J.; Suzuki, M.; Wiedijk, F., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 5144 (2008), Springer), 232-245 · Zbl 1166.68338 |
| [26] | Carette, J.; Farmer, W. M., Formalizing mathematical knowledge as a biform theory graph: a case study, (Geuvers, H.; England, M.; Hasan, O.; Rabe, F.; Teschke, O., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 10383 (2017), Springer), 9-24 · Zbl 1367.68299 |
| [27] | Carette, J.; Farmer, W. M.; Laskowski, P., HOL Light QE (2018), 19 pp. · Zbl 1511.68307 |
| [28] | Carette, J.; Farmer, W. M.; O’Connor, R., Mathscheme: project description, (Davenport, J. H.; Farmer, W. M.; Rabe, F.; Urban, J., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 6824 (2011), Springer), 287-288 · Zbl 1335.68226 |
| [29] | Carette, J.; Kiselyov, O.; Shan, C., Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages, J. Funct. Program., 19, 5, 509-543 (2009) · Zbl 1191.68158 |
| [30] | Chaieb, A.; Nipkow, T., Proof synthesis and reflection for linear arithmetic, J. Autom. Reason., 41, 33-59 (2008) · Zbl 1171.03006 |
| [31] | Chlipala, A., Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant (2013), MIT Press · Zbl 1288.68001 |
| [32] | Christiansen, D.; Brady, E., Elaborator reflection: extending Idris in Idris, SIGPLAN Not., 51, 9, 284-297 (Sep. 2016) · Zbl 1361.68035 |
| [33] | Christiansen, D. R., Type-directed elaboration of quasiquotations: a high-level syntax for low-level reflection, (Proceedings of the 26Nd 2014 International Symposium on Implementation and Application of Functional Languages. Proceedings of the 26Nd 2014 International Symposium on Implementation and Application of Functional Languages, IFL ’14 (2014), ACM: ACM New York, NY, USA), 1-9 |
| [34] | Christiansen, D. R., Practical Reflection and Metaprogramming for Dependent Types (2016), IT University of Copenhagen, Ph.D. thesis |
| [35] | Church, A., A formulation of the simple theory of types, J. Symb. Log., 5, 56-68 (1940) · JFM 66.1192.06 |
| [36] | Clavel, M.; Meseguer, J., Reflection in conditional rewriting logic, Theor. Comput. Sci., 285, 245-288 (2002) · Zbl 1001.68060 |
| [37] | Constable, R. L., Using reflection to explain and enhance type theory, (Schwichtenberg, H., Proof and Computation. Proof and Computation, NATO ASI Series, vol. 139 (1995), Springer), 109-144 · Zbl 0831.68101 |
| [38] | Constable, R. L.; Allen, S. F.; Bromley, H. M.; Cleaveland, W. R.; Cremer, J. F.; Harper, R. W.; Howe, D. J.; Knoblock, T. B.; Mendler, N. P.; Panangaden, P.; Sasaki, J. T.; Smith, S. F., Implementing Mathematics with the Nuprl Proof Development System (1986), Prentice-Hall: Prentice-Hall Englewood Cliffs, New Jersey |
| [39] | Contejean, E.; Courtieu, P.; Forest, J.; Pons, O.; Urbain, X., Certification of automated termination proofs, (Frontiers of Combining Systems. Frontiers of Combining Systems, Lecture Notes in Computer Science, vol. 4720 (2007), Springer), 148-162 · Zbl 1148.68465 |
| [40] | The Coq proof assistant reference manual, Version 8.7.2 (2018), available at |
| [41] | Coquand, T.; Huet, G., The calculus of constructions, Inf. Comput., 76, 95-120 (1988) · Zbl 0654.03045 |
| [42] | Costantini, S., Meta-reasoning: a survey, (Kakas, A. C.; Sadri, F., Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part II. Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part II, Lecture Notes in Computer Science, vol. 2408 (2002)), 253-288 · Zbl 1012.68190 |
| [43] | Davies, R.; Pfenning, F., A modal analysis of staged computation, J. ACM, 48, 555-604 (2001) · Zbl 1323.68107 |
| [44] | Demers, F.-N.; Malenfant, J., Reflection in logic, functional and object-oriented programming: a short comparative study, (IJCAI ’95 Workshop on Reflection and Metalevel Architectures and Their Applications in AI (1995)), 29-38 |
| [45] | Ebner, G.; Ullrich, S.; Roesch, J.; Avigad, J.; de Moura, L., A metaprogramming framework for formal verification, Proc. ACM Program. Lang., 1, ICFP, 34 (2017) |
| [46] | Farmer, W. M., A partial functions version of Church’s simple theory of types, J. Symb. Log., 55, 1269-1291 (1990) · Zbl 0722.03007 |
| [48] | Farmer, W. M., Theory interpretation in simple type theory, (Heering, J.; Meinke, K.; Möller, B.; Nipkow, T., Higher-Order Algebra, Logic, and Term Rewriting. Higher-Order Algebra, Logic, and Term Rewriting, Lecture Notes in Computer Science, vol. 816 (1994), Springer), 96-123 |
| [49] | Farmer, W. M., Formalizing undefinedness arising in calculus, (Basin, D.; Rusinowitch, M., Automated Reasoning—IJCAR 2004. Automated Reasoning—IJCAR 2004, Lecture Notes in Computer Science, vol. 3097 (2004), Springer), 475-489 · Zbl 1126.03303 |
| [50] | Farmer, W. M., Biform theories in Chiron, (Kauers, M.; Kerber, M.; Miner, R. R.; Windsteiger, W., Towards Mechanized Mathematical Assistants. Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science, vol. 4573 (2007), Springer), 66-79 · Zbl 1202.03025 |
| [51] | Farmer, W. M., Andrews’ type system with undefinedness, (Benzmüller, C.; Brown, C.; Siekmann, J.; Statman, R., Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday. Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday, Studies in Logic (2008), College Publications), 223-242 · Zbl 1226.03017 |
| [52] | Farmer, W. M., The seven virtues of simple type theory, J. Appl. Log., 6, 267-286 (2008) · Zbl 1149.03012 |
| [53] | Farmer, W. M., Chiron: a set theory with types, undefinedness, quotation, and evaluation (2013), 154 pp. |
| [54] | Farmer, W. M., The formalization of syntax-based mathematical algorithms using quotation and evaluation, (Carette, J.; Aspinall, D.; Lange, C.; Sojka, P.; Windsteiger, W., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 7961 (2013), Springer), 35-50 · Zbl 1390.68778 |
| [55] | Farmer, W. M., Simple type theory with undefinedness, quotation, and evaluation (2014), 87 pp. |
| [56] | Farmer, W. M., Incorporating quotation and evaluation into Church’s type theory: syntax and semantics, (Kohlhase, M.; Johansson, M.; Miller, B.; de Moura, L.; Tompa, F., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 9791 (2016), Springer), 83-98 · Zbl 1344.68204 |
| [57] | Farmer, W. M., Theory morphisms in Church’s type theory with quotation and evaluation, (Geuvers, H.; England, M.; Hasan, O.; Rabe, F.; Teschke, O., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 10383 (2017), Springer), 147-162 · Zbl 1367.68302 |
| [58] | Farmer, W. M.; Guttman, J. D.; Thayer, F. J., IMPS: an interactive mathematical proof system, J. Autom. Reason., 11, 213-248 (1993) · Zbl 0802.68129 |
| [59] | Farmer, W. M.; Guttman, J. D.; Thayer Fábrega, F. J., IMPS: an updated system description, (McRobbie, M.; Slaney, J., Automated Deduction—CADE-13. Automated Deduction—CADE-13, Lecture Notes in Computer Science, vol. 1104 (1996), Springer), 298-302 · Zbl 1412.68220 |
| [60] | Farmer, W. M.; Larjani, P., Frameworks for reasoning about syntax that utilize quotation and evaluation (2013), 38 pp. |
| [61] | Friedman, D. P.; Wand, M., Reification: reflection without metaphysics, (LISP and Functional Programming (1984)), 348-355 |
| [62] | Gabbay, M. J.; Pitts, A. M., A new approach to abstract syntax involving binders, Form. Asp. Comput., 13, 341-363 (2002) · Zbl 1001.68083 |
| [63] | Giese, M.; Buchberger, B., Towards Practical Reflection for Formal Mathematics (2007), Research Institute for Symbolic Computation (RISC), Johannes Kepler University, RISC Report Series 07-05 |
| [64] | Girard, J.-Y., Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur (1972), Université Paris 7, Ph.D. thesis |
| [65] | Glanzberg, M., Truth, (Zalta, E. N., The Stanford Encyclopedia of Philosophy (2013)) |
| [66] | Gödel, K., Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte Math. Phys., 38, 173-198 (1931) · JFM 57.0054.02 |
| [67] | Gonthier, G., The four colour theorem: engineering of a formal proof, (Kapur, D., Computer Mathematics. Computer Mathematics, ASCM 2008. Computer Mathematics. Computer Mathematics, ASCM 2008, Lecture Notes in Computer Science, vol. 5081 (2007), Springer), 333 · Zbl 1166.68346 |
| [68] | Gonthier, G.; Asperti, A.; Avigad, J.; Bertot, Y.; Cohen, C.; Garillot, F.; Roux, S. L.; Mahboubi, A.; O’Connor, R.; Biha, S. O.; Pasca, I.; Rideau, L.; Solovyev, A.; Tassi, E.; Théry, L., A machine-checked proof of the odd order theorem, (Interactive Theorem Proving. Interactive Theorem Proving, ITP 2013. Interactive Theorem Proving. Interactive Theorem Proving, ITP 2013, Lecture Notes in Computer Science, vol. 7998 (2013), Springer), 163-179 · Zbl 1317.68211 |
| [69] | Gonthier, G.; Mahboubi, A.; Tassi, E., A Small Scale Reflection Extension for the Coq System (2015), Inria Saclay Ile de France, Research Report RR-6455 |
| [70] | Gordon, M. J.C.; Melham, T. F., Introduction to HOL: A Theorem Proving Environment for Higher Order Logic (1993), Cambridge University Press · Zbl 0779.68007 |
| [71] | Grégoire, B.; Mahboubi, A., Proving equalities in a commutative ring done right in Coq, (Hurd, J.; Melham, T. F., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2005. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2005, Lecture Notes in Computer Science, vol. 3603 (2005), Springer), 98-113 · Zbl 1152.68702 |
| [72] | Grundy, J.; Melham, T.; O’Leary, J., A reflective functional language for hardware design and theorem proving, J. Funct. Program., 16 (2006) · Zbl 1086.68526 |
| [73] | Halbach, V., Axiomatic Theories of Truth (2011), Cambridge University Press · Zbl 1223.03001 |
| [74] | Halbach, V.; Leigh, G. E., Axiomatic theories of truth, (Zalta, E. N., The Stanford Encyclopedia of Philosophy (2013)) |
| [75] | Harrison, J., Metatheory and Reflection in Theorem Proving: A Survey and Critique (1995), SRI: SRI Cambridge, available at |
| [76] | Harrison, J., HOL Light: an overview, (Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 5674 (2009), Springer), 60-66 · Zbl 1252.68255 |
| [77] | Henkin, L., Completeness in the theory of types, J. Symb. Log., 15, 81-91 (1950) · Zbl 0039.00801 |
| [78] | Hickey, J.; Nogin, A.; Constable, R. L.; Aydemir, B. E.; Barzilay, E.; Bryukhov, Y.; Eaton, R.; Granicz, A.; Kopylov, A.; Kreitz, C.; Krupski, V.; Lorigo, L.; Schmitt, S.; Witty, C.; Yu, X., MetaPRL — a modular logical environment, (Basin, D.; Wolff, B., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2003. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2003, Lecture Notes in Computer Science, vol. 2758 (2003)), 287-303 |
| [79] | Howe, D., Reflecting the semantics of reflected proof, (Aczel, P.; Simmons, H.; Wainer, S., Proof Theory (1992), Cambridge University Press), 229-250 · Zbl 0808.03007 |
| [80] | James, D. W.H.; Hinze, R., A reflection-based proof tactic for lattices in Coq, (Horváth, Z.; Zsók, V.; Achten, P.; Koopman, P. W.M., Proceedings of the Tenth Symposium on Trends in Functional Programming. Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009. Proceedings of the Tenth Symposium on Trends in Functional Programming. Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Trends in Functional Programming. Intellect, vol. 10 (2009)), 97-112 |
| [81] | Jay, C. B.; Palsberg, J., Typed self-interpretation by pattern matching, (Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming. Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011 (2011)), 247-258 · Zbl 1323.68124 |
| [82] | Hunt, W. A.; Kaufmann, M.; Krug, R. B.; Moore, J. S.; Smith, E. W., Meta reasoning in ACL2, (Hurd, J.; Melham, T. F., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2005. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2005, Lecture Notes in Computer Science, vol. 3603 (2005), Springer), 163-178 · Zbl 1152.68522 |
| [83] | Kaufmann, M.; Moore, J. S., An industrial strength theorem prover for a logic based on Common Lisp, IEEE Trans. Softw. Eng., 23, 203-213 (1997) |
| [84] | Kavvos, G. A., On the semantics of intensionality and intensional recursion (Dec. 2017), available from |
| [85] | Knoblock, T. B.; Constable, R. L., Formalized metareasoning in type theory, (Proceedings of the Symposium on Logic in Computer Science. Proceedings of the Symposium on Logic in Computer Science, LICS ’86 (1986), IEEE Computer Society), 237-248 |
| [86] | Koellner, P., On reflection principles, Ann. Pure Appl. Log., 157, 206-219 (2009) · Zbl 1162.03030 |
| [87] | Leitgeb, H., What theories of truth should be like (but cannot be), Philos. Compass, 2, 276-290 (2007) |
| [88] | Martin-Löf, P., Intuitionistic Type Theory (1984), Bibliopolis · Zbl 0571.03030 |
| [89] | Melham, T.; Cohn, R.; Childs, I., On the semantics of ReFLect as a basis for a reflective theorem prover (2013), Computing Research Repository (CoRR) |
| [90] | Mendhekar, A.; Friedman, D. P., An exploration of relationships between reflective theories, (Proceedings. Proceedings, Reflect., vol. 96 (Apr. 1996)), 233-250 |
| [91] | Miller, D., Abstract syntax for variable binders: an overview, (Lloyd, J.; etal., Computational Logic — CL 2000. Computational Logic — CL 2000, Lecture Notes in Computer Science, vol. 1861 (2000), Springer), 239-253 · Zbl 0983.68036 |
| [92] | Mogensen, T. A., Efficient self-interpretation in lambda calculus, J. Funct. Program., 2, 345-364 (1994) |
| [93] | Moggi, E.; Fagorzi, S., A monadic multi-stage metalanguage, (Gordon, A. D., Foundations of Software Science and Computational Structures. Foundations of Software Science and Computational Structures, FOSSACS 2003. Foundations of Software Science and Computational Structures. Foundations of Software Science and Computational Structures, FOSSACS 2003, Lecture Notes in Computer Science, vol. 2620 (2003), Springer), 358-374 · Zbl 1029.68042 |
| [94] | Nanevski, A.; Pfenning, F., Staged computation with names and necessity, J. Funct. Program., 15, 893-939 (2005) · Zbl 1085.68025 |
| [95] | Nanevski, A.; Pfenning, F.; Pientka, B., Contextual modal type theory, ACM Trans. Comput. Log., 9 (2008) · Zbl 1367.03060 |
| [96] | Nogin, A.; Kopylov, A.; Yu, X.; Hickey, J., A computational approach to reflective meta-reasoning about languages with bindings, (Pollack, R., ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized Reasoning about Languages with Variable Binding. ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN 2005 (2005), ACM), 2-12 |
| [97] | Norell, U., Towards a Practical Programming Language Based on Dependent Type Theory (2007), Chalmers University of Technology, Ph.D. thesis |
| [98] | Norell, U., Dependently typed programming in Agda, (Kennedy, A.; Ahmed, A., Proceedings of TLDI’09 (2009), ACM), 1-2 · Zbl 1263.68038 |
| [99] | Odersky, M.; Spoon, L.; Venners, B., Programming in Scala (2016), Artima |
| [100] | Oostdijk, M.; Geuvers, H., Proof by computation in the Coq system, Theor. Comput. Sci., 272 (2002) · Zbl 0984.68137 |
| [101] | Pfenning, F.; Elliot, C., Higher-order abstract syntax, (Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (1988), ACM Press), 199-208 |
| [102] | Pitts, A. M., Nominal logic, a first order theory of names and binding, Inf. Comput., 186, 165-193 (2003) · Zbl 1056.03014 |
| [103] | Plataformatec, Elixir (2018) |
| [104] | Polonsky, A., Axiomatizing the quote, (Bezem, M., Computer Science Logic (CSL’11) — 25th International Workshop/20th Annual Conference of the EACSL. Computer Science Logic (CSL’11) — 25th International Workshop/20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs), vol. 12 (2011), Schloss Dagstuhl — Leibniz-Zentrum für Informatik), 458-469 · Zbl 1247.03022 |
| [105] | Quine, W. V.O., Mathematical Logic (2003), Harvard University Press · JFM 66.0027.03 |
| [106] | Rabe, F., Generic literals, (Kerber, M.; Carette, J.; Kaliszyk, C.; Rabe, F.; Sorge, V., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 9150 (2015), Springer), 102-117 · Zbl 1417.68216 |
| [107] | Rendel, T.; Ostermann, K.; Hofer, C., Typed self-representation, SIGPLAN Not., 44, 6, 293-303 (Jun. 2009) |
| [108] | Reynolds, J. C., Towards a theory of type structure, (Robinet, B., Programming Symposium. Programming Symposium, Lecture Notes in Computer Science, vol. 19 (1974), Springer), 408-425 · Zbl 0309.68016 |
| [109] | MetaOCaml: a compiled, type-safe, multi-stage programming language (2011) |
| [110] | Scalameta Project, Scalameta (2018) |
| [111] | Sheard, T.; Jones, S. P., Template meta-programming for Haskell, ACM SIGPLAN Not., 37, 60-75 (2002) |
| [112] | Spivak, M., Calculus (2008), Publish or Perish · Zbl 0159.34302 |
| [113] | Stump, A., Directly reflective meta-programming, High.-Order Symb. Comput., 22, 115-144 (2009) · Zbl 1183.68164 |
| [114] | Taha, W., A gentle introduction to multi-stage programming, (Lengauer, C.; Batory, D.; Consel, C.; Odersky, M., Domain-Specific Program Generation. Domain-Specific Program Generation, Lecture Notes in Computer Science, vol. 3016 (2004), Springer), 30-50 |
| [115] | Taha, W.; Sheard, T., MetaML and multi-stage programming with explicit annotations, Theor. Comput. Sci., 248, 211-242 (2000) · Zbl 0949.68047 |
| [116] | Tarski, A., Pojęcie prawdy w językach nauk dedukcyjnych, Pr. Tow. Nauk. Warsz., 3, 34 (1933) |
| [117] | Tarski, A., Der Wahrheitsbegriff in den formalisierten Sprachen, Stud. Philos., 1, 261-405 (1935) · Zbl 0013.28903 |
| [118] | Tarski, A., The concept of truth in formalized languages, (Corcoran, J., Logic, Semantics, Meta-Mathematics (1983), Hackett), 152-278 |
| [119] | (2018), The F# Software Foundation |
| [120] | van der Walt, P., Reflection in Agda (2012), Universiteit Utrecht, Master’s thesis |
| [121] | van der Walt, P.; Swierstra, W., Engineering proof by reflection in Agda, (Hinze, R., Implementation and Application of Functional Languages. Implementation and Application of Functional Languages, Lecture Notes in Computer Science, vol. 8241 (2012), Springer), 157-173 |
| [122] | von Henke, F. W.; Pfab, S.; Pfeifer, H.; Rueß, H., Case studies in meta-level theorem proving, (Grundy, J.; Newey, M., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs’98, vol. 1479 (1998), Springer), 461-478 |
| [123] | Wand, M., The theory of fexprs is trivial, LISP Symb. Comput., 10, 3, 189-199 (1998) |
| [124] | Wildmoser, M.; Nipkow, T., Certifying machine code safety: shallow versus deep embedding, (Slind, K.; Bunker, A.; Gopalakrishnan, G., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2004. Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, TPHOLs 2004, Lecture Notes in Computer Science, vol. 3223 (2004), Springer), 305-320 · Zbl 1099.68545 |
| [125] | Yu, X., Reflection and its Application to Mechanized Metareasoning About Programming Languages (2007), California Institute of Technology, Ph.D. thesis |
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.
