The Coq mailing list

[geoff AT cs.miami.edu]

IJCAR 2024 --- Co-Located workshops. More information below.

PAAR-2024: 9TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING
https://paar2024.github.io/

QUANTIFY 2024: International Workshop on Quantification
https://qbf24.pages.sai.jku.at/quantify/

SC-Square 2024: 9th International Workshop on Satisfiability Checking and 
Symbolic Computation
http://www.sc-square.org/CSA/workshop9.html

Termination and Complexity Competition 2024
http://www.termination-portal.org/wiki/Termination_Competition_2024

ThEdu'24: Theorem proving components for Educational software
http://www.uc.pt/en/congressos/thedu/ThEdu24

UNIF 2024: The 38th International Workshop on Unification
https://lat.inf.tu-dresden.de/unif2024

5th International Workshop on Automated (Co)inductive Theorem Proving
https://wait2024.github.io/

The TPTP Tea Party
https://www.tptp.org/TPTP/TPTPTParty/2024/



******************************************************************************
                                                                            
                                                                             
        PAAR-2024: 9TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING 
                   -- co-located with IJCAR 2024  -- 
                                                                            
                      July 2, 2024, Nancy, France

        Web site: https://paar2024.github.io/
        Submission link: https://easychair.org/conferences/?conf=paar2024
        Abstract registration deadline: April 5, 2024
        Submission deadline: April 12, 2024
        Topics: automated reasoning, implementation, tools


******************************************************************************


The automation of logical reasoning is a challenge that has been
studied intensively in fields including mathematics, philosophy, and
computer science. PAAR is the workshop on turning this theory into
practice: how can automated reasoning tools be built that work and are
useful in applications? PAAR covers all aspects of this challenge:
which theories, logics, or fragments are well-behaved in practice, and
connect well to application domains? which reasoning tasks are
tractable and useful? which algorithms are able to solve real-world
instances? how should automated reasoning tools be designed,
implemented, tested, and evaluated?

The goal of PAAR is to bring together theoreticians, tool developers,
and users, to concentrate on the practical aspects of automated
reasoning. The workshop welcomes high-quality contributions of any
kind, including new research results, presentation of work in
progress, presentation of new tools, new implementation techniques,
new application domains, or case studies.


Submission Guidelines
---------------------
Researchers interested in participating are invited to submit either an
extended abstract (up to 8 pages) or a regular paper (up to 15 pages), 
excluding
references, via EasyChair at https://easychair.org/conferences/?conf=paar2024.
Submissions will be refereed by the program committee, which will select a 
balanced 
program of high-quality contributions. Short submissions that could stimulate 
fruitful discussion at the workshop are particularly welcome.

Submissions should be prepared in LaTeX using the CEUR-WS.org style template
(CEURART, one-column). The package containing the class file and the user 
guide
can be downloaded from http://ceur-ws.org/Vol-XXX/CEURART.zip.

Topics include, but are not limited to:
--------------------------------------
* automated reasoning in propositional, first-order, higher-order, and
  non-classical logics;
* implementation of provers (SAT, SMT, resolution, superposition, tableau,
   instantiation-based, rewriting, logical frameworks, etc.);
* automated reasoning tools for all kinds of practical problems and
  applications;
* pragmatics of automated reasoning within proof assistants;
* practical experiences, usability aspects, feasibility studies;
* evaluation of implementation techniques and automated reasoning tools;
* performance aspects, benchmarking approaches; non-standard approaches to
  automated reasoning, non-standard forms of automated reasoning, new
  applications;
* implementation techniques, optimisation techniques, machine learning,
  strategies and heuristics, fairness;
* tools or methods that support prover development;
* system descriptions and demos.  

Invited Speakers
-------------------

* N.N.
* N.N.

Programme Committee
-------------------

* Cláudia Nalon, University of Brasília, BR (PC co-chair)
* Alexander Steen, University of Greifswald, DE (PC co-chair)
* Martin Suda, Czech Technical University in Prague, CZ (PC co-chair)
* to be completed

Publication
-----------
PAAR proceedings will be published electronically in a workshop
proceedings venue (such as CEUR workshop proceedings or
EasyChair Kalpa proceedings).

Venue
-----
IJCAR 2024 in Nancy, France

Important dates
---------------
* Abstract submission: April 5, 2024
* Paper submission: April 12, 2024
* Workshop: July 2, 2024




******************************************************************************

International Workshop on Quantification (QUANTIFY 2024)
(co-located with the International Joint Conference on Automated Reasoning) 

https://qbf24.pages.sai.jku.at/quantify/

******************************************************************************



*** Overview ***

Quantifiers play an important role in language extensions of many logics. 
The use of quantifiers often allows for a more succinct encoding as it 
would be possible without quantifiers. However, the introduction of 
quantifiers affects the complexity of the extended formalism in general. 
In consequence, theoretical results established for the quantifier-free 
formalism may not directly be transferred to the quantified case. Further, 
techniques successfully implemented in reasoning tools for quantifier-free 
formulas cannot directly be lifted to a quantified version. 

The goal of the Workshop on Quantification (QUANTIFY 2024) is 
to bring together researchers who investigate the impact of 
quantification from a theoretical as well as from a practical 
point of view. Quantification is a topic in different research 
areas, e.g., in SAT in terms of QBF, in CSP in terms of QCSP, 
in SMT, ATP, Computer Algebra, etc. 

This workshop has the aim to provide an interdisciplinary forum 
where researchers of various fields may exchange their experiences.

In particular, the following topics shall be considered at the workshop:

* Theoretical aspects of quantification.
* Practical aspects of quantification.
* Intersections between the different research communities 
  working on quantification.


*** Organizers ***

* Konstantin Korovin, University of Manchester, UK
* Martina Seidl, Johannes Kepler University Linz, Austria


*** Program Committee ***

* Konstantin Korovin, University of Manchester, UK
* Martina Seidl, Johannes Kepler University Linz, Austria
TBA


*** Important Dates ***

Paper Submission: May 1
Notification of Acceptance: May 21
Camera Ready: June 1
Workshop: July 1



*** Submission ***

Submissions of extended abstracts, full papers, and tutorials are solicited 
and will be managed via Easychair: 


https://easychair.org/conferences/?conf=quantify24


Submitted papers should be formatted in LNCS format.

We solicit three types of submissions:

* Talk abstracts (maximum two pages, excluding references) 
  describing already published results.
* Full papers (maximum 15 pages, excluding references) on novel, 
  unpublished work.
* Tutorial papers (maximum 15 pages, excluding references) 
  introducing a research field related to quantifiers.  

The talk abstracts should include a relevant bibliography of related work 
and an outline of the planned talk. For this category, we explicitly advocate 
talks which summarize the results of one or more already published papers. 

Full papers should contain novel, unpublished work that qualifies to be 
published in a special issue of a journal or formal workshop proceedings. 

Tutorial papers should survey results already published, maybe in multiple 
articles or presentations capturing the commonalities and differences 
of various quantification approaches (perhaps even interdisciplinary).

Each submission will be assessed by the program committee and the workshop 
organizers with respect to novelty, originality, and scope.

Submissions related to completed work as well as work in progress are 
welcome. 
Authors are encouraged to provide additional material such as source code of 
tools, experimental data, benchmarks and related publications in an appendix 
or a related webpage. The additional material will be considered at the 
discretion of the reviewers.

Previously published work or extensions thereof may be submitted to the 
workshop but that case has to be explicitly stated in the submitted paper. 
This regulation also applies to work which is currently under review 
elsewhere.


Authors of accepted abstracts and papers are expected to give a talk 
at the workshop.


*** Plans for Publications ***

The outcomes of the discussions will be summarized in a workshop report, 
which can be made publicly available as technical report (unless the
participants decide not to do so). 

In case we get enough full and tutorial papers, we will organize a 
special issue on quantification (e.g., in the Journal of Satisfiability 
(JSAT) 
or formal workshop proceedings. 

*** Contact ***

For any questions, contact <quantify24 AT easychair.org>.



******************************************************************************
 9th International Workshop on Satisfiability Checking and Symbolic 
Computation
                           SC-Square 2024

                      July 2, 2024, Nancy France

   http://www.sc-square.org/CSA/workshop9.html

******************************************************************************

The 9th SC-Square Workshop is a satellite event of IJCAR, held at the Inria 
Nancy
research center and LORIA in Nancy, France, from July 1 to July 6, 2024.

Main conference website:
https://merz.gitlabpages.inria.fr/2024-ijcar/

SC-Square Workshop website:
http://www.sc-square.org/CSA/workshop9.html

=== Keynote Speakers ===

We are pleased to announce our keynote speakers:

- Manuel Kauers (Johannes Kepler University, Austria)
- Lawrence Paulson (University of Cambridge, UK)

=== Key Dates ===

Submission deadline: April 12, 2024
ISSAC Fast-Track Deadline*: May 3, 2024
Notification: May 17, 2024
Final version: May 31, 2024
Workshop date: July 2, 2024

*This year, considering the rather tight schedule between the ISSAC 
conference authors notification (April 30) and the workshop (July 2), we will 
allow an ISSAC fast track for papers, i.e.,
(1) papers that do not make it to ISSAC on topics related to SC-Square will 
have the opportunity to be submitted late to SC-Square as full papers;
(2) papers that do make it to ISSAC on topics related to SC-Square will have 
the opportunity to be submitted late to SC-Square as presentation-only papers.


=== Scope ===

Symbolic Computation is concerned with the efficient algorithmic determination
of exact solutions to complicated mathematical problems. Satisfiability
Checking has recently started to tackle similar problems but with different
algorithmic and technological solutions.

The two communities share many central interests, but researchers from these 
two
communities rarely interact. Also, the lack of common or compatible interfaces
for tools is an obstacle to their fruitful combination. Bridges between the
communities in the form of common platforms and road-maps are necessary to
initiate an exchange, and to support and direct their interaction. The aim of
this workshop is to provide an opportunity to discuss, share knowledge and
experience across both communities.


=== Submitting to the Workshop ===

The workshop series has emerged from an H2020 FETOPEN CSA project 
"SC-Square", which ran from 2016 to 2018. It has been continued aiming at 
building bridges bewteen Satisfiability Checking and Symbolic Computation. It 
is open for submission and participation to everyone interested in the 
topics, whether or not they were members or associates of the original 
project.

The topics of interest include but are not limited to:

- Satisfiability Checking for Symbolic Computation
- Symbolic Computation for Satisfiability Checking
- Applications relying on both Symbolic Computation and Satisfiability 
Checking
- Combination of Symbolic Computation and Satisfiability Checking tools
- Quantifier elimination and decision procedures and their embedding into 
logic provers, including but not limited to SMT solvers, and computer algebra 
software

==== Submission guidelines ====

Submissions should be in English, formatted in Springer LNCS style and 
submitted
via EasyChair using this link:
https://easychair.org/conferences/?conf=scsquare2024

We invite three types of submissions:

(1) FULL PAPERS on research, case studies or tool development should present 
unpublished work not submitted elsewhere (with a limit of 16 pages, not 
counting references)
(2) EXTENDED ABSTRACTS on research, case studies or tool development should 
present unpublished (potentially ongoing) work not submitted elsewhere (2–4 
pages, not counting references)
(3) PRESENTATION-ONLY submissions on already published work, work to be 
published elsewhere, or work in progress on SC-Square related open problems 
or future challenges. Please submit an abstract for approval by the PC (with 
a limit of 2 pages).

To receive the appropriate level of peer review, please declare your category 
of
your submission by prefixing the title on the EasyChair form with "FP", "EA" 
or
"PO" accordingly.

For consistency, all submissions must use the LNCS style. Current llncs latex
files are available from " LaTeX2e Proceedings Templates download" at:
https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines

We plan to publish the proceedings of the workshop digital form, hosted with
CEUR-WS (see http://ceur-ws.org/). Authors may opt out of this, should they
prefer to publish the material elsewhere.

People from industry and business are warmly invited to submit papers to
describe their problems, challenges, goals, and expectations for the SC-square
community.


=== Workshop Co-Chairs ===

Daniela Kaufmann (TU Wien, AT)
Chris Brown (U. S. Naval Academy, USA)

=== Program Committee ===

Erika Abraham (RWTH Aachen University, DE)
Haniel Barbosa (Universidade Federal de Minas Gerais, BR)
Armin Biere (University of Freiburg, DE)
Anna Bigatti (University of Genova, IT)
Martin Brain (City University of London, UK)
Curtis Bright (University of Waterloo, CA)
David Cerna (Institute of Computer Science, Czech Academy of Sciences, CZ)
James H. Davenport (University of Bath, UK)
Matthew England (Coventry University, UK)
Pascal Fontaine (University of Liege, BE)
Alberto Griggio (Fondazione Bruno Kessler, IT)
Mikolas Janota (Czech Technical University in Prague, CZ)
Konstantin Korovin (The University of Manchester, UK)
Ilias Kotsireas (Wilfrid Laurier University, CA & Maplesoft)
Gereon Kremer (Certora, IL)
Alex Ozdemir (Stanford University, US)
Stefan Ratschan (Institute of Computer Science, Czech Academy of Sciences, CZ)
Christoph Scholl (University of Freiburg, DE)
Thomas Sturm (CNRS, FR & MPI Informatics, DE)
Bican Xia (Peking University, CN)




******************************************************************************

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


Important dates

    Tool and Benchmark Submission: June 12, 2024
    First Run: June 19, 2024
    Bugfix Deadline: June 26, 2024
    IJCAR: July 3-6, 2024





*************************************************************************
                            ThEdu'24
          Theorem proving components for Educational software
                          2 July 2024
             http://www.uc.pt/en/congressos/thedu/ThEdu24
*************************************************************************

THedu'24 Scope:

  Computer Theorem Proving is becoming a paradigm as well as a
  technological base for a new generation of educational software in
  science, technology, engineering and mathematics. The workshop brings
  together experts in automated deduction with experts in education in
  order to further clarify the shape of a new software generation and
  to discuss existing systems.    

Important Dates

 * Extended Abstracts: 10 April 2024
 * Author Notification: 8 May 2024
 * Workshop Day: 2 July 2024

Topics of interest include:

 * interactive and automated theorem provers designed or adapted
   for education;
 * methods of automated deduction applied to checking students' input;
 * combinations of deduction and computation enabling systems to
   propose next step guidance;
 * combination of symbolic artificial intelligence and machine
   learning for the teaching of proof and proving;
 * design of libraries of statements and/or formal proofs for use
   in educational systems;
 * graphical user interfaces for theorem proving in the classroom;
 * specific systems integrated in educational components such as
   dynamic geometry software, automatic provers providing readable
   output or explicit counter examples, etc.;
 * the role of logic and formal systems in the didactic of proof
   and proving in mathematics education;
 * experience reports about the use of automatic or interactive
   theorem provers for teaching.

Submission

  We welcome submission of extended abstracts and demonstration
  proposals presenting original unpublished work which is not been
  submitted for publication elsewhere.

  All accepted extended abstracts and demonstrations will be presented
  at the workshop. Abstracts will be made available online.

  Extended abstracts and demonstration proposals should be submitted
  via easychair, https://easychair.org/conferences/?conf=thedu24
  formatted according to http://www.easychair.org/publications/easychair.zip

  Extended abstracts and demonstration proposals should be 5-10 pages
  in length and are to be submitted in PDF format.

  At least one of the authors of each accepted extended
  abstract/demonstration proposal is expected to attend THedu'24 and
  presents their extended abstract/demonstration.


Program Committee (tentative)

  David Cerna, Johannes Kepler University, Austria
  Joao Marcos, Federal University of Rio Grande do Norte, Brazil 
  Filip Maric, University of Belgrade, Serbia
  Julien Narboux, University of Strasbourg, France, (co-chair)
  Walther Neuper,  Johannes Kepler University, Linz, Austria (co-chair)
  Pedro Quaresma, University of Coimbra, Portugal (co-chair)
  Philppe R. Richard, University of Montréal, Canada
  Vanda Santos, University of Aveiro, Portugal
  Anders Schlichtkrull, Aalborg University, Denmark
  Wolfgang Schreiner, Johannes Kepler University, Austria
  Athina Thoma, University of Southampton, UK
  M. Pilar Velez, Nebrija University, Spain
  Jorgen Villadsen, Technical University of Denmark, Denmark
  Kitty Yan, University of Toronto, Canada


Proceedings

  Abstracts and system descriptions will be available in ThEdu'24
  Web-wage. After the Workshop an open call for papers will be
  issued. It is expected that authors of accepted extended abstract
  can submit a substantially revised version, extended to 14-20 pages,
  for publication by the Electronic Proceedings in Theoretical
  Computer Science (EPTCS).
UNIF 2024 Call for Papers


******************************************************************************
                           Call for Papers
                              UNIF 2024
            The 38th International Workshop on Unification
                     Nancy, France, July 2, 2024
       A satellite workshop of CADE/IJCAR, affiliated with IJCAR
                 https://lat.inf.tu-dresden.de/unif2024
******************************************************************************

UNIF 2024 is the 38th event in a series of international meetings
devoted to unification theory and its applications. Unification is
concerned with the problem of making two given terms equal, either
syntactically or modulo an equational theory. It is a fundamental
process used in various areas of computer science, including automated
reasoning, term rewriting, logic programming, natural language
processing, program analysis, knowledge representation, types, etc.

The International Workshop on Unification (UNIF) is a forum for
researchers in unification theory and related fields to present recent
(even unfinished) work, and to discuss new ideas and trends. It is also
a good opportunity for students, young researchers and scientists working
in related areas to get an overview of the current state of the art in
unification theory.


Topics
------
A non-exhaustive list of topics of interest includes:

  * syntactic and equational unification algorithms
  * matching and constraint solving
  * higher-order unification
  * unification in modal, temporal, and description logics
  * admissibility of inference rules
  * narrowing
  * disunification
  * anti-unification
  * complexity issues  
  * combination methods
  * implementation techniques
  * applications


Submission
----------

Short papers or extended abstracts, up to 5 pages in EasyChair style,
should be submitted electronically as PDF files through the EasyChair
submission site:

  https://easychair.org/conferences/?conf=unif2024

Abstracts will be evaluated by the Program Committee regarding their
significance for the workshop. We allow submissions of work presented/
submitted in/to another conference.

Accepted abstracts will be presented at the workshop and included in
the informal proceedings of the workshop, available in electronic form
on the Web page of UNIF 2024. At least one of the authors should register
for the workshop.

Based on the number and quality of submissions we will decide whether to
organize a special journal issue.


Important Dates
---------------
  * Paper submission:                  April 18, 2024 (AoE)
  * Author notification:                  May 23, 2024 (AoE)
  * Camera-ready version:           June 7, 2024 (AoE)
  * UNIF 2024:                             July 2, 2024


Invited Speakers
----------------

To be announced.

******************************************************************************

5th International Workshop on Automated (Co)inductive Theorem Proving

******************************************************************************


We are delighted to announce the Fifth International Workshop on Automated 
(Co)inductive Theorem Proving, an event dedicated to the latest developments 
in inductive and coinductive methods for verification. This workshop is a 
significant gathering for researchers and practitioners in the field, 
providing an invaluable opportunity to explore current challenges and 
innovations in computational verification.

Key Themes:

Advances in inductive reasoning for recursive structures and loop-containing 
programs.
Developments in coinductive methods and their growing relevance in 
verification and industrial applications.
Cross-disciplinary collaboration to foster innovation in computational 
verification methods, including SMT, HOL, FOL, etc.

Featured Speakers Announcement: We are thrilled to announce that this year's 
workshop will feature at least two distinguished invited speakers: Prof. 
Dmitriy Traytel from the University of Copenhagen and Dr. Stefan Hetzl from 
the Vienna University of Technology.

Call for Abstracts: We invite you to submit an extended abstract showcasing 
your latest research, findings, or ongoing studies in the field of automated 
(co)inductive theorem proving. This is a fantastic platform to share your 
work with a diverse and expert audience, engage in intellectual exchange, and 
contribute to the advancement of the field. We welcome studies and findings 
published within the last five years.

Submission Guidelines: abstracts are to be sent to wait.in.france AT gmail.com

Length: 1-2 pages excluding references.

Recommended Format: easychair.cls

Important Dates:
Abstract Submission Deadline: 15 May.
Notification of Acceptance: 1 June.

Workshop Format: The workshop will feature in-depth tutorials, talks by 
leading experts, and a panel discussion for interactive dialogue. It is an 
ideal setting for networking, collaboration, and gaining new insights into 
the challenges and opportunities in automated theorem
proving.

Remote Participation: While on-site attendance is encouraged to fully benefit 
from the interactive nature of the workshop, provisions for remote 
participation will be available for wider accessibility.

Dissemination and Special Issue: Selected abstracts and presentation slides 
will be published on the workshop website. There's also a plan for a special 
journal issue based on the workshop's theme, subject to participant interest.

Join Us: Be a part of this stimulating event to discuss, learn, and 
contribute to the future of automated (co)inductive theorem proving. Don’t 
miss this opportunity to engage with a vibrant community and shape the future 
of verification techniques. We look forward to your submissions and 
participation!

For more information, please visit the workshop website 
(https://wait2024.github.io/) or contact the organizers, Yutaka Nagashima and 
Sorin Stratulat at wait.in.france AT gmail.com.


******************************************************************************

TPTP Tea Party

******************************************************************************
The TPTP Tea Party brings together developers and users of the TPTP World, 
including (but not limited to):

* The TPTP problem library and the TSTP solution library
* The TPTP languages, problem formats, and solution formats
* The SZS ontology
* SystemOnTPTP
* The CADE ATP System Competition (CASC)
* etc

The meeting aims to elicit feedback, suggestions, criticisms, etc, of these 
resources, in order to ensure that their continued development meets the 
needs of successful automated reasoning.
The meeting will be structured discussion following an agenda of topics that 
have been suggested and agreed upon in advance.

This year funding for participants is provided by Working Group 2 Automated 
Theorem Provers, COST Action 2011 EuroProofNet.
If you would like to receive announcements about the meeting, funding, and 
more, please join the TPTP World Google Group 
(https://groups.google.com/g/tptp-world)