- Termtools - lists.rwth-aachen.de

von Florian Frohn

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

7 Stunden, 16 Minuten

1
0
0 0

Termination and Complexity Competition 2024: Call for Participation

von Florian Frohn

*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 Woche, 4 Tage

1
0
0 0

discussions & poll regarding the new termCOMP format

von Florian Frohn

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

2 Monate

1
1
0 0

FSCD 2024: Extended deadline (Abstract: February 12/ Submission:

von Carsten Fuhs

============================================================ Updated information on: EXTENDED DEADLINES, invited speakers ============================================================ FINAL CALL FOR PAPERS 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/ IMPORTANT DATES --------------- Due to a number of requests, submission deadlines will be extended for FSCD 2024 as follows: Abstract: February 12, 2024 *** extended Submission: February 19, 2024 *** extended Rebuttal: April 2-6, 2024 Notification: April 22, 2024 Final version: May 6, 2024 All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered. INVITED SPEAKERS ---------------- Delia Kesner, Université Paris Cité Bettina Könighofer, TU Graz Sebastian Ullrich, LEAN Focused Research Organisation Stephanie Weirich, UPenn (joint w/ ICALP and LICS) 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. The suggested, but not exclusive, list of topics for submission is: 1. Calculi: - Rewriting systems (string, term, higher-order, graph, conditional, modulo, infinitary, etc.); - Lambda calculus; - Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.); - Proof theory (natural deduction, sequent calculus, proof nets, etc.); - Type theory and logical frameworks; - Homotopy type theory; - Process algebras (synchronous, asynchronous, static and dynamic semantics with and without time, etc.); - Quantum calculi. 2. Methods in Computation and Deduction: - Type systems (polymorphism, dependent, recursive, intersection, session, etc.); - Induction, coinduction; - Matching, unification, completion, orderings; - Strategies (normalization, completeness, etc.); - Tree automata; - Model building and model checking; - Proof search and theorem proving; - Constraint solving and decision procedures. 3. Semantics: - Operational semantics and abstract machines; - Game Semantics and applications; - Domain theory and categorical models; - Quantitative models (timing, probabilities, etc.); - Quantum computation and emerging models in computation. 4. Algorithmic Analysis and Transformations of Formal Systems: - Type inference and type checking; - Abstract Interpretation; - Complexity analysis and implicit computational complexity; - Checking termination, confluence, derivational complexity and related properties; - Symbolic computation. 5. Tools and Applications: - Programming and proof environments; - Verification tools; - Proof assistants and interactive theorem provers; - Applications in industry; - Applications of formal systems in other sciences; - Applications of formal systems in education. 6. Formal Systems for Semantics and Verification in new challenging areas: - Certification; - Security; - Blockchain protocols; - Data bases; - Deep learning and machine learning algorithms; - Planning. PUBLICATION ----------- The proceedings will be published as an electronic volume in the Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl. All LIPIcs proceedings are open access. SPECIAL ISSUE ------------- Authors of selected papers will be invited to submit an extended version to a special issue of Logical Methods in Computer Science, or to TheoretiCS. SUBMISSION GUIDELINES --------------------- The submission site is: https://easychair.org/conferences/?conf=fscd2024 Submissions must be formatted using the LIPIcs style files (https://submission.dagstuhl.de/series/details/5#author) and submitted via EasyChair. Submissions can be made in two categories. Regular research papers are limited to 15 pages, excluding references and appendices. They must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 15 pages, excluding references. Shorter papers are welcome and will be given equal consideration. A system description must present new software tools, or significantly new versions of such tools, in which FSCD topics play an important role. An archive of the code with instructions on how to install and run the tool must be submitted. In addition, a webpage where the system can be experimented with should be provided. One author of each accepted paper is expected to register and present the work in person at the conference. Alternatively to in-person presentation, also online presentation is possible, but in-person registration by at least one author will still be required. BEST PAPER AWARD BY JUNIOR RESEARCHERS -------------------------------------- The program committee will select a paper in which at least one author is a junior researcher, i.e. either a student or whose PhD award date is less than three years from the first day of the meeting. When submitting the paper, other authors should declare to the PC Chair that at least 50% of contribution is made by the junior researcher(s). PROGRAM COMMITTEE CHAIR ----------------------- Jakob Rehof, TU Dortmund University Email: fscd2024 at easychair.org 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

2 Monate, 2 Wochen

1
0
0 0

TRS format at TermComp

von Florian Frohn

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

3 Monate, 1 Woche

8
10
0 0

Probabilistic Rewriting at termCOMP

von Florian Frohn

Dear all, after the nice interactive 0th probabilistic termination competition last year, we plan to introduce new (non-interactive) categories for probabilistic rewriting. A proposal for the new categories is available in this GitHub discussion [1]. Please share your opinions there. Best Florian [1] https://github.com/orgs/TermCOMP/discussions/82

3 Monate, 1 Woche

1
0
0 0

FSCD 2024: Second Call for Papers

von Carsten Fuhs

===================================================== Updated information on: co-location, invited speakers ===================================================== SECOND CALL FOR PAPERS 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/ IMPORTANT DATES --------------- All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered. Abstract: February 5, 2024 Submission: February 12, 2024 Rebuttal: April 2-6, 2024 Notification: April 22, 2024 Final version: May 6, 2024 INVITED SPEAKERS ---------------- Delia Kesner, Université Paris Cité Stephanie Weirich, UPenn (joint w/ ICALP and LICS) Sebastian Ullrich, LEAN Focused Research Organisation N.N. (TBA) 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. The suggested, but not exclusive, list of topics for submission is: 1. Calculi: - Rewriting systems (string, term, higher-order, graph, conditional, modulo, infinitary, etc.); - Lambda calculus; - Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.); - Proof theory (natural deduction, sequent calculus, proof nets, etc.); - Type theory and logical frameworks; - Homotopy type theory; - Process algebras (synchronous, asynchronous, static and dynamic semantics with and without time, etc.); - Quantum calculi. 2. Methods in Computation and Deduction: - Type systems (polymorphism, dependent, recursive, intersection, session, etc.); - Induction, coinduction; - Matching, unification, completion, orderings; - Strategies (normalization, completeness, etc.); - Tree automata; - Model building and model checking; - Proof search and theorem proving; - Constraint solving and decision procedures. 3. Semantics: - Operational semantics and abstract machines; - Game Semantics and applications; - Domain theory and categorical models; - Quantitative models (timing, probabilities, etc.); - Quantum computation and emerging models in computation. 4. Algorithmic Analysis and Transformations of Formal Systems: - Type inference and type checking; - Abstract Interpretation; - Complexity analysis and implicit computational complexity; - Checking termination, confluence, derivational complexity and related properties; - Symbolic computation. 5. Tools and Applications: - Programming and proof environments; - Verification tools; - Proof assistants and interactive theorem provers; - Applications in industry; - Applications of formal systems in other sciences; - Applications of formal systems in education. 6. Formal Systems for Semantics and Verification in new challenging areas: - Certification; - Security; - Blockchain protocols; - Data bases; - Deep learning and machine learning algorithms; - Planning. PUBLICATION ----------- The proceedings will be published as an electronic volume in the Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl. All LIPIcs proceedings are open access. SPECIAL ISSUE ------------- Authors of selected papers will be invited to submit an extended version to a special issue of Logical Methods in Computer Science, or to TheoretiCS. SUBMISSION GUIDELINES --------------------- The submission site is: https://easychair.org/conferences/?conf=fscd2024 Submissions must be formatted using the LIPIcs style files (https://submission.dagstuhl.de/series/details/5#author) and submitted via EasyChair. Submissions can be made in two categories. Regular research papers are limited to 15 pages, excluding references and appendices. They must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 15 pages, excluding references. Shorter papers are welcome and will be given equal consideration. A system description must present new software tools, or significantly new versions of such tools, in which FSCD topics play an important role. An archive of the code with instructions on how to install and run the tool must be submitted. In addition, a webpage where the system can be experimented with should be provided. One author of each accepted paper is expected to register and present the work in person at the conference. Alternatively to in-person presentation, also online presentation is possible, but in-person registration by at least one author will still be required. BEST PAPER AWARD BY JUNIOR RESEARCHERS -------------------------------------- The program committee will select a paper in which at least one author is a junior researcher, i.e. either a student or whose PhD award date is less than three years from the first day of the meeting. When submitting the paper, other authors should declare to the PC Chair that at least 50% of contribution is made by the junior researcher(s). PROGRAM COMMITTEE CHAIR ----------------------- Jakob Rehof, TU Dortmund University Email: fscd2024 at easychair.org 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

3 Monate, 2 Wochen

1
0
0 0

Inquiry about the expected answers of TPDB

von Yurika Hirobe

Dear Termination-Portal Organization. I hope this email finds you well. My name is Yurika Hirobe, and I am currently a master's student at the University of Tokyo. I am writing to you today as I have been utilizing your Termination-Competition dataset, which is available at the following link: [ https://github.com/TermCOMP/TPDB ], for my research purposes. Then I'm in trouble because expected answers corresponding to the benchmarks included in the dataset cannot be found. From my understanding, I believe that there should be XML files that provide comprehensive information, including the expected answers for each benchmark. Unfortunately, I have encountered some difficulties in locating such files within the dataset. It is crucial for my research to have access to this information to ensure the accuracy and completeness of my analysis. Hence, I kindly request your guidance in this matter. Could you please direct me to the specific location or resources where I can find the expected answers for the dataset? Your assistance in this regard would be of immense help to my research project. Thank you for your time and consideration. I look forward to hearing from you. Best regards, Yutika Hirobe Master's Student University of Tokyo yurikahirobe(a)gmail.com

5 Monate, 3 Wochen

3
2
0 0

Some inquiries about TPDB

von Zhang Yao

Hello, I'm interested in utilizing the benchmark in TPDB for conducting experiments on verification tools. However, I'm uncertain about the ground truth for these cases, specifically, whether a case is terminating or non-terminating. Could you kindly provide guidance on how to determine the termination status of these cases? Thank you!

6 Monate, 2 Wochen

2
1
0 0

Final Run tomorrow

von YAMADA, Akihisa

Dear all, the final run is ready at: https://termcomp.herokuapp.com/Y2023/ I will start it in 15:30 CET tomorrow, i.e., the first break of WST. Demonstration categories will be after the competition. Best, Akihisa

7 Monate, 2 Wochen

3
3
0 0

2024

2023

2022

2021

2020

Termtools