Weber, Matthias An extended type system with lambda-typed lambda-expressions. (English) Zbl 1516.03007 Log. Methods Comput. Sci. 16, No. 4, Paper No. 12, 50 p. (2020). MSC: 03B40 PDFBibTeX XMLCite \textit{M. Weber}, Log. Methods Comput. Sci. 16, No. 4, Paper No. 12, 50 p. (2020; Zbl 1516.03007) Full Text: arXiv Link
Ehrhard, Thomas An introduction to differential linear logic: proof-nets, models and antiderivatives. (English) Zbl 1456.03097 Math. Struct. Comput. Sci. 28, No. 7, 995-1060 (2018). MSC: 03F52 PDFBibTeX XMLCite \textit{T. Ehrhard}, Math. Struct. Comput. Sci. 28, No. 7, 995--1060 (2018; Zbl 1456.03097) Full Text: DOI arXiv
Kesner, Delia; Renaud, Fabien A prismoid framework for languages with resources. (English) Zbl 1231.68103 Theor. Comput. Sci. 412, No. 37, 4867-4892 (2011). MSC: 68N18 03B40 03F52 PDFBibTeX XMLCite \textit{D. Kesner} and \textit{F. Renaud}, Theor. Comput. Sci. 412, No. 37, 4867--4892 (2011; Zbl 1231.68103) Full Text: DOI
Gabbay, Murdoch J.; Mulligan, Dominic P. Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms. (English) Zbl 1186.68102 Inf. Comput. 208, No. 3, 230-258 (2010); corrigendum ibid. 212, 119 (2012). MSC: 68N18 PDFBibTeX XMLCite \textit{M. J. Gabbay} and \textit{D. P. Mulligan}, Inf. Comput. 208, No. 3, 230--258 (2010; Zbl 1186.68102) Full Text: DOI
Ehrhard, Thomas; Regnier, Laurent Uniformity and the Taylor expansion of ordinary lambda-terms. (English) Zbl 1154.68354 Theor. Comput. Sci. 403, No. 2-3, 347-372 (2008). MSC: 68N18 PDFBibTeX XMLCite \textit{T. Ehrhard} and \textit{L. Regnier}, Theor. Comput. Sci. 403, No. 2--3, 347--372 (2008; Zbl 1154.68354) Full Text: DOI HAL
Jojgov, Gueorgui Tactics and parameters. (English) Zbl 1264.03042 Dahn, Ingo (ed.) et al., Proceedings of the workshop on mathematics, logic and computation (satellite event of ICALP 2003), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 85, No. 7, 50-68 (2003). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{G. Jojgov}, Electron. Notes Theor. Comput. Sci. 85, No. 7, 50--68 (2003; Zbl 1264.03042) Full Text: DOI
Duggan, Dominic Higher-order substitutions. (English) Zbl 1003.68024 Inf. Comput. 164, No. 1, 1-53 (2001). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{D. Duggan}, Inf. Comput. 164, No. 1, 1--53 (2001; Zbl 1003.68024) Full Text: DOI Link
Kamareddine, Fairouz; Nederpelt, Rob A useful \(\lambda\)-notation. (English) Zbl 0873.03018 Theor. Comput. Sci. 155, No. 1, 85-109 (1996). MSC: 03B40 68Q55 03B70 PDFBibTeX XMLCite \textit{F. Kamareddine} and \textit{R. Nederpelt}, Theor. Comput. Sci. 155, No. 1, 85--109 (1996; Zbl 0873.03018) Full Text: DOI
Pollack, Robert On extensibility of proof checkers. (English) Zbl 07774803 Dybjer, Peter (ed.) et al., Types for proofs and programs. International workshop TYPES ’94, Båstad, Sweden, June 6–10, 1994. Selected papers. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 996, 140-161 (1995). MSC: 68V15 PDFBibTeX XMLCite \textit{R. Pollack}, Lect. Notes Comput. Sci. 996, 140--161 (1995; Zbl 07774803) Full Text: DOI
Pollack, Randy Closure under alpha-conversion. (English) Zbl 1527.03013 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 313-332 (1994). MSC: 03B40 PDFBibTeX XMLCite \textit{R. Pollack}, Lect. Notes Comput. Sci. 806, 313--332 (1994; Zbl 1527.03013) Full Text: DOI
Magnusson, Lena; Nordström, Bengt The ALF proof editor and its proof engine. (English) Zbl 1527.68259 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 213-237 (1994). MSC: 68V15 PDFBibTeX XMLCite \textit{L. Magnusson} and \textit{B. Nordström}, Lect. Notes Comput. Sci. 806, 213--237 (1994; Zbl 1527.68259) Full Text: DOI
de Bruijn, N. G. Telescopic mappings in typed lambda calculus. (English) Zbl 0723.68024 Inf. Comput. 91, No. 2, 189-204 (1991). MSC: 68N15 03B40 PDFBibTeX XMLCite \textit{N. G. de Bruijn}, Inf. Comput. 91, No. 2, 189--204 (1991; Zbl 0723.68024) Full Text: DOI
Luo, Zhaohui A higher-order calculus and theory abstraction. (English) Zbl 0719.03004 Inf. Comput. 90, No. 1, 107-137 (1991). Reviewer: Z.Luo MSC: 03B15 03F35 68Q60 03B70 PDFBibTeX XMLCite \textit{Z. Luo}, Inf. Comput. 90, No. 1, 107--137 (1991; Zbl 0719.03004) Full Text: DOI
Coquand, Thierry; Huet, Gérard The calculus of constructions. (English) Zbl 0654.03045 Inf. Comput. 76, No. 2-3, 95-120 (1988). Reviewer: T.Coquand MSC: 03F35 03B40 68N01 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{G. Huet}, Inf. Comput. 76, No. 2--3, 95--120 (1988; Zbl 0654.03045) Full Text: DOI
Coquand, Thierry; Huet, Gérard A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction. (English) Zbl 0591.68036 J. Symb. Comput. 1, 323-328 (1985). MSC: 68Q65 68Q60 03Fxx 03B35 03B15 03B40 03F55 68T15 00A15 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{G. Huet}, J. Symb. Comput. 1, 323--328 (1985; Zbl 0591.68036) Full Text: DOI