Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro Formalization of metatheory of the lambda calculus in constructive type theory using the barendregt variable convention. (English) Zbl 07460121 Math. Struct. Comput. Sci. 31, No. 3, 341-360 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{E. Copello} et al., Math. Struct. Comput. Sci. 31, No. 3, 341--360 (2021; Zbl 07460121) Full Text: DOI OpenURL
Faggian, Claudia; Guerrieri, Giulio Factorization in call-by-name and call-by-value calculi via linear logic. (English) Zbl 07410426 Kiefer, Stefan (ed.) et al., Foundations of software science and computation structures. 24th international conference, FOSSACS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12650, 205-225 (2021). MSC: 68Nxx 68Qxx PDF BibTeX XML Cite \textit{C. Faggian} and \textit{G. Guerrieri}, Lect. Notes Comput. Sci. 12650, 205--225 (2021; Zbl 07410426) Full Text: DOI arXiv OpenURL
de’Liguoro, Ugo; Treglia, Riccardo The untyped computational \(\lambda \)-calculus and its intersection type discipline. (English) Zbl 1464.68056 Theor. Comput. Sci. 846, 141-159 (2020). MSC: 68N18 03B40 18C15 PDF BibTeX XML Cite \textit{U. de'Liguoro} and \textit{R. Treglia}, Theor. Comput. Sci. 846, 141--159 (2020; Zbl 1464.68056) Full Text: DOI Link OpenURL
Dal Lago, Ugo; Guerrieri, Giulio; Heijltjes, Willem Decomposing probabilistic lambda calculi. (English) Zbl 07250936 Goubault-Larrecq, Jean (ed.) et al., Foundations of software science and computation structures. 23rd international conference, FOSSACS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12077, 136-156 (2020). MSC: 68Nxx 68Qxx PDF BibTeX XML Cite \textit{U. Dal Lago} et al., Lect. Notes Comput. Sci. 12077, 136--156 (2020; Zbl 07250936) Full Text: DOI arXiv OpenURL
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 PDF BibTeX XML Cite \textit{G. A. Kavvos}, Log. Methods Comput. Sci. 16, No. 3, Paper No. 10, 66 p. (2020; Zbl 07243672) Full Text: arXiv Link OpenURL
Fujita, Ken-etsu A formal system of reduction paths for parallel reduction. (English) Zbl 1433.68190 Theor. Comput. Sci. 813, 327-340 (2020). MSC: 68Q42 03B40 68R10 PDF BibTeX XML Cite \textit{K.-e. Fujita}, Theor. Comput. Sci. 813, 327--340 (2020; Zbl 1433.68190) Full Text: DOI OpenURL
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 PDF BibTeX XML Cite \textit{L. Gheri} and \textit{A. Popescu}, J. Autom. Reasoning 64, No. 4, 641--675 (2020; Zbl 1468.68073) Full Text: DOI OpenURL
Guerrieri, Giulio; Manzonetto, Giulio The bang calculus and the two Girard’s translations. (English) Zbl 07450000 Ehrhard, Thomas (ed.) et al., Proceedings of the joint international workshop on linearity & trends in linear logic and applications, Linearity-TLLA 2018, Oxford, UK, July 7–8, 2018. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 292, 15-30 (2019). MSC: 03F52 03B40 68N18 PDF BibTeX XML Cite \textit{G. Guerrieri} and \textit{G. Manzonetto}, Electron. Proc. Theor. Comput. Sci. (EPTCS) 292, 15--30 (2019; Zbl 07450000) Full Text: arXiv Link OpenURL
Leventis, Thomas A deterministic rewrite system for the probabilistic \(\lambda\)-calculus. (English) Zbl 1434.68091 Math. Struct. Comput. Sci. 29, No. 10, 1479-1512 (2019). MSC: 68N18 03B40 68Q55 PDF BibTeX XML Cite \textit{T. Leventis}, Math. Struct. Comput. Sci. 29, No. 10, 1479--1512 (2019; Zbl 1434.68091) Full Text: DOI OpenURL
Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory. (English) Zbl 1433.68542 Alves, Sandra (ed.) et al., Selected papers of the 12th workshop on logical and semantic frameworks, with applications (LSFA 2017), Brasilia, Brazil, September 23–24, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 338, 79-95 (2018). MSC: 68V15 03B35 03B38 03B40 PDF BibTeX XML Cite \textit{E. Copello} et al., Electron. Notes Theor. Comput. Sci. 338, 79--95 (2018; Zbl 1433.68542) Full Text: DOI OpenURL
Fujita, Ken-etsu The Church-Rosser theorem and quantitative analysis of witnesses. (English) Zbl 1436.03104 Inf. Comput. 263, 52-56 (2018). MSC: 03B40 PDF BibTeX XML Cite \textit{K.-e. Fujita}, Inf. Comput. 263, 52--56 (2018; Zbl 1436.03104) Full Text: DOI OpenURL
Ishii, Katsumasa A proof of the leftmost reduction theorem for \(\lambda\beta\eta\)-calculus. (English) Zbl 1436.03105 Theor. Comput. Sci. 747, 26-32 (2018). MSC: 03B40 PDF BibTeX XML Cite \textit{K. Ishii}, Theor. Comput. Sci. 747, 26--32 (2018; Zbl 1436.03105) Full Text: DOI OpenURL
Rocha-Oliveira, Ana Cristina; Galdino, André Luiz; Ayala-Rincón, Mauricio Confluence of orthogonal term rewriting systems in the prototype verification system. (English) Zbl 1407.68441 J. Autom. Reasoning 58, No. 2, 231-251 (2017). MSC: 68T15 68N30 68Q42 PDF BibTeX XML Cite \textit{A. C. Rocha-Oliveira} et al., J. Autom. Reasoning 58, No. 2, 231--251 (2017; Zbl 1407.68441) Full Text: DOI OpenURL
Copello, Ernesto; Szasz, Nora; Tasistro, Álvaro Formal metatheory of the lambda calculus using Stoughton’s substitution. (English) Zbl 1383.03021 Theor. Comput. Sci. 685, 65-82 (2017). Reviewer: Martin W. Bunder (Wollongong) MSC: 03B40 PDF BibTeX XML Cite \textit{E. Copello} et al., Theor. Comput. Sci. 685, 65--82 (2017; Zbl 1383.03021) Full Text: DOI OpenURL
Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald Certifying confluence proofs via relative termination and rule labeling. (English) Zbl 1398.68485 Log. Methods Comput. Sci. 13, No. 2, Paper No. 4, 27 p. (2017). MSC: 68T15 68Q42 PDF BibTeX XML Cite \textit{J. Nagele} et al., Log. Methods Comput. Sci. 13, No. 2, Paper No. 4, 27 p. (2017; Zbl 1398.68485) Full Text: DOI arXiv OpenURL
Klin, Bartek; Szynwelski, Michał SMT solving for functional programming over infinite structures. (English) Zbl 1477.68072 Atkey, Robert (ed.) et al., Proceedings of the sixth workshop on mathematically structured functional programming, MSFP 2016, Eindhoven, Netherlands, April 8, 2016. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 207, 57-75 (2016). MSC: 68N18 PDF BibTeX XML Cite \textit{B. Klin} and \textit{M. Szynwelski}, Electron. Proc. Theor. Comput. Sci. (EPTCS) 207, 57--75 (2016; Zbl 1477.68072) Full Text: arXiv Link OpenURL
Inoue, Jun; Taha, Walid Reasoning about multi-stage programs. (English) Zbl 1420.68040 J. Funct. Program. 26, Paper No. e22, 53 p. (2016). MSC: 68N18 68N30 PDF BibTeX XML Cite \textit{J. Inoue} and \textit{W. Taha}, J. Funct. Program. 26, Paper No. e22, 53 p. (2016; Zbl 1420.68040) Full Text: DOI OpenURL
Nakazawa, Koji; Fujita, Ken-etsu Compositional Z: confluence proofs for permutative conversion. (English) Zbl 1368.03020 Stud. Log. 104, No. 6, 1205-1224 (2016). Reviewer: Martin W. Bunder (Wollongong) MSC: 03B40 PDF BibTeX XML Cite \textit{K. Nakazawa} and \textit{K.-e. Fujita}, Stud. Log. 104, No. 6, 1205--1224 (2016; Zbl 1368.03020) Full Text: DOI OpenURL
McBride, Conor I got plenty o’ nuttin’. (English) Zbl 1343.68060 Lindley, Sam (ed.) et al., A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday. Cham: Springer (ISBN 978-3-319-30935-4/pbk; 978-3-319-30936-1/ebook). Lecture Notes in Computer Science 9600, 207-233 (2016). MSC: 68N30 03B70 03F52 68N18 PDF BibTeX XML Cite \textit{C. McBride}, Lect. Notes Comput. Sci. 9600, 207--233 (2016; Zbl 1343.68060) Full Text: DOI OpenURL
Blanqui, Frédéric Termination of rewrite relations on \(\lambda\)-terms based on Girard’s notion of reducibility. (English) Zbl 1332.68103 Theor. Comput. Sci. 611, 50-86 (2016). MSC: 68Q42 03B40 PDF BibTeX XML Cite \textit{F. Blanqui}, Theor. Comput. Sci. 611, 50--86 (2016; Zbl 1332.68103) Full Text: DOI arXiv OpenURL
Guerrieri, Giulio Head reduction and normalization in a call-by-value lambda-calculus. (English) Zbl 1428.68100 Chiba, Yuki (ed.) et al., Second international workshop on rewriting techniques for program transformations and evaluation, WPTE’15, Warsaw, Poland, July 2, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. OASIcs – OpenAccess Ser. Inform. 46, 3-17 (2015). MSC: 68N18 PDF BibTeX XML Cite \textit{G. Guerrieri}, OASIcs -- OpenAccess Ser. Inform. 46, 3--17 (2015; Zbl 1428.68100) Full Text: DOI OpenURL
Komori, Yuichi; Matsuda, Naosuke; Yamakawa, Fumika A simplified proof of the Church-Rosser theorem. (English) Zbl 1338.03017 Stud. Log. 102, No. 1, 175-183 (2014). MSC: 03B40 PDF BibTeX XML Cite \textit{Y. Komori} et al., Stud. Log. 102, No. 1, 175--183 (2014; Zbl 1338.03017) Full Text: DOI OpenURL
Hillenbrand, Thomas; Piskac, Ruzica; Waldmann, Uwe; Weidenbach, Christoph From search to computation: redundancy criteria and simplification at work. (English) Zbl 1383.68076 Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 169-193 (2013). MSC: 68T15 03B35 68Q42 PDF BibTeX XML Cite \textit{T. Hillenbrand} et al., Lect. Notes Comput. Sci. 7797, 169--193 (2013; Zbl 1383.68076) Full Text: DOI OpenURL
Blanqui, Frédéric; Kirchner, Claude; Riba, Colin On the confluence of lambda-calculus with conditional rewriting. (English) Zbl 1209.68104 Theor. Comput. Sci. 411, No. 37, 3301-3327 (2010). MSC: 68N18 68Q42 PDF BibTeX XML Cite \textit{F. Blanqui} et al., Theor. Comput. Sci. 411, No. 37, 3301--3327 (2010; Zbl 1209.68104) Full Text: DOI arXiv OpenURL
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 PDF BibTeX XML Cite \textit{M. J. Gabbay} and \textit{D. P. Mulligan}, Inf. Comput. 208, No. 3, 230--258 (2010; Zbl 1186.68102) Full Text: DOI OpenURL
Gabbay, Murdoch J.; Lengrand, Stéphane The lambda-context calculus (extended version). (English) Zbl 1192.68137 Inf. Comput. 207, No. 12, 1369-1400 (2009). MSC: 68N18 PDF BibTeX XML Cite \textit{M. J. Gabbay} and \textit{S. Lengrand}, Inf. Comput. 207, No. 12, 1369--1400 (2009; Zbl 1192.68137) Full Text: DOI Link OpenURL
Urban, Christian Nominal techniques in Isabelle/HOL. (English) Zbl 1140.68061 J. Autom. Reasoning 40, No. 4, 327-356 (2008). MSC: 68T15 03B40 PDF BibTeX XML Cite \textit{C. Urban}, J. Autom. Reasoning 40, No. 4, 327--356 (2008; Zbl 1140.68061) Full Text: DOI OpenURL
Nakazawa, Koji; Tatsuta, Makoto Strong normalization of classical natural deduction with disjunctions. (English) Zbl 1141.03027 Ann. Pure Appl. Logic 153, No. 1-3, 21-37 (2008). Reviewer: M. Yasuhara (Princeton) MSC: 03F05 03B05 03B40 PDF BibTeX XML Cite \textit{K. Nakazawa} and \textit{M. Tatsuta}, Ann. Pure Appl. Logic 153, No. 1--3, 21--37 (2008; Zbl 1141.03027) Full Text: DOI OpenURL
Cirstea, Horatiu; Houtmann, Clément; Wack, Benjamin Distributive \(\rho\)-calculus. (English) Zbl 1279.03057 Denker, Grit (ed.) et al., Proceedings of the 6th international workshop on rewriting logic and its applications (WRLA 2006), Vienna, Austria, April 1–2, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 176, No. 4, 95-111 (2007). MSC: 03B70 03B40 68Q42 PDF BibTeX XML Cite \textit{H. Cirstea} et al., Electron. Notes Theor. Comput. Sci. 176, No. 4, 95--111 (2007; Zbl 1279.03057) Full Text: DOI OpenURL
Faure, Germain Term collections in {\(\lambda\)} and {\(\rho\)}-calculi. (English) Zbl 1277.03010 Jouannaud, Jean-Pierre (ed.) et al., Proceedings of the second international workshop on developments in computational models (DCM 2006), Venice, Italy, July 16, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 171, No. 3, 3-19 (2007). MSC: 03B40 68Q42 68Q55 PDF BibTeX XML Cite \textit{G. Faure}, Electron. Notes Theor. Comput. Sci. 171, No. 3, 3--19 (2007; Zbl 1277.03010) Full Text: DOI OpenURL
Minari, Pierluigi Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters. (English) Zbl 1117.03020 Arch. Math. Logic 46, No. 5-6, 385-424 (2007). Reviewer: Reinhard Kahle (Coimbra) MSC: 03B40 03F03 03F05 03F07 PDF BibTeX XML Cite \textit{P. Minari}, Arch. Math. Logic 46, No. 5--6, 385--424 (2007; Zbl 1117.03020) Full Text: DOI OpenURL
Matthes, Ralph Non-strictly positive fixed points for classical natural deduction. (English) Zbl 1066.03057 Ann. Pure Appl. Logic 133, No. 1-3, 205-230 (2005). Reviewer: M. Yasuhara (Princeton) MSC: 03F05 03B40 68N18 PDF BibTeX XML Cite \textit{R. Matthes}, Ann. Pure Appl. Logic 133, No. 1--3, 205--230 (2005; Zbl 1066.03057) Full Text: DOI OpenURL
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 PDF BibTeX XML Cite \textit{G. Jojgov}, Electron. Notes Theor. Comput. Sci. 85, No. 7, 50--68 (2003; Zbl 1264.03042) Full Text: DOI OpenURL
Compagnoni, Adriana; Goguen, Healfdene Typed operational semantics for higher-order subtyping. (English) Zbl 1055.68075 Inf. Comput. 184, No. 2, 242-297 (2003). MSC: 68Q55 PDF BibTeX XML Cite \textit{A. Compagnoni} and \textit{H. Goguen}, Inf. Comput. 184, No. 2, 242--297 (2003; Zbl 1055.68075) Full Text: DOI OpenURL
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 PDF BibTeX XML Cite \textit{R. Vestergaard} and \textit{J. Brotherston}, Inf. Comput. 183, No. 2, 212--244 (2003; Zbl 1054.68028) Full Text: DOI OpenURL
Tsuiki, Hideki A domain-theoretic semantics of lax generic functions. (English) Zbl 1051.68046 Theor. Comput. Sci. 294, No. 1-2, 307-331 (2003). MSC: 68N18 PDF BibTeX XML Cite \textit{H. Tsuiki}, Theor. Comput. Sci. 294, No. 1--2, 307--331 (2003; Zbl 1051.68046) Full Text: DOI OpenURL
Andou, Y. Church-Rosser property of a simple reduction for full first-order classical natural deduction. (English) Zbl 1016.03006 Ann. Pure Appl. Logic 119, No. 1-3, 225-237 (2003). MSC: 03B10 03B40 03F05 PDF BibTeX XML Cite \textit{Y. Andou}, Ann. Pure Appl. Logic 119, No. 1--3, 225--237 (2003; Zbl 1016.03006) Full Text: DOI OpenURL
Neergaard, Peter Møller; Sørensen, Morten Heine Conservation and uniform normalization in lambda calculi with erasing reductions. (English) Zbl 1012.03022 Inf. Comput. 178, No. 1, 149-179 (2002). MSC: 03B40 68N18 PDF BibTeX XML Cite \textit{P. M. Neergaard} and \textit{M. H. Sørensen}, Inf. Comput. 178, No. 1, 149--179 (2002; Zbl 1012.03022) Full Text: DOI OpenURL
Vestergaard, René; Brotherston, James The mechanisation of Barendregt-style equational proofs (the residual perspective). (English) Zbl 1268.68057 Ambler, S. J. (ed.) et al., MERLIN 2001. Proceedings of the workshop on mechanized reasoning about languages with variable binding (in connection with IJCAR 2001), Siena, Italy, June 18, 2001. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 58, No. 1, 18-36 (2001). MSC: 68N18 68T15 PDF BibTeX XML Cite \textit{R. Vestergaard} and \textit{J. Brotherston}, Electron. Notes Theor. Comput. Sci. 58, No. 1, 18--36 (2001; Zbl 1268.68057) Full Text: DOI OpenURL
Hashimoto, M.; Ohori, A. A typed context calculus. (English) Zbl 0989.68017 Theor. Comput. Sci. 266, No. 1-2, 249-272 (2001). MSC: 68N18 PDF BibTeX XML Cite \textit{M. Hashimoto} and \textit{A. Ohori}, Theor. Comput. Sci. 266, No. 1--2, 249--272 (2001; Zbl 0989.68017) Full Text: DOI OpenURL
Bethke, Inge; Klop, Jan Willem; de Vrijer, Roel Descendants and origins in term rewriting. (English) Zbl 1046.68564 Inf. Comput. 159, No. 1-2, 59-124 (2000). MSC: 68Q42 03B40 PDF BibTeX XML Cite \textit{I. Bethke} et al., Inf. Comput. 159, No. 1--2, 59--124 (2000; Zbl 1046.68564) Full Text: DOI Link OpenURL
Larson, Jean A. (ed.) 1999–2000 Winter Meeting of the Association for Symbolic Logic, Washington, DC, January 21–23, 2000. (English) Zbl 0952.03501 Bull. Symb. Log. 6, No. 2, 232-247 (2000). MSC: 03-06 PDF BibTeX XML Cite \textit{J. A. Larson} (ed.), Bull. Symb. Log. 6, No. 2, 232--247 (2000; Zbl 0952.03501) Full Text: DOI Link OpenURL
Matthes, Ralph Monotone (co)inductive types and positive fixed-point types. (English) Zbl 0940.03018 Theor. Inform. Appl. 33, No. 4-5, 309-328 (1999). MSC: 03B40 68Q42 68Q65 PDF BibTeX XML Cite \textit{R. Matthes}, Theor. Inform. Appl. 33, No. 4--5, 309--328 (1999; Zbl 0940.03018) Full Text: DOI EuDML Link OpenURL
Xi, Hongwei Upper bounds for standardizations and an application. (English) Zbl 0938.03027 J. Symb. Log. 64, No. 1, 291-303 (1999). Reviewer: Teruo Hikita (Kawasaki) MSC: 03B40 PDF BibTeX XML Cite \textit{H. Xi}, J. Symb. Log. 64, No. 1, 291--303 (1999; Zbl 0938.03027) Full Text: DOI OpenURL
van Raamsdonk, Femke; Severi, Paula; Sørensen, Morten Heine B.; Xi, Hongwei Perpetual reductions in \(\lambda\)-calculus. (English) Zbl 0920.03024 Inf. Comput. 149, No. 2, 173-225 (1999). MSC: 03B40 PDF BibTeX XML Cite \textit{F. van Raamsdonk} et al., Inf. Comput. 149, No. 2, 173--225 (1999; Zbl 0920.03024) Full Text: DOI OpenURL
Dami, Laurent A lambda-calculus for dynamic binding. (English) Zbl 0895.68015 Theor. Comput. Sci. 192, No. 2, 201-231 (1998). MSC: 68N15 PDF BibTeX XML Cite \textit{L. Dami}, Theor. Comput. Sci. 192, No. 2, 201--231 (1998; Zbl 0895.68015) Full Text: DOI OpenURL
Nipkow, Tobias More Church-Rosser proofs (in Isabelle/HOL). (English) Zbl 1412.68248 McRobbie, M. A. (ed.) et al., Automated deduction – CADE-13. 13th international conference on automated deduction, New Brunswick, NJ, USA, July/August 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1104, 733-747 (1996). MSC: 68T15 03B40 PDF BibTeX XML Cite \textit{T. Nipkow}, Lect. Notes Comput. Sci. 1104, 733--747 (1996; Zbl 1412.68248) Full Text: DOI OpenURL