@inproceedings{RISC7279,
author = {William Steingartner and Martin Mormák and Wolfgang Schreiner},
title = {{A Visualization Framework for Semantics of a Concatenative Compositional Language}},
booktitle = {{New Trends in Database and Information Systems}},
language = {english},
abstract = {Concatenative programming languages represent an interesting learning environment for teaching formal semantics, stack-based computations, and higher-order programming constructs. However, students often have difficulty understanding the relationship between formal semantic rules and concrete program execution because intermediate states of computation are not directly observable.This paper presents a visualization framework for the KKJ language based on executable semantics. Semantic rules specified in the SLANG language generate execution traces consisting of successive program configurations that are subsequently visualized. The proposed approach transforms formal semantic specifications into observable execution behavior and allows users to observe the evolution of the stack, quotations, and higher-order operations during program execution. The resulting framework establishes a link between formal semantics, executable semantics, and program visualization, thereby supporting the conceptual understanding of stack-based and higher-order computations in concatenative languages. Unlike existing visualization tools, the proposed framework visualizes semantic transitions directly derived from executable semantic specifications, rather than from implementation-level execution.},
series = {Communications in Computer and Information Science},
volume = {3175},
pages = {332--347},
publisher = {Springer},
address = {Cham},
isbn_issn = {ISBN 978-3-032-39822-2},
year = {2027},
editor = {Genoveva Vargas Solar and Kostas Stefanidis and Themis Palpanas and Patrick Marcel and Mirian Halfeld-Ferrari and Panos Vassiliadis and Tatjana Welzer and Enrico Gallinucci and Veronika Peralta},
refereed = {yes},
keywords = {computer science education, concatenative languages, executable semantics, execution trace, formal semantics, program visualization, stack-based computation},
sponsor = {KEGA project 028TUKE-4/2026 – “Innovative approaches to teaching and researching formal methods in the context of modern software engineering”},
length = {16},
conferencename = {ADBIS 2026: European Conference on Advances in Databases and Information Systems, Orléans, France, September 28 – October 1, 2026},
url = {https://doi.org/10.1007/978-3-032-39823-9_31}
}

@inproceedings{RISC7268,
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Quantitative Generalization for Variadic Nominal Terms}},
booktitle = {{Proceedings of the 40th International Workshop on Unification (UNIF 2026)}},
language = {english},
series = {RISC Report Series},
volume = {26-10},
pages = {24--31},
publisher = {RISC, Johannes Kepler University Linz},
isbn_issn = {ISSN: 2791-4267},
year = {2026},
editor = {Silvio Ghilardi and Cleo Pau},
refereed = {yes},
length = {8},
url = {https://doi.org/10.35011/risc.26-10}
}

@inproceedings{RISC7267,
author = {Marcos Mercandeli-Rodrigues and Andrés Felipe González Barragan and David M. Cerna and Temur Kutsia and Mauricio Ayala-Rincón},
title = {{On Completeness of Absorptive Anti-Unification}},
booktitle = {{Proceedings of the 40th International Workshop on Unification (UNIF 2026)}},
language = {english},
series = {RISC Report Series},
volume = {26-10},
pages = {55--62},
publisher = {RISC, Johannes Kepler University Linz},
isbn_issn = {ISSN: 2791-4267},
year = {2026},
editor = {Silvio Ghilardi and Cleo Pau},
refereed = {yes},
length = {8},
url = {https://doi.org/10.35011/risc.26-10}
}

@inproceedings{RISC7258,
author = {J. Ablinger and A. Behring and J.~Bluemlein and A. De Freitas and A. von Manteuffel and C. Schneider and K. Schoenwald},
title = {{The complete three-loop unpolarized and polarized massive operator matrix elements and asymptotic Wilson coefficients}},
booktitle = {{ 17th International Symposium on Radiative Corrections: Applications of Quantum Field Theory to Phenomenology (RADCOR2025)}},
language = {english},
abstract = {We report on the three-loop unpolarized and polarized massive operator matrix elements, with single- and two-mass corrections, and the associated deep-inelastic massive Wilson coefficients in the region $Q^2 gg m_Q^2$, the calculation of which has been completed recently. We also provide fast and precise numerical representations ofthe massless Wilson coefficients, splitting functions to tree-loop order, and target-mass corrections in $x$-space well suited for QCD-fitting codes.},
series = {POS},
volume = {497},
number = {076},
pages = {1--16},
isbn_issn = {ISSN 1824-8039 },
year = {2026},
note = {arXiv:2602.10334 [hep-ph]},
editor = {M. C. Kumar and Narayan Rana and Vajravelu Ravindran and Satyajit Seth and Ambresh Shivaji},
refereed = {no},
keywords = { three-loop unpolarized and polarized massive operator matrix elements, deep-inelastic scattering, computer algebra, special functions},
length = {16},
url = {https://doi.org/10.22323/1.497.0076}
}

@inproceedings{RISC7270,
author = {J. Ablinger and A. Behring and J.~Bluemlein and A. De Freitas and A. von Manteuffel and C. Schneider and K. Schoenwald},
title = {{The variable flavor number scheme to three-loop order}},
booktitle = {{Proceedings of Loops and Legs in Quantum Field Theory}},
language = {english},
abstract = {We describe the variable flavor number scheme to three-loop order, which modifies the massless parton densities by single- and two-mass effects and introduces heavy-quark parton distribution functions for charm and bottom. A renormalization group analysis shows the validity of this picture at large scales $Q^2$, where it resembles the non-power-suppressed heavy-flavor corrections completely. We also provide numerical implementations of a series of charged and neutral current Wilson coefficients.},
volume = {PoS LL2026 (2026) 025},
pages = {1--11},
isbn_issn = {ISSN 1824-8039},
year = {2026},
note = {arXiv:2607.05235 [hep-ph]},
editor = {P. Marquard and M. Steinhauser},
refereed = {no},
keywords = {variable flavor number scheme, heavy-quark parton distribution function, computer algebra, numerical implementation},
length = {11},
url = {https://doi.org/10.22323/1.521.0025}
}

@inproceedings{RISC7273,
author = {J. Bluemlein and A. De Freitas and P. Marquard and J. Obrovsky and C. Schneider},
title = {{Holonomic techniques for massive 3-loop form factors: the gluonic case}},
booktitle = {{Proceedings of Loops and Legs in Quantum Field Theory}},
language = {english},
abstract = {Massive three-loop form factors for vector, axial-vector, scalar, and pseudoscalar currents are vital for precision collider phenomenology. Extending the quarkonic framework to the more complex gluonic case, in Ref.~cite{BFMOS:26} we computed these contributions widely using advanced computer algebra, automated guessing, and large-scale PSLQ searches. Here, we outline the core strategy of the large-moment method and illustrate its main challenges, including solving record-sized recurrences and differential equations. Our high-precision evaluation provides an exact analytic representation around $s=0$ in terms of MZVs. We achieved a complete analytic series expansion around $s=pminfty$ for the first time, which depends on MZVs and three constants out ofhigher number spaces, along with reliable analytic continuations across $s in (-infty, infty)$, serving as a landmark benchmark for modern symbolic computation.},
series = {PoS(LL2026)071},
pages = {1--11},
isbn_issn = {ISSN 1824-8039},
year = {2026},
note = {arXiv:2609.24279},
editor = {P. Marquard and M. Steinhauser},
refereed = {no},
keywords = {form factor, Feynman diagrams, linear differential equation, linear difference equation, large moment method, guessing, PSLQ},
length = {11},
url = {https://doi.org/10.22323/1.521.0071}
}

@inproceedings{RISC7265,
author = {B. Dundua and G. Ehling and S. Escobar and M. Fernández and T. Kutsia},
title = {{Quantitative Equational Rewriting}},
booktitle = {{Proceedings of the 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026) }},
language = {english},
series = {LIPIcs},
volume = {386},
pages = {1--18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
isbn_issn = {ISBN 978-3-95977-442-0},
year = {2026},
editor = {M. Koucký and D. Petrișan},
refereed = {yes},
length = {18},
url = {https://doi.org/10.4230/LIPIcs.MFCS.2026.76}
}

@inproceedings{RISC7266,
author = { Mauricio Ayala-Rincón and Thaynara Arielly de Lima and Maria Júlia Dias Lima and Temur Kutsia and Marcos Mercandeli-Rodrigues},
title = {{ Anti-Unification Completeness Analysis in PVS}},
booktitle = {{Proceedings of the 21st Workshop on Logical Frameworks and Meta Languages: Theory and Practice }},
language = {english},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {448},
pages = {29--46},
publisher = {Open Publishing Association},
isbn_issn = {ISSN: 2075-2180},
year = {2026},
editor = {Sophie Tourret and Olivier Hermant},
refereed = {yes},
length = {18},
url = {https://dx.doi.org/10.4204/EPTCS.448.3}
}

@inproceedings{RISC7251,
author = {Georg Regensburger and Clemens Hofstadler and Peter Krug},
title = {{Refuting noncommutative ideal memberschip via matrix certificates}},
booktitle = {{Proceedings of ISSAC 2026}},
language = {english},
abstract = {The ideal membership problem in free algebras is undecidable in general. More precisely, while membership can always be verified in finite time (e.g., via noncommutative Gröbner bases), non-membership is undecidable in general.In this work, we introduce matrix certificates for refuting ideal membership of (commutative and) noncommutative polynomials. Such certificates are matrix evaluations that vanish on the generators of an ideal but not on a given candidate polynomial. For commutative polynomials, a perfect Nullstellensatz guarantees the existence of such certificates with commuting square matrices. For noncommutative polynomials, certificates may require non-square matrices or may not exist at all. To handle evaluations on non-square matrices, we use quivers and their matrix representations.We have implemented an approach for finding matrix certificates by ansatz in SageMath and demonstrate its effectiveness on different examples. Our method relies on the ability to efficiently find one (simple) solution to a system of commutative polynomial equations, which we do by combining SAT solving with Hensel lifting. Our experiments suggest that, in practice, ideal (non-)membership can be efficiently decided and certified.},
pages = {209--218},
isbn_issn = {979-8-4007-2595-1},
year = {2026},
editor = {Christoph Koutschan and Alin Bostan and Clement pernet and Thi Xuan Vu},
refereed = {yes},
length = {10},
url = {https://dl.acm.org/doi/10.1145/3815436.3815447}
}