- Termtools - lists.rwth-aachen.de

FSCD 2024: First Call for Papers

von Carsten Fuhs

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 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 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

8 Monate, 1 Woche

1
0
0 0

0th probabilistic termCOMP

von YAMADA, Akihisa

Dear all, in August 25th, we plan the "0th" probabilistic termination competition. It imitates the termination competition in 2003: participants present examples on whiteboard/screen, and all participants input the examples to their tools on laptops and report the outputs. I'm sorry that this announcement is so late. Best regards, Akihisa

8 Monate, 3 Wochen

1
0
0 0

CPF/CeTA: split for relative termination?

von Johannes Waldmann

Dear all, (sIsEmpty works fine, thanks René) can CPF/CeTA do "split" for relative termination? "split" can be used as a notational trick, to avoid unlabeling split for full termination is: SN(D / R-D) && SN(R-D) => SN(R) (application: semantic labeling in the first premise) http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/1f1ecb… I think I want SN(D / R+S) && SN(R-D / S-D) => SN(R/S) (cf. Geser "Relative Termination" (UIB 91-03) Section 3.2) but I cannot get CeTA to accept this, https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/489 - Johannes.

8 Monate, 3 Wochen

1
1
0 0

first run

von YAMADA, Akihisa

Dear all, I have already started the first run. https://termcomp.herokuapp.com/Y2023/ We observe already a conflict :) and runscript errors :( Please analyze. Best, Akihisa

8 Monate, 3 Wochen

1
2
0 0

can CeTA infer relative termination from absolute termination?

von Johannes Waldmann

Dear all, for proving relative termination SN(R/S), a very crude method is to infer it from SN(R \cup S). Does the CPF format (the CeTA verifier) have a provision for that? - Johannes. NB: crude, but powerful, on current SRS_Relative benchmarks, see our WST contribution ...

9 Monate

2
1
0 0

CeTA postprocessor

von YAMADA, Akihisa

Dear certified category participants, sorry to be late, I've uploaded post-processor ceta-2.45 with id=780. Please use it if you want to test (though, as before, I expect to have problems in the first run). Best, Akihisa

9 Monate, 2 Wochen

1
0
0 0

termCOMP 2023 registration

von YAMADA, Akihisa

Dear all, please register your tools by editing Y2023/info.php of https://github.com/TermCOMP/starexec-master/ by August 6. The registration status can be monitored here: https://termcomp.herokuapp.com/Y2023/ Best, Akihisa

9 Monate, 3 Wochen

1
0
0 0

Termination and Complexity Competition 2023: Second Call for

von Juergen Giesl

*Termination and Complexity Competition 2023* http://www.termination-portal.org/wiki/Termination_Competition_2023 *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 19th International Workshop on Termination (WST 2023, https://termination-portal.org/wiki/WST2023). 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 WST. 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_2023 *Important dates* - Tool and Benchmark Submission: August 6, 2023 - First Run: August 13, 2023 - Bugfix Deadline: August 20, 2023 - Final Run: August 24, 2023 - WST: August 24-25, 2023

9 Monate, 3 Wochen

1
0
0 0

Problems with StarExec + SymPy

von lommen＠cs.rwth-aachen.de

Dear all, we are currently trying to prepare our tool for the TermComp. However, the newest version of our tool requires SymPy. Unfortunately, so far we fail to get SymPy running on StarExec. Does anybody have experience on running SymPy (or more generally Python + some not-installed dependency) on StarExec? If you have any ideas, please let me know! Thanks, Nils

10 Monate, 2 Wochen

1
0
0 0

CALL FOR NOMINATION - FSCD Steering Committee Membership Election

von Carsten Fuhs

Formal Structures for Computation and Deduction (FSCD) Steering Committee Membership Election 2023 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). 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 * Monday 26 June 2023 (AoE) * The election statements will be posted on the FSCD webpage before the start of FSCD 2023. The election will take place at the General Meeting of FSCD 2023, 3-6 July 2023. Herman Geuvers herman at cs.ru.nl FSCD SC Chair

10 Monate, 4 Wochen

1
0
0 0

2024

2023

2022

2021

2020

Termtools