Hu, Jason Z. S.; Jang, Junyoung; Pientka, Brigitte Normalization by evaluation for modal dependent type theory. (English) Zbl 07775446 J. Funct. Program. 33, Paper No. e7, 51 p. (2023). MSC: 68N18 PDFBibTeX XMLCite \textit{J. Z. S. Hu} et al., J. Funct. Program. 33, Paper No. e7, 51 p. (2023; Zbl 07775446) Full Text: DOI OA License
Popescu, Andrei Rensets and renaming-based recursion for syntax with bindings extended version. (English) Zbl 07722430 J. Autom. Reasoning 67, No. 3, Paper No. 23, 27 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Popescu}, J. Autom. Reasoning 67, No. 3, Paper No. 23, 27 p. (2023; Zbl 07722430) Full Text: DOI
Popescu, Andrei Rensets and renaming-based recursion for syntax with bindings. (English) Zbl 07628212 Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 618-639 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Popescu}, Lect. Notes Comput. Sci. 13385, 618--639 (2022; Zbl 07628212) Full Text: DOI arXiv
Kavvos, G. A. Dual-context calculi for modal logic. (English) Zbl 07243672 Log. Methods Comput. Sci. 16, No. 3, Paper No. 10, 66 p. (2020). MSC: 03B45 PDFBibTeX XMLCite \textit{G. A. Kavvos}, Log. Methods Comput. Sci. 16, No. 3, Paper No. 10, 66 p. (2020; Zbl 07243672) Full Text: arXiv Link
Gheri, Lorenzo; Popescu, Andrei A formalized general theory of syntax with bindings: extended version. (English) Zbl 1468.68073 J. Autom. Reasoning 64, No. 4, 641-675 (2020). MSC: 68N30 68Q60 68V20 PDFBibTeX XMLCite \textit{L. Gheri} and \textit{A. Popescu}, J. Autom. Reasoning 64, No. 4, 641--675 (2020; Zbl 1468.68073) Full Text: DOI
Jay, Barry Self-quotation in a typed, intensional lambda-calculus. (English) Zbl 1525.68017 Silva, Alexandra (ed.), Proceedings of the 33rd conference on the mathematical foundations of programming semantics (MFPS XXXIII), Ljubljana, Slovenia, June 12–15, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 336, 207-222 (2018). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{B. Jay}, Electron. Notes Theor. Comput. Sci. 336, 207--222 (2018; Zbl 1525.68017) Full Text: DOI
Stump, Aaron The calculus of dependent lambda eliminations. (English) Zbl 1418.68038 J. Funct. Program. 27, Paper No. e14, 41 p. (2017). MSC: 68N18 PDFBibTeX XMLCite \textit{A. Stump}, J. Funct. Program. 27, Paper No. e14, 41 p. (2017; Zbl 1418.68038) Full Text: DOI
Dowek, Gilles; Gabbay, Murdoch J. PNL to HOL: from the logic of nominal sets to the logic of higher-order functions. (English) Zbl 1309.03013 Theor. Comput. Sci. 451, 38-69 (2012). MSC: 03B70 68N18 PDFBibTeX XMLCite \textit{G. Dowek} and \textit{M. J. Gabbay}, Theor. Comput. Sci. 451, 38--69 (2012; Zbl 1309.03013) Full Text: DOI arXiv
Felty, Amy; Momigliano, Alberto Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. (English) Zbl 1252.68252 J. Autom. Reasoning 48, No. 1, 43-105 (2012). MSC: 68T15 03B70 PDFBibTeX XMLCite \textit{A. Felty} and \textit{A. Momigliano}, J. Autom. Reasoning 48, No. 1, 43--105 (2012; Zbl 1252.68252) Full Text: DOI
Pitts, Andrew M. Structural recursion with locally scoped names. (English) Zbl 1271.68079 J. Funct. Program. 21, No. 3, 235-286 (2011). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{A. M. Pitts}, J. Funct. Program. 21, No. 3, 235--286 (2011; Zbl 1271.68079) Full Text: DOI
Cheney, James A simple nominal type theory. (English) Zbl 1337.03039 Abel, Andreas (ed.) et al., Proceedings of the 3rd international workshop on logical frameworks and metalanguages: theory and practice (LFMTP 2008), Pittsburgh, PA, USA, June 23, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 228, 37-52 (2009). MSC: 03B70 03B40 PDFBibTeX XMLCite \textit{J. Cheney}, Electron. Notes Theor. Comput. Sci. 228, 37--52 (2009; Zbl 1337.03039) Full Text: DOI
Washburn, Geoffrey; Weirich, Stephanie Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism. (English) Zbl 1128.68021 J. Funct. Program. 18, No. 1, 87-140 (2008). MSC: 68N18 PDFBibTeX XMLCite \textit{G. Washburn} and \textit{S. Weirich}, J. Funct. Program. 18, No. 1, 87--140 (2008; Zbl 1128.68021) Full Text: DOI
Vestergaard, René; Brotherston, James A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (English) Zbl 1054.68028 Inf. Comput. 183, No. 2, 212-244 (2003). MSC: 68N18 03B40 68T15 PDFBibTeX XMLCite \textit{R. Vestergaard} and \textit{J. Brotherston}, Inf. Comput. 183, No. 2, 212--244 (2003; Zbl 1054.68028) Full Text: DOI
Snyder, Wayne; Gallier, Jean Higher-order unification revisited: Complete sets of transformations. (English) Zbl 0682.03034 J. Symb. Comput. 8, No. 1-2, 101-140 (1989). Reviewer: N.Zamov MSC: 03F35 03B35 PDFBibTeX XMLCite \textit{W. Snyder} and \textit{J. Gallier}, J. Symb. Comput. 8, No. 1--2, 101--140 (1989; Zbl 0682.03034) Full Text: DOI