- Termtools - lists.rwth-aachen.de

technical information about StarExec
by Florian Frohn 13 Jun '24

13 Jun '24

Dear all, here is the information that I have about the current StarExec configuration: root@starexec2:~# uname -r 5.15.0-112-generic oot@starexec2:~# dpkg -l libc6-dev:amd64 python3 Desired=Unknown/Install/Remove/Purge/Hold | Status=Not/Inst/Conf-files/Unpacked/halF-conf/Half-inst/trig-aWait/Trig-pend |/ Err?=(none)/Reinst-required (Status,Err: uppercase=bad) ||/ Name Version Architecture Description +++-===============-===============-============-========================================================================= ii libc6-dev:amd64 2.35-0ubuntu3.8 amd64 GNU C Library: Development Libraries and Header Files ii python3 3.10.6-1~22.04 amd64 interactive high-level object-oriented language (default python3 version) Note that the information here https://www.starexec.org/starexec/public/machine-specs.txt is outdated! Best Florian

1 0

TRS format at TermComp
by Florian Frohn 13 Jun '24

13 Jun '24

Dear all, at the last WST, there were some discussions about the input format for TRSs. My takeaway was that not everyone is happy with the current XML format. So we (the TermComp SC) recently started to discuss whether the format should be changed. As far as I can see, there are three obvious options: (a) keep the current format Pro: no work Contra: not human readable (b) go back to the old format [1] (here's [2] an example) Pro: - human readable - the same format is used for other categories (e.g., Complexity of ITSs and Termination of Integer TRSs) - some tools can still parse it Contra: There were some issues with the semantics, in particular if there were several VAR sections. However, from my understanding, these issues can be resolved by forbidding more than one VAR section. (c) a new S-expression based format has been proposed for the confluence competition [3] Pro: human readable(?) Contra: no tool can parse it yet So if you compete, or are interested in, the TRS categories at TermComp, please let us know what you think. I'm also particularly interested in the following questions: - If you participate, can your tool still parse the old format? - Do you recall more details about the reasons for the switch from the old format to the current one? A related (but mostly independent) question is whether we should separate the properties to be analyzed (full vs innermost rewriting, termination vs complexity etc.) from the actual TRS. That could avoid a lot of redundancy in the TPDB. If you have an opinion on that, please share it. Thanks, Florian [1] https://www.lri.fr/~marche/tpdb/format.html [2] https://aprove.informatik.rwth-aachen.de/interface/v-AProVE2023/trs_wst [3] http://cl-informatik.uibk.ac.at/iwc/2023/proceedings.pdf, page 32

8 16

ARI for higher-order at termCOMP
by Florian Frohn 11 Jun '24

11 Jun '24

Dear all, since, in contrast to other categories, there is no converter from the new ARI to the old XTC format for higher-order TRSs, we decided to use the XTC format instead of the ARI format for the higher-order category one last time. In this way, tools that participated in the past can enter the competition with little effort, and tool authors have plenty of time to implement a parser for the new ARI format before termCOMP '25. If you intended to join the higher-order category this year, and your tool already supports the new ARI format, then please get in touch, so that we can discuss whether we should have an additional higher-order category with the new ARI format. Best Florian

1 0

StarExec still down
by Florian Frohn 10 Jun '24

10 Jun '24

Dear all, while the registration deadline for termCOMP is approaching, StarExec is still unavailable, unfortunately. The reason is an update which takes longer than expected due to technical problems. Hence, no testing is possible at the moment, neither for the participants, nor for me as organizer. Hopefully, StarExec will be back online soon. In any case, these technical issues should not prevent anyone from participating, of course. So if necessary, we will extend the registration deadline further. Let's reassess the situation when StarExec is again available. Best Florian

2 1

Termination and Complexity Competition 2024: Second Call for
by Florian Frohn 03 Jun '24

03 Jun '24

*Termination and Complexity Competition 2024* http://www.termination-portal.org/wiki/Termination_Competition_2024 *Call for Participation* Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis. After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques. The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas. The competition will be affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2024, https://merz.gitlabpages.inria.fr/2024-ijcar/). It will be run on the StarExec platform (https://www.starexec.org/). The final run and a presentation of the final results will be live at IJCAR. We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications. A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed. For further information, we refer to the website of the termination and complexity competition: https://termination-portal.org/wiki/Termination_Competition_2024 <https://termination-portal.org/wiki/Termination_Competition_2024> _Important dates_ As StarExec is currently unavailable due to an update, the deadline has been extended to give all participants the opportunity to properly test their tools before submission. * Tool and Benchmark Submission (*extended*): June 19, 2024 * First Run: June 24, 2024 * Bugfix Deadline: June 30, 2024 * Final Run: July 3/4, 2024 * Presentation of the results at IJCAR: July 5, 2024

1 0

CALL FOR NOMINATION - FSCD Steering Committee Membership Election
by Carsten Fuhs 24 May '24

24 May '24

Formal Structures for Computation and Deduction (FSCD) Steering Committee Membership Election 2024 CALL FOR NOMINATION The FSCD SC consists of the SC Chair, 6 elected members, PC Chairs of the last 3 years, the Publicity Chair, Workshop Chair and former SC Chair. Every year the outgoing elected SC members are replaced by new members elected by a secret ballot. Each SC member normally serves for 3 years, unless exceptions apply (see the FSCD Rules of Business http://fscd-conference.org/organization/rules-of-business/ for details). Note that past SC members are allowed to run for SC membership again. The current steering committee composition, together with the serving time for each member, is available here: https://fscd-conference.org/organization/steering-committee/ Candidates for SC membership are requested to email the FSCD SC Chair an election statement (including a brief bio) on one a4 page, preferably in PDF, no later than * Friday 21 June 2024 (AoE) * The election statements will be posted on the FSCD webpage before the start of FSCD 2024. The election will take place at the General Meeting of FSCD 2024, 10-13 July 2024. Herman Geuvers herman at cs.ru.nl FSCD SC Chair

1 0

FSCD 2024: Call for Participation (early registration deadline: *May
by Carsten Fuhs 14 May '24

14 May '24

============================================================================== CALL FOR PARTICIPATION Ninth International Conference on Formal Structures for Computation and Deduction (FSCD 2024) July 10-13, 2024, Tallinn, Estonia https://fscd-conference.org/2024 FSCD 2024 will be co-located with ICALP 2024 and LICS 2024. https://compose.ioc.ee/icalp2024/ https://lics.siglog.org/lics24/ OVERVIEW -------- FSCD (https://fscd-conference.org/) covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logic, models of computation, semantics and verification in new challenging areas. REGISTRATION ------------ The registration page for the conferences is already open and linked from: https://compose.ioc.ee/icalp2024/#registration This link should be used also to register for affiliated workshops. The early registration deadline is *** May 17, 2024 ***. FSCD 2024 is co-located with ICALP 2024 (July 8-12, 2024) and LICS 2024 (July 8-11, 2024), and special rates are available for joint registration to the conferences. INVITED SPEAKERS ---------------- Information about the invited speakers is here: https://compose.ioc.ee/icalp2024/#invited - Delia Kesner, Université Paris Cité - Bettina Könighofer, TU Graz - Sebastian Ullrich, Lean FRO - Stephanie Weirich, University of Pennsylvania (joint ICALP/LICS/FSCD speaker) ACCEPTED PAPERS --------------- The list of accepted papers is here: https://cs.ioc.ee/fscd24/accepted.html AFFILIATED WORKSHOPS -------------------- The following workshops are affiliated with FSCD, ICALP, and LICS in 2024: https://compose.ioc.ee/icalp2024/#workshops - Parameterized Approximation Algorithms Workshop (PAAW 2024) - July 6, 2024 - Trends in Arithmetic Theories (TAT 2024) - July 6, 2024 - Geometric and Topological Methods in Computer Science (GETCO 2024) - July 6-7, 2024 - Algorithmic Aspects of Temporal Graphs VII (AATG 2024) - July 7, 2024 - Learning and Automata (LearnAut 2024) - July 7, 2024 - Logic Mentoring Workshop (LMW 2024) - July 7, 2024 - Parameterized Algorithms and Constraint Satisfaction (PACS 2024) - July 7, 2024 - Structure meets Power (SmP 2024) - July 7, 2024 - Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2024) - July 8, 2024 - Mathematically Structured Functional Programming (MSFP 2024) - July 8, 2024 - Eighth International Workshop on Trends in Linear Logic and Applications (TLLA 2024) - July 8-9, 2024 - Intersection Types and Related Systems (ITRS 2024) - July 9, 2024 - International Workshop on Confluence (IWC 2024) - July 9, 2024 - Women in Logic 2024 - July 9, 2024 PROGRAM COMMITTEE CHAIR ----------------------- Jakob Rehof, TU Dortmund University PROGRAM COMMITTEE ----------------- Thorsten Altenkirch, University of Nottingham Sandra Alves, University of Porto Takahito Aoto, Niigata University Mauricio Ayala-Rincón, Brasilia University Stephanie Balzer, CMU Thierry Coquand, University of Gothenburg Alejandro Díaz-Caro, Quilmes National University & CONICET-Buenos Aires University Claudia Faggian, CNRS, Université de Paris Silvia Ghilezan, University of Novi Sad Simon Gay, University of Glasgow Cezary Kaliszyk, University of Innsbruck Ambrus Kaposi, Eötvös Loránd University, Budapest Dexter Kozen, Cornell University Dominique Larchey-Wendling, CNRS, Loria Marina Lenisa, University of Udine Sonia Marin, University of Birmingham Naoki Nishida, Nagoya University Christine Paulin-Mohring, Paris-Saclay University Pierre-Marie Pédrot, Inria Rennes-Bretagne-Atlantique Elaine Pimentel, University College London Jakob Rehof (Chair), TU Dortmund University Simona Ronchi della Rocca, University of Torino Sylvain Schmitz, Université Paris Cité Aleksy Schubert, University of Warsaw Jakob Grue Simonsen, University of Copenhagen Kathrin Stark, Heriot-Watt University, Edinburgh Lutz Straßburger, Inria Saclay Tachio Terauchi, Waseda University Sarah Winkler, Free University of Bolzano CONFERENCE CHAIR ---------------- Niccolò Veltri, Tallinn University of Technology WORKSHOP CHAIR -------------- Luigi Liquori, Inria STEERING COMMITTEE WORKSHOP CHAIR --------------------------------- Cynthia Kop, Radboud University Nijmegen PUBLICITY CHAIR --------------- Carsten Fuhs, Birkbeck, University of London FSCD STEERING COMMITTEE ----------------------- Herman Geuvers (Chair), Radboud University Nijmegen Patrick Baillot, CNRS, Université de Lille Alejandro Díaz-Caro, Quilmes National University & CONICET-Buenos Aires University Amy Felty, University of Ottawa Carsten Fuhs, Birkbeck, University of London Marco Gaboardi, Boston University Jürgen Giesl, RWTH Aachen University Delia Kesner, Université Paris Cité Naoki Kobayashi, University of Tokyo Cynthia Kop, Radboud University Nijmegen Luigi Liquori, Inria Giulio Manzonetto, Université Paris-Nord Daniele Nantes, Imperial College London / University of Brasilia Femke van Raamsdonk, Vrije Universiteit Amsterdam We are looking forward to seeing you in Tallinn! ==============================================================================

1 0

new ARI format at termCOMP '24
by Florian Frohn 26 Apr '24

26 Apr '24

Dear all, the conversion to the new ARI format is done for all first-order TRS/SRS categories [1]. The tool to convert back and forth between XTC and ARI is available here [2] (note that you have to use the branch xtc, not the master branch). Some documentation for the new format is available here [3]. If you have suggestions to improve it, please let me know. Regarding valid identifiers, there might be (hopefully minimal) changes in the (near) future. In particular, the question which identifiers should be quoted is not entirely settled. If you're interested, please participate in the corresponding discussion on Github [4]. Nevertheless, I think the current version is good enough to start testing. Let me know if you run into any problems. Best Florian [1] https://github.com/TermCOMP/TPDB-ARI [2] https://github.com/TermCOMP/ari-conversion/tree/xtc [3] https://termination-portal.org/wiki/Term_Rewriting [4] https://github.com/orgs/TermCOMP/discussions/83#discussioncomment-8676014

1 0

Termination and Complexity Competition 2024: Call for Participation
by Florian Frohn 15 Apr '24

15 Apr '24

*Termination and Complexity Competition 2024* http://www.termination-portal.org/wiki/Termination_Competition_2024 *Call for Participation* Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis. After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques. The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas. The competition will be affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2024, https://merz.gitlabpages.inria.fr/2024-ijcar/). It will be run on the StarExec platform (https://www.starexec.org/). The final run and a presentation of the final results will be live at IJCAR. We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications. A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed. For further information, we refer to the website of the termination and complexity competition: https://termination-portal.org/wiki/Termination_Competition_2024 <https://termination-portal.org/wiki/Termination_Competition_2024> _Important dates_ * Tool and Benchmark Submission: June 12, 2024 * First Run: June 19, 2024 * Bugfix Deadline: June 26, 2024 * IJCAR: July 3-6, 2024

1 0

discussions & poll regarding the new termCOMP format
by Florian Frohn 21 Feb '24

21 Feb '24

Dear all, in case you missed it: There are some interesting discussions about adapting the ARI format for termCOMP, see [1]. In particular, there's also a poll about the new format for SRSs [2]. Currently, there are five votes only... So if you're interested, please have a look at the corresponding discussion [3] and vote! Best Florian [1] https://github.com/orgs/TermCOMP/discussions [2] https://github.com/orgs/TermCOMP/discussions/88 [3] https://github.com/orgs/TermCOMP/discussions/87

1 1