hol-info — Discussion, questions and announcements related to the HOL System.

[Hol-info] Third CfP: Festschrift and Workshop in Honor of David Basin (Deadline extended to 11 June 2026)

[Achim D. B. <adb...@0x...>]

Dear Fellow Researchers!

Our dear colleague and friend David Basin is turning 65 in December 2026 and this has to be celebrated! We therefore organize a Festschrift and a Fest to celebrate his birthday and his extensive research contributions! 

The Fest/celebration itself will be held as a one-day event on the 15th of January 2027 at ETH Zürich. We have already checked that David is available. You do not have to keep it a secret - on the contrary, it is great if you share this message with anybody who might like to contribute!

We hereby cordially invite you to contribute an article to the Festschrift and present it at the Fest. We welcome contributions in all areas close to David's research and interests, including but not limited to security, privacy, formal methods, logic, automated reasoning, model checking, theorem proving, software engineering, bridge, juggling, biking and more. The articles will be lightly reviewed by the Festschrift committee, and the proceedings will be **published by Springer Heidelberg in the LNCS series**. David will of course love to receive a research article from you, but also short personal articles that celebrate the history and friendship with David will be very much appreciated.

We would like to set a deadline for submissions at the 21st of May 2026 via our submission site <https://easychair.org/conferences/?conf=feschi2027>. Articles should be formatted in Springer’s LNCS style and not exceed 5 pages for personal articles and 16 pages for scientific articles. If you have a work that you would like to contribute that does not fit into this page limit, it might be possible, but please reach out to us first. 

There will be no participation fee for the Fest and coffee breaks, lunch, and dinner will be included. Travel and accommodation costs are at the expense of the participants. We are happy to provide hotel suggestions for Zürich.   

Submission Information:

* Format: 16 pages in LNCS format, templates available at:
  <https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines>
* Submission: 
  <https://easychair.org/conferences/?conf=feschi2027>
* Website (under construction) with updates and further information: 
  <https://feschi2027.github.io/>
* Timeline:
  * Submission:   11 June 2026 (extended)
  * Notification: end of June 2026 (to be confirmed)
  * Camera Ready Copy: early September 2026 (to be confirmed)


Please let us know if you have any questions!

Best wishes
Achim D. Brucker (University of Exeter)
Sebastian Mödersheim (Danmarks Tekniske Universitet)
Christoph Sprenger (ETH Zürich)
Luca Viganò (King’s College London)





  
--  
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter  
           https://www.brucker.ch | https://logicalhacking.com/blog  
                         @adbrucker | @logicalhacking

[Hol-info] Call for Papers - ICFEM 2026 (17–20 November 2026, Southampton, UK)

[Asieh S. F. <A.S...@so...>]

The 27th International Conference on Formal Engineering Methods (ICFEM)

17–20 November 2026 , Southampton, UK

https://icfem2026.github.io/

ICFEM is an internationally leading conference series in formal methods and software engineering. Since 1997, ICFEM has served as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners from industry, academia, and government are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, as well as in theoretical work that promises to bring practical and tangible benefits. ICFEM has been hosted in many countries around the world.

This year, the 27th International Conference on Formal Engineering Methods will be held in Southampton, UK. ICFEM 2026 welcomes submissions from researchers and practitioners worldwide to advance the field of formal methods and software engineering.
Scope and Topics:

Authors are invited to submit high-quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to:

  *
Formal specification and modeling
  *
Formal approaches to fault prevention and detection
  *
Abstraction, refinement, and evolution
  *
Formal verification and validation
  *
Integration of formal methods and testing
  *
Integration of formal methods and review
  *
SAT/SMT solvers for software analysis and testing
  *
Practical formal methods
  *
Applications of formal methods
  *
Formal approaches to software maintenance
  *
Formal approaches to safety-critical system development
  *
Supporting tools for formal methods
  *
Formal methods for agile development
  *
Formal methods for human-machine pair programming
  *
Formal methods for and with AI
  *
Formal methods for Cyber-physical systems and IoT
  *
Formal methods for security
  *
Formal certification of products
  *
Industrial case studies

Important Dates (AoE):

  *   Abstract submission: 1 June 2026

  *   Full paper submission: 8 June 2026

  *   Notification: 8 August 2026

  *   Camera-ready: 7 September 2026

  *   Conference: 17–20 November 2026

More information and submission details:
https://icfem2026.github.io/


Co-located Workshop:

The Eighth International Workshop on Formal Methods for Autonomous Systems (FMAS 2026) is a two-day peer-reviewed international workshop that brings together researchers working on a range of techniques for the formal verification of autonomous systems, to present their work, discuss key challenges, and stimulate collaboration. Papers from previous editions of FMAS are indexed on DBLP: https://dblp.dagstuhl.de/db/conf/fmas/index.html. FMAS welcomes submissions that use formal methods to specify, model, or verify autonomous systems, in whole or in part. We are especially interested in work using integrated formal methods, where multiple (formal or non-formal) methods are combined during the software engineering process.

More details can be found on our website:
https://fmasworkshop.github.io/FMAS2026/

* Abstract Deadline: 14 August 2026 (AoE)
* Paper Deadline: 17 August 2026 (AoE)
* Notification: 6 October 2026 (AoE)
* Workshop: 17-19 November 2026

[Hol-info] MFCS 2026 - Last Call for Papers

[Sarah W. <sar...@ir...>]

========================================================

MFCS 2026 - Last Call for Papers

========================================================

The **51th conference on Mathematical Foundations of Computer Science** (MFCS) will take place in:

Paris, France August 24th-28th, 2026

**MFCS** is among the conferences with the longest history in the field — the first conference in the series was held already in 1972. Traditionally, the conference moved between the Czech Republic, Poland, and Slovakia; since 2013, the conference has traveled around Europe.

The conference will be preceded, on August 23, by the **Young Research Forum Workshop** intended for students and postdocs. The workshop will start at 13:00 and will feature talks/discussions around different topics related to research and academic life. After the workshop, there will be a social event with board games.

NEW: Up to **10 papers** will be accepted by the program committee, for which **no presence onsite** of an author is required. In this case, a reduced fee will be applied.


========================================================

Important dates and information

========================================================

Submissions: April 24th, 2026

Author notification: June 19th, 2026

Camera-ready version: June 26th, 2026

Conference: August 24th-28th, 2026 (YRF Workshop on August 23rd, afternoon)

Deadlines are firm; late submissions will not be considered. All dates are AoE.

Conference website: https://mfcs2026.irif.fr/

========================================================

Invited Speakers

========================================================

Jakub Orpšal (University of Birmingham, UK)
Damien Pous (CNRS, ENS Lyon, France)
Noga Ron-Zewi (University of Haifa, Israel)
Tatiana Starikovskaya (ENS Paris, France)
Ryan Williams (MIT, USA)

========================================================

Submission guidelines

========================================================

1) Papers must present original research on the theory of computer science. No prior publication and no simultaneous submission to other publication outlets (either a conference or a journal) is allowed. Authors are encouraged to also make full versions of their submissions freely accessible in an on-line repository such as arXiv.

2) Submissions take the form of an extended abstract of up-to 12 pages (LIPIcs document class), excluding a separate title page, references and a clearly labelled appendix. The appendix may consist either of omitted proofs or of a full version of the submission, and it will be read at the discretion of program committee members. The extended abstract has to present the merits of the paper and its main contributions clearly, and describe the key concepts and technical ideas used to obtain the results. Submissions must provide the proofs which can enable the main mathematical claims of the paper to be verified.

3) Submissions authored or co-authored by members of the program committee are allowed.

4) At the time of submission, authors may declare that they are unable to attend the conference in Paris and therefore cannot give an in-person presentation. This choice will not influence the evaluation of submissions by the Program Committee. The Program Committee will rank all papers irrespective of their presentation status. Approximately 80 papers will be selected for in-person presentation, and up to 10 papers will be accepted without presentation. All accepted papers will be published in the same proceedings. This option is intended for authors who wish to publish their results at the conference but, for various reasons (e.g., family or financial constraints), are unable to attend the conference in person.

5) At least one author of each accepted paper with presentation is expected to register for the conference, and give the talk in-person. At least one author of each accepted paper without in-person presentation is expected to register for the conference for a reduced fee, and for each such paper the authors are expected to provide a pre-recorded video of the paper presentation that will be made available on-line during the conference. (Pre-recorded videos of the other papers are optional.)

6) Papers authored only by students should be marked as such at the time of submission in order to be eligible for the best student paper award.

7) MFCS proceedings are published in the Leibniz International Proceedings in Informatics (LIPIcs) series. The camera-ready version of accepted papers will need to comply with the LIPIcs style.

8) All submissions should be made via HotCRP at https://mfcs26.hotcrp.com/.

========================================================

MFCS 2025 Programme Committee

========================================================

Michal Koucký (Charles University, Czech Republic) - chair
Daniela Petrișan (Université Paris Cité, IRIF, France) - co-chair

C. Aiswarya (Chennai Mathematical Institute, India)
Christel Baier (Technische Universität Dresden, Germany)
Ivona Bezáková (Rochester Institute of Technology, USA)
Markus Bläser (Saarland University, Germany)
Achim Blumensath (Masaryk University, Czech Republic)
Martin Böhm (University of Wrocław, Poland)
Édouard Bonnet (CNRS, ENS de Lyon, France)
Joshua Brakensiek (University of California, Berkeley, USA)
André Chailloux (Inria de Paris, France)
Panagiotis Charalampopoulos (King's College London, UK)
Lorenzo Clemente (University of Warsaw, Poland)
Ugo Dal Lago (University of Bologna, Italy)
Debarati Das (Pennsylvania State University, USA)
Samir Datta (Chennai Mathematical Institute, India)
Jakub Gajarský (Masaryk University and University of Warsaw, Czech Republic/Poland)
Anna Gál (University of Texas at Austin, USA)
Sumegha Garg (Rutgers University, USA)
Mayank Goswami (City University of New York, USA)
Florian Horn (Université Paris Cité, IRIF, CNRS, France)
Dušan Knop (Czech Technical University, Czech Republic)
Hanna Komlos (Max Planck Institute for Informatics, Germany)
Stephan Kreutzer (TU Berlin, Germany)
Bruno Loff (University of Lisbon, Portugal)
Wolfgang Merkle (Heidelberg University, Germany)
Igor Carboni Oliveira (University of Warwick, UK)
Kristýna Pekárková (AGH University of Krakow, Poland)
Thomas Place (University of Bordeaux, LABRI, France)
Cécilia Pradic (Swansea University, UK)
Jakub Przybyło (AGH University of Krakow, Poland)
Colin Riba (ENS de Lyon, LIP, France)
Kilian Risse (Lund University, Sweden)
Robert Robere (McGill University, Canada)
Michał Skrzypczak (University of Warsaw, Poland)
Paweł Sobociński (TalTech, Estonia)
Henning Urbat (FAU Erlangen-Nürnberg, Germany)
Pavel Veselý (Charles University, Czech Republic)
Philip Wellnitz (National Institute of Informatics, Japan)
Sarah Winter (Université Paris Cite, IRIF, CNRS, France)
James Worrell (University of Oxford, UK)
Standa Živný (University of Oxford, UK)

==========================================

[Hol-info] PAAR-2026: Deadline Extension

[<ge...@cs...>]

        PAAR-2026: 10TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING
                   -- co-located with IJCAR 2026  --
                   --    as part of FLoC 2026     --

                    July 25, 2026, Lisbon, Portugal

        Web site: https://paar2026.github.io/
        Submission link: https://submissions.floc26.org/paar
        Abstract registration deadline (extended): April 22, 2026 (AoE)
        Submission deadline (extended): April 26, 2026 (AoE)

Venue
-----
IJCAR 2026 in Lisbon, Portugal

Scope
-----

PAAR provides a forum for developers of automated reasoning tools to discuss and
compare different implementation techniques, and for users to discuss and
communicate their applications and requirements. The workshop will bring together
different groups to concentrate on practical aspects of the implementation and
application of automated reasoning tools. It will allow researchers to present
their work in progress, and to discuss new implementation techniques and applications.

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, 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;
* support tools for prover development;
* system descriptions and demos.
We are particularly interested in contributions that help the community to understand how to build useful reasoning systems in practice, and how to apply existing systems to real problems.

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

Important dates
---------------
* Abstract submission (extended): April 22, 2026 (AoE)
* Paper submission (extended): April 26, 2026 (AoE)
* Author notification (extended): May 20, 2026
* Camera-ready paper versions due: July 1, 2026
* Workshop: July 25, 2026

Program Committee
-----------------
* Jan Jakubuv, Czech Technical University in Prague, CZ
* Cezary Kaliszyk, University of Melbourne, AU
* Daniela Kaufmann, TU Wien, AT
* Boris Konev, University of Liverpool, UK
* Daniel Le Berre, CNRS - Université d'Artois, FR
* Ondrej Lengal, Brno University of Technology, CZ
* Tomer Libal, University of Luxembourg, LU
* Michael Rawson, University of Southampton, UK
* Philipp Ruemmer, Uppsala University, SE
* Renate A. Schmidt, The University of Manchester, UK
* Stephan Schulz, DHBW Stuttgart, DE
* Frieder Stolzenburg, Harz University of Applied Sciences, DE
* Geoff Sutcliffe, University of Miami, US
* Sophie Tourret, Inria and MPI for Informatics, DE
* Zsolt Zombori, Alfréd Rényi Institute of Mathematics, Hungarian Academy of Sciences, HU

[Hol-info] Fixed ARQNL 2026 - Call for Papers

[<ge...@cs...>]

--------------------------------------------------------------------
Sorry for the empty email yesterday folks ... nasty BOM characters!
--------------------------------------------------------------------
                    ARQNL 2026 - Call for Papers

                   6th International Workshop on
       Automated Reasoning in Quantified Non-Classical Logics
                    (associated with IJCAR 2026)
                   24 July 2026, Lisbon, Portugal

                     http://iltp.de/ARQNL-2026/

IMPORTANT DATES

Abstract submission: 27 April 2026
Paper submission: 4 May 2026
Author notification: 15 June 2026
Final paper version: 29 June 2026
Workshop: 24 July 2026


MOTIVATION

Non-classical logics   such as modal logics, conditional logics,
intuitionistic logic, description logics, logic of here-and-there,
temporal logics, linear logic, dynamic logic, deontic logics, fuzzy
logic, paraconsistent logic, relevance logic   have many applications
in AI, Computer Science, Philosophy, Linguistics and Mathematics.
Hence, automating the proof search in these logics is a crucial task.


AIMS AND SCOPE

The ARQNL workshop aims at fostering the development of proof
calculi, automated theorem proving systems and model finders for
all sorts of quantified non-classical logics. The workshop will
provide a forum for researchers to present and discuss recent
developments in this area. The contributions may range from theory
to system descriptions and implementations. Contributions may also
outline relevant applications, describe problem formalizations,
example problems, and benchmarks. We welcome contributions from
computer scientists, linguists, philosophers, and mathematicians.

Topics of the ARQNL workshop will cover all aspects related to the
automation of quantified non-classical logics, including but not
limited to:

* Proof theory, semantics, meta theory, and cut-elimination
* Proof search calculi, including sequent calculi, tableau calculi,
  connection calculi, resolution calculi, and instance-based calculi
* Modal logic, conditional logic, intuitionistic logic, description
  logic, temporal logic, linear logic, multivalued logic, dynamic
  logic, deontic logic, fuzzy logic, paraconsistent logic, relevance
  logic, free logic, and natural logic
* Techniques, strategies and heuristics to deal with first-order or
  higher-order quantification
* Implementation of theorem provers and experimental evaluations
* Problem libraries and benchmarking for theorem provers
* Applications, formalizations, and example problems
* User interfaces, proof representation, and syntax issues

ARQNL 2026 is associated with IJCAR 2026, the International Joint
Conference on Automated Reasoning.


PAPER SUBMISSIONS

Submissions of papers are solicited in three categories:
(A) Full papers (up to 15 pages excluding references)
(B) Short papers (up to 8 pages excluding references)
(C) Talk abstracts (up to 2 pages excluding references)

Submission is electronically, through EasyChair (see the ARQNL
website for further details). Submissions will be refereed by the
programme committee, and evaluated with respect to relevance,
originality, and correctness. Proceedings will be published in the
CEUR Workshop Proceedings.


PROGRAMME COMMITTEE (PC)

PC CHAIRS
Christoph Benzmueller (University of Bamberg)
Jens Otten (University of Pernambuco)
Revantha Ramanayake (University of Groningen)

PC COMMITTEE
(TBA)

--------------------------------------------------------------------

[Hol-info] Call for Contributions - Workshop on Formal Methods in Quantum Computing

[Laarman, A.W. (Alfons) <a.w...@li...>]

Call for Contributions

Second Workshop on Formal Methods in Quantum Computing
Lisbon, Portugal, July 18, 2026, co-located with FLoC 2026

Submission: Monday, May 11, AoE
Notification: June
Workshop: July 18
Website: https://fmqc-workshop.github.io/2026/call

=============================================
About

The recent surge in quantum computing, driven by substantial investments from governments and industry leaders such as IBM and Google, highlights its growing significance in both research and applications. Positioned at the intersection of quantum physics, applied mathematics, and theoretical computer science, the field presents vast opportunities for interdisciplinary collaboration and synergy.

This workshop, approaching quantum computing from a computer science perspective, seeks to bridge the gap between diverse research communities and foster the transfer of technology and methodologies from computer science, promoting cross-disciplinary innovation and progress.

=============================================
Call for Contributions

Workshop contributions can be extended abstracts as well as short and long papers (including already published results). There are no formatting guidelines for contributions. Accepted contributions will be invited for presentation at the workshop.

At the workshop, we will assess whether there is sufficient interest in a special issue.

Topics of interest include but are not limited to:

  *   ZX-Calculus
  *   Quantum Process Algebra
  *   Efficient Data Structures (e.g., Quantum Decision Diagrams and Tensor Networks)
  *   SAT/SMT Solving in Quantum Computing
  *   Programming Languages for Quantum Computing
  *   Quantum Topology
  *   Quantum Error Correction Codes (e.g., Topological Codes)
  *   Post-Quantum Cryptography
  *   Model Counting for Quantum Computing

=============================================
Confirmed Invited Speakers

Bob Coecke (keynote)
Yu-Fang Chen
Tim Coopmans
Johannes Klaus Fichte
Markus Hecher
Kuldeep Meel
Christopher Vasko

=============================================
Organizers

Max Bannach
Alfons Laarman
Jaco van de Pol
Christian Schilling

[Hol-info] LSFA 2026 - Call for Papers (Extended deadlines)

[Alexandre M. <ma...@ua...>]

Dear all,

We are pleased to inform you that, after multiple requests,  the submission deadlines for LSFA 2026 have been extended.

  - Abstract deadline:              April 17, 2026  April 20, 2026 (extended and final deadline)
  - Full paper deadline:           April 24, 2026  April 28, 2026 (extended and final deadline)

In the following, the updated Call for Papers.


----------------------------------------------------------------------------------------
LSFA 2026 - Call for Papers (Extended deadlines)

21st International Symposium on Logical and Semantic Frameworks with Applications
- LSFA 2026 -
18 - 19 July 2026
Lisbon, Portugal
https://lsfa-workshop.github.io/2026/

----------------------------------------------------------------------------------------

Logical and semantic frameworks are formal languages used to represent logics, languages, and systems.
These frameworks provide foundations for the formal specification of systems and programming languages,
supporting tool development and reasoning.
We are inviting formal submissions on the following topics, but not limited to:

Automated deduction
Applications of logical and/or semantic frameworks
Computational and logical properties of semantic frameworks
Formal semantics of languages and systems
Implementation of logical and/or semantic frameworks
Lambda and combinatory calculi
Logical aspects of computational complexity
Logical frameworks
Process calculi
Proof theory
Semantic frameworks
Specification languages and meta-languages
Type theory

The program committee is chaired by Valeria de Paiva, Topos Institute, Berkeley,and
Thaynara de Lima, Federal University of Goiás, Goiânia.


*** Formal Paper Submissions ***

Contributions should be written in English and submitted in the form of:
- full papers (with a maximum of 16 pages excluding references) or ;
- short papers (with a maximum of 6 pages excluding references).

They must be unpublished and not submitted simultaneously for publication elsewhere.
The papers should be prepared in latex using EPTCS style.
https://style.eptcs.org/
The submission should be in the form of a PDF file uploaded to HotCRP.
https://submissions.floc26.org/lsfa/
If software or data is relevant to a paper, a link that provides access
to the software/data must be provided to enable reproduction of results.

Following LSFA traditions, besides Proceedings, we are considering
publishing a Special Issue LSFA 25+26 (more details regarding past
publications at https://lsfa-workshop.github.io/).

*** Important Dates ***

  - Abstract deadline:             April 17, 2026 April 20, 2026 (Final deadline)
  - Full paper deadline:           April 24, 2026 April 28, 2026 (Final deadline)
  - Notification of acceptance:    May 25, 2026
  - Conference:                    July 18-19, 2026

-------------------------------------------------------
Alexandre Madeira
http://sweet.ua.pt/madeira/

[Hol-info] [Vardi-list] Ask the Candidates for ACM President

[Moshe V. <va...@ri...>]

Please help to get the word out by posting on social media!


The 2026 Candidates for ACM President are Jens Palsberg from UCLA and Elisa 
Bertino from Purdue. Each candidate will provide an official statement to 
appear with the ACM election materials . In addition, we are soliciting 
questions from the computing community that we will send to both candidates. 
Questions will be collected through a Google form and through a forum at 
OnlineQuestions.org (Event 16933). The questions will be 
collected/collated/edited by moderator, Moshe Vardi.

You need not be an ACM member to post questions!

https://www.cs.rice.edu/~vardi/acmelection2026/

Moderator: Moshe Vardi


_______________________________________________
Vardi-list mailing list
Var...@ma...
https://mailman.rice.edu/mailman/listinfo/vardi-list

[Hol-info] LSFA 2026 -- Last call for papers

[Alexandre M. <ma...@ua...>]

----------------------------------------------------------------------------------------
LSFA 2026 - Last Call for Papers

21st International Symposium on Logical and Semantic Frameworks with Applications
- LSFA 2026 -
18 - 19 July 2026
Lisbon, Portugal
https://lsfa-workshop.github.io/2026/

----------------------------------------------------------------------------------------

Logical and semantic frameworks are formal languages used to represent logics, languages, and systems.
These frameworks provide foundations for the formal specification of systems and programming languages,
supporting tool development and reasoning.
We are inviting formal submissions on the following topics, but not limited to:

Automated deduction
Applications of logical and/or semantic frameworks
Computational and logical properties of semantic frameworks
Formal semantics of languages and systems
Implementation of logical and/or semantic frameworks
Lambda and combinatory calculi
Logical aspects of computational complexity
Logical frameworks
Process calculi
Proof theory
Semantic frameworks
Specification languages and meta-languages
Type theory

The program committee is chaired by Valeria de Paiva, Topos Institute, Berkeley,and
Thaynara de Lima, Federal University of Goiás, Goiânia.


*** Formal Paper Submissions ***

Contributions should be written in English and submitted in the form of:
- full papers (with a maximum of 16 pages excluding references) or ;
- short papers (with a maximum of 6 pages excluding references).

They must be unpublished and not submitted simultaneously for publication elsewhere.
The papers should be prepared in latex using EPTCS style.
https://style.eptcs.org/
The submission should be in the form of a PDF file uploaded to HotCRP.
https://submissions.floc26.org/lsfa/
If software or data is relevant to a paper, a link that provides access
to the software/data must be provided to enable reproduction of results.

Following LSFA traditions, besides Proceedings, we are considering
publishing a Special Issue LSFA 25+26 (more details regarding past
publications at https://lsfa-workshop.github.io/).

*** Important Dates ***

  - Abstract deadline:             April 17, 2026
  - Full paper deadline:           April 24, 2026
  - Notification of acceptance:    May 25, 2026
  - Conference:                    July 18-19, 2026

-------------------------------------------------------
Alexandre Madeira
http://sweet.ua.pt/madeira/

[Hol-info] [cfp] (LPNMR 2026) 18th International Conference on Logic Programming and Non-monotonic Reasoning

[Antonio I. <ant...@un...>]

*** Please accept our apologies if you receive multiple copies of this CFP
***

====================================================
LPNMR 2026 - Preliminary Call for Papers

18th International Conference on Logic Programming and Non-monotonic
Reasoning (LPNMR 2026)
Klagenfurt, Austria | September 7-11, 2026
Website: https://lpnmr2026.aics.aau.at
Contact us: lpn...@ea...
Submission: https://easychair.org/conferences/?conf=lpnmr2026
====================================================

====================================================
IMPORTANT DATES
====================================================

- Paper registration: April 30, 2026
- Submission deadline: May 7, 2026
- Final notification: June 11, 2026
- Final versions due: July 2, 2026
- Conference: September 7-11, 2026

====================================================
AIMS AND SCOPE
====================================================

LPNMR 2026 is the eighteenth in the series of international conferences on
logic programming and non-monotonic reasoning. LPNMR is a forum for
exchanging ideas on declarative logic programming, non-monotonic reasoning,
and knowledge representation. The aim of the conference is to facilitate
interactions between researchers and practitioners interested in the design
and implementation of logic-based programming languages and database
systems, and those working in knowledge representation and non-monotonic
reasoning. LPNMR strives to encompass theoretical and experimental studies
that have led or will lead to advances in declarative programming and
knowledge representation, as well as their use in practical applications.
LPNMR 2026 aims to bring together researchers from LPNMR and neighboring
areas in order to share research experiences, promote collaboration and
identify directions for joint future research.

====================================================
TOPICS
====================================================

Authors are invited to submit papers presenting original and unpublished
research on all aspects of non-monotonic approaches in logic programming
and knowledge representation. Conference topics include, but are not
limited to:

- Foundations of LPNMR: Semantics of new and existing languages; Action
languages; Causality; Formalization of Commonsense Reasoning and
understanding its laws and nature; Relationships among formalisms;
Complexity and expressive power; Inference algorithms and heuristics for
LPNMR systems; Extensions of traditional LPNMR languages such as new
logical connectives or new inference capabilities; Updates, revision, and
other operations on LPNMR systems; Uncertainty in LPNMR systems

- Implementation of LPNMR systems: System descriptions, comparisons, and
evaluations; Algorithms and novel techniques for efficient evaluation;
LPNMR benchmarks; Systems using LPNMR subsystems

- Applications of LPNMR: Use of LPNMR in Commonsense Reasoning and other
areas of knowledge representation; LPNMR languages and algorithms in
planning, diagnosis, and argumentation; Reasoning with preferences,
decision making, and policies; Applications of LPNMR languages in data
integration and exchange systems; Software engineering and model checking;
Applications of LPNMR to bioinformatics, linguistics, psychology, and other
sciences; Integration of LPNMR systems with other computational paradigms

====================================================
SUBMISSION AND PUBLICATION
====================================================

LPNMR 2026 welcomes submissions of long papers (up to 15 pages) or short
papers (up to 8 pages) in the following categories:

- Technical papers
- System papers
- Application papers

The indicated number of pages includes the title page, figures, tables,
references, and appendix. All submissions will be peer-reviewed and
accepted papers will appear in the conference proceedings published in the
Springer's Lecture Notes in Artificial Intelligence (LNAI) series.
Submissions must be written in English, present original research, and be
formatted according to Springer's guidelines and technical instructions
available at:

https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines

LPNMR 2026 will not accept any paper which, at the time of submission, is
under review or has already been published or accepted for publication in a
journal or another conference. Authors are also required not to submit
their papers elsewhere during LPNMR's review period. However, these
restrictions do not apply to workshops (e.g., ASPOCP 2026) with a limited
audience and without archival proceedings.

====================================================
FAST JOURNAL TRACK FOR BEST PAPERS
====================================================

Two award-winning papers (Best Paper Award and Best Student Paper Award of
LPNMR 2026) will be invited for publication in either the Artificial
Intelligence Journal or the Journal of Artificial Intelligence Research,
based on the preference of the authors.
Additionally, about 5-7 high-quality papers with a logic programming focus
will be invited for publication in the journal of Theory and Practice of
Logic Programming.

====================================================
VENUE
====================================================

LPNMR 2026 will be held on the campus of the University of Klagenfurt in
September 2026. Klagenfurt is the capital of the state Carinthia in the
south of Austria. The name Klagenfurt was first mentioned in the late 12th
century and legend has it that Klagenfurt was founded after a couple of
brave men had slain the abominable Lindwurm, a winged dragon. The city is
located next to the lake Woerthersee, one of the most beautiful lakes in
Austria, surrounded by several forest-covered hills and mountains. Being a
small city, with a Renaissance-style city center reflecting 800 years of
history and with an Italian influence, Klagenfurt is a pleasant place to
live and work.

====================================================
ORGANISING COMMITTEE
====================================================

General Chair:
        Wolfgang Faber, University of Klagenfurt, Austria

Program Co-chairs:
        Martin Gebser, University of Klagenfurt, Austria
        Yanhong Annie Liu, Stony Brook University, USA

[Hol-info] ProoVer-2026: First Proof Verifier Competition

[<ge...@cs...>]

ProoVer-2026: First Proof Verifier Competition
27th July 2026, Lisbon, Portugal
Co-located with CASC-J13 at IJCAR 2026 / FLoC 2026

We are pleased to announce ProoVer-2026, the first edition of the annual
competition for automatic proof verifiers. In ProoVer, verifiers are
given a mix of valid proofs and *evil* proofs in which tricky errors
have been deliberately introduced. The goal is to correctly identify
which proofs are valid and which are flawed.

Participants submit proof verifier systems that receive FOF (First-Order
Form) problems paired with TSTP-format proofs, and must determine
whether each proof is valid or flawed. For this first edition, only a
limited set of inference rules and formula roles will be used: `axiom`,
`conjecture`, `negated_conjecture`, as well as `plain` steps which
will be either skolemization steps or purely deductive steps whose
correctness can be delegated to an external ATP. What precisely makes a 
proof correct or incorrect will not be fully specified, and it is one 
of the main task  to handle edge cases and decide what should or should 
not be considered an acceptable proof according to the TSTP standard and 
general proof-checking principles.

Each system is evaluated on 100 problems: 50 valid proofs and 50 evil
proofs, with a time limit of 30 seconds per problem (wall-clock). The
output format is one SZS status line per problem, indicating whether the
proof is verified, failed, or uncertain. The competition infrastructure
is shared with CASC (StarExec).

IMPORTANT DATES (Anywhere on Earth)
------------------------------------
   System registration deadline   : 29th June 2026
   System descriptions deadline   : 13th July 2026
   Formal ProoVer registration    : 13th July 2026
   System delivery deadline       : 13th July 2026
   Competition start              : 10:00am, 27th July 2026

As ProoVer is held jointly with CASC, we will have a shared dinner and
if you participate in both competitions, registration fees are charged
only once (but you will get goodies for both! Great deal!).

For more information, please visit https://proover-competition.github.io/

The competition organizers are Julie Cailler and Simon Guilloud. If you
have any questions about the competition, please email us!

[Hol-info] [C.A.R.L.A. 2026 - Second Call for Papers] 2nd Workshop on Cognitive Architectures for Robotics: LLMs and Logic in Action, Lisbon, Portugal | July 26

[Manuel A. B. S. <man...@un...>]

*2nd Call for Papers*

2nd Workshop on Cognitive Architectures for Robotics: LLMs and Logic in
Action (C.A.R.L.A. 2026)
July *18*, 2026 | Lisbon, Portugal
<https://carla-ws.github.io/web/>https://ws-carla.github.io/web/

Part of FLoC 2026

https://www.floc26.org/




*IMPORTANT DATES (AoE):*


- Paper registration: *May 8*
- Paper submission: *May 16*
- Notification: *May 24*
- Camera-Ready Deadline: *June 19*


Accepted papers will be presented as posters, with a subset selected for

oral presentations.

The workshop will take place in person at FLoC 2026, with the option

for authors to participate virtually.


*GENERAL INFORMATION*


The Workshop on Cognitive Architectures for Robotics: LLMs and Logic in

Action (CARLA) seeks to transform the landscape of intelligent behaviors by

pioneering the integration of large language models (LLMs), symbolic

reasoning, and logic solvers into autonomous systems.



As robotics advances toward real-world applications requiring adaptability,

safety, and complex decision-making, this workshop focuses on harnessing

the synergy between data-driven learning models and symbolic, logic-based

systems to advance automation.



This year, the workshop further expands its scope to explicitly include

simulated environments as first-class experimental and methodological

tools. In particular, CARLA emphasizes the use of videogames and digital

twins as scalable, controllable, and safe testbeds for cognitive robotics

research. These environments enable systematic investigation of embodied

reasoning, LLM-driven planning, and logic-based decision-making under

diverse and dynamic conditions that would be difficult or costly to

reproduce in physical settings.



By bridging cognitive architectures with the structured management of

virtual applications, CARLA aims to foster principled approaches to

transferring knowledge and behaviors learned in simulation to real-world

systems, while supporting reproducibility and benchmarking across research

efforts.





*SCOPE*


CARLA invites research contributions and discussions in the following
focus areas:


*- Knowledge Representation for Robotics:* Frameworks and methodologies
   for integrating structured knowledge into robotic architectures.

*- LLMs as Cognitive Engines:* Leveraging LLMs to process complex commands,
  generate actionable   insights, and facilitate human-robot communication.

*- Neuro-Symbolic Systems in Robotics:* Hybrid approaches combining
  neural networks with symbolic reasoning for decision-making and task
execution.

*- Logic Solvers in Robotic Control:* Employing constraint solvers, SAT
solvers,
  or theorem provers for autonomous planning and reliable decision-making.

*- Adaptive and Safe Robotic Architectures:* Strategies for real-time
adaptation
  and coordination in robotic systems using LLMs and symbolic logic.

*- Human-Robot Collaboration:* Innovations in language-driven interactions,
  focusing on usability, interpretability, and reliability in diverse
scenarios.

*- Challenges of LLM Deployment in Robotics:* Addressing safety,
robustness,
  and ethical considerations when integrating LLMs into robotic systems.

*- LLM-Driven Planning and Problem Solving:* Enabling robots to perform
  dynamic planning and adapt to novel situations using LLM-guided reasoning.

* - Video Games and Virtual Worlds as Testbeds for Cognitive Robotics: *
Leveraging the virtual environments
  of videogames and digital twins as controlled and scalable testbeds for
investigating
  embodied reasoning, LLM-driven planning, and logic-based decision-making,
  enabling systematic experimentation in safe and reproducible settings.


*SUBMISSIONS*


*CARLA welcomes the following types of submissions:*


- Original Research Papers: Presenting novel research contributions
  aligned with the workshop’s focus areas.

- Work-in-Progress Reports: Sharing preliminary findings and
  ongoing research efforts.

- Position Papers: Discussing emerging challenges, visionary ideas,
  and future directions at the intersection of robotics, LLMs, and logic
solvers.

- Already Presented Works: Contributions that have been previously
  presented at other venues but are relevant to the workshop themes.
  Such works can be resubmitted to foster further discussion and
exploration.



*Submissions should adhere to the following guidelines:*


- Maximum of 12 pages (excluding references) for full papers and 6 pages
(excluding references) for short papers.

- Formatting must follow the CEURART style:
https://ceur-ws.org/HOWTOSUBMIT.html

- All submissions must be in English and submitted in PDF format.



Accepted original contributions may be published in the CEUR-WS
Proceedings,

together with other FLoC workshops, subject to compliance with the
publishing requirements.



Accepted non-original contributions will be showcased on the

workshop website with links to the original publication, where available.


*Submission site*
Submissions will be managed via the FLoC submission system.

Papers will remain private during the review process. All authors must
maintain

up-to-date profiles to ensure proper conflict-of-interest management and
paper matching.

Incomplete profiles may result in desk rejection.



*Submit papers through the dedicated C.A.R.L.A. submission system:*
https://submissions.floc26.org/carla/


*Anonymity*


The workshop follows a single-blind review process.

Submissions must not be anonymized by removing author names,

affiliations, and acknowledgments.




*ORGANIZATION*


- Fabrizio Lo Scudo, University of Calabria, Italy

- Denise Angilica, University of Calabria, Italy

- Sotirios Batsakis, Hellenic Mediterranean University, Greece

- Manuel Alejandro Borroto Santana, University of Calabria, Italy

[Hol-info] FMICS 2026: Last Call for Papers!

[Rozier, Kristin-Y. [A. E] <kyr...@ia...>]

**********************************************************
   Formal Methods for Industrial Critical Systems (FMICS)
   31st International Conference, co-located with CONFEST

https://confest-2026.github.io/fmics/

                  2 - 4 September 2026
         University of Liverpool, Liverpool, UK
**********************************************************


Theme of the Conference:
-----------------------
The aim of the FMICS conference series is to provide a forum for 
researchers an practitioners who are interested in the development and 
application of formal methods in industry. FMICS brings together 
scientists and engineers who are active in the area of formal methods 
and interested in exchanging their experiences in the industrial usage 
of these methods. The FMICS conference series also strives to promote 
research and development for the improvement of formal methods and tools 
for industrial applications.

FMICS is the ERCIM Working Group conference on Formal Methods for 
Industrial Critical Systems, and it is the key conference in the 
intersection of industrial applications and Formal Methods.


Topics of Interest:
-------------------
We encourage submissions on cross-cutting approaches that bring together 
formal methods and industrial applications.
     * Formal specification, including specification elicitation, 
validation, debugging, sanity checking, revision, coverage, and 
explainability.
     * Case studies and experience reports on industrial applications of 
formal methods, focusing on lessons learned or identification of new 
research directions.
     * Methods, techniques, and tools to support automated analysis, 
certification, debugging, learning, optimization, and transformation of 
complex, distributed, real-time, embedded, mobile, and autonomous systems.
     * Verification and validation methods (model checking, theorem 
proving, SAT/SMT constraint solving, abstract interpretation, etc.) that 
address shortcomings of existing methods with respect to their 
industrial applicability (e.g., scalability and usability issues, tool 
qualification, and certification).
     * Transfer to industry and impact of adoption of formal methods on 
the development process and associated costs in industry. Application of 
formal methods in standardization and industrial forums.


Important Dates:
----------------
Abstract Submission: 10 Apr 2026
Paper Submission:    17 Apr 2026
Paper Notifications:  1 Jun 2026
Camera-ready Papers: 15 Jun 2026
Conference:         2-4 Sep 2026


Submission Details:
-------------------
Papers must describe original research work and results. Submitted 
papers must not have previously appeared in a journal or conference with 
published proceedings and must not be concurrently submitted to any 
other peer-reviewed workshop, symposium, conference, or archival 
journal. Any partial overlap with any such published or concurrently 
submitted paper must be clearly indicated.

Submissions should clearly motivate relevance to industrial 
applications. Case study papers should identify lessons learned, 
validate theoretical results (such as scalability of methods), and 
provide specific motivation for further research and development.

Papers should not exceed 15 pages (excluding references) formatted 
according to the Springer author guidelines LNCS style. Any appendices 
(beyond the above page limit) might not be considered in the review 
process. All submissions will be reviewed by at least three members of 
the Programme Committee, which will make a selection among the 
submissions based on the novelty, soundness, and applicability of the 
presented ideas and results. Papers must be written in English and 
submitted in PDF format at the EasyChair submission site:

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

For all papers with experimental results, we strongly recommend 
providing reviewers with an artifact that they can use to reproduce 
results, e.g., via a paper website.


ERCIM Award:
------------
As in best FMICS tradition, the paper with the best contributions to 
Software Science and Technology will be honoured with the EASST ERCIM award.


Keynote Speakers:
-----------------
Julia Badger, NASA Johnson Space Center, USA
Colin O’Halloran, D-RisQ, UK
Ezio Bartocci, TU Wien, Austria (Shared CONFEST Keynote)
Ichiro Hasuo, National Institute of Informatics, Japan (Shared CONFEST 
Keynote)

Organizers:
-----------
Peter Gorm Larsen (Aarhus University, Denmark)
Kristin Yvonne Rozier (Iowa State University, USA)


Programme Committee:
--------------------
Jefferson Andrade, Instituto Federal do Espírito Santo
Ramesh Bharadwaj, U.S. Navy
John Fitzgerald, Newcastle University
John Hatcliff, Kansas State University
Joseph Kiniry, Galois, Inc.
Tsutomu Kobayashi, Japan Aerospace Exploration Agency (JAXA)
Tiziana Margaria, University of Limerick
Mieke Massink, CNR-ISTI, Pisa, Italy
Stephan Merz, INRIA Nancy
Stefan Mitsch, DePaul University
Rosemary Monahan, Maynooth University
Tomohiro Oda, Software Research Associates, Inc.
Claudio Pinello, Collins Aerospace
Anne Remke, WWU Münster
Cristina Seceleanu, Mälardalen University
Martina Seidl, Johannes Kepler University Linz
Giulia Sindoni, University of Leeds
Bernhard Steffen, University of Dortmund
Laura Titolo, Code Metal
Christoph Torens, German Aerospace Center, Institute of Flight Systems
Jaco van de Pol, Aarhus University and University of Twente
Marcel Verhoef, European Space Agency
Virginie Wiels, ONERA / DTIS
Anton Wijs, Eindhoven University of Technology
Naijun Zhan, Institute of Software, Chinese Academy of Sciences

-- 
  ____________________________________________________________
                                     __
            /\                       \ \_____
           /  \                   ###[==_____>
          /    \                     /_/      __
         /  __  \                             \ \_____
         | (  ) |                          ###[==_____>
        /| /\/\ |\                            /_/
       / | |  | | \
      /  |=|==|=|  \       Kristin Yvonne Rozier, Ph.D.
    /    | |  | |    \     Associate Professor, Iowa State Univ
   / USA | ~||~ |NASA \    Departments of Aerospace Engineering,
  |______|  ~~  |______|     Computer Science, Mathematics, and
         (__||__)            Electrical and Computer Engineering
         /_\  /_\
         !!!  !!!https://laboratory.temporallogic.org

[Hol-info] MFCS 2026 - Second Call for Papers

[Sarah W. <sar...@ir...>]

========================================================

MFCS 2026 - Second Call for Papers

========================================================

The 51th conference on Mathematical Foundations of Computer Science (MFCS) will take place in:

Paris, France August 24th-28th, 2026

MFCS is among the conferences with the longest history in the field — the first conference in the series was held already in 1972. Traditionally, the conference moved between the Czech Republic, Poland, and Slovakia; since 2013, the conference has traveled around Europe.

The conference will be preceded, on August 23, by the Young Research Forum Workshop intended for students and postdocs.

NEW: Up to 10 papers will be accepted by the program committee, for which no presence onsite is required.

========================================================

Important dates and information

========================================================

Submissions: April 24th, 2026

Author notification: June 19th, 2026

Camera-ready version: June 26th, 2026

Conference: August 24th-28th, 2026 (YRF Workshop on August 23rd, afternoon)

Deadlines are firm; late submissions will not be considered. All dates are AoE.

Conference website: https://mfcs2026.irif.fr/

========================================================

Invited Speakers

========================================================

Jakub Orpšal (University of Birmingham, UK)
Damien Pous (CNRS, ENS Lyon, France)
Noga Ron-Zewi (University of Haifa, Israel)
Tatiana Starikovskaya (ENS Paris, France)
Ryan Williams (MIT, USA)

========================================================

Submission guidelines

========================================================

1) Papers must present original research on the theory of computer science. No prior publication and no simultaneous submission to other publication outlets (either a conference or a journal) is allowed. Authors are encouraged to also make full versions of their submissions freely accessible in an on-line repository such as arXiv.

2) Submissions take the form of an extended abstract of up-to 12 pages (LIPIcs document class), excluding title page, references and a clearly labelled appendix. The appendix may consist either of omitted proofs or of a full version of the submission, and it will be read at the discretion of program committee members. The extended abstract has to present the merits of the paper and its main contributions clearly, and describe the key concepts and technical ideas used to obtain the results. Submissions must provide the proofs which can enable the main mathematical claims of the paper to be verified.

3) Submissions authored or co-authored by members of the program committee are allowed.

4) At the time of submission, authors may declare that they are unable to attend the conference in Paris and therefore cannot give an in-person presentation. This choice will not influence the evaluation of submissions by the Program Committee. The Program Committee will rank all papers irrespective of their presentation status. Approximately 80 papers will be selected for in-person presentation, and up to 10 papers will be accepted without presentation. All accepted papers will be published in the same proceedings. This option is intended for authors who wish to publish their results at the conference but, for various reasons (e.g., family or financial constraints), are unable to attend the conference in person.

5) At least one author of each accepted paper with presentation is expected to register for the conference, and give the talk in-person. At least one author of each accepted paper without in-person presentation is expected to register for the conference for a reduced fee, and for each such paper the authors are expected to provide a pre-recorded video of the paper presentation that will be made available on-line during the conference. (Pre-recorded videos of the other papers are optional.)

6) Papers authored only by students should be marked as such at the time of submission in order to be eligible for the best student paper award.

7) MFCS proceedings are published in the Leibniz International Proceedings in Informatics (LIPIcs) series. The camera-ready version of accepted papers will need to comply with the LIPIcs style.

========================================================

MFCS 2025 Programme Committee

========================================================

Michal Koucký (Charles University, Czech Republic) - chair
Daniela Petrișan (Université Paris Cité, IRIF, France) - co-chair

C. Aiswarya (Chennai Mathematical Institute, India)
Christel Baier (Technische Universität Dresden, Germany)
Ivona Bezáková (Rochester Institute of Technology, USA)
Markus Bläser (Saarland University, Germany)
Achim Blumensath (Masaryk University, Czech Republic)
Martin Böhm (University of Wrocław, Poland)
Édouard Bonnet (CNRS, ENS de Lyon, France)
Joshua Brakensiek (University of California, Berkeley, USA)
André Chailloux (Inria de Paris, France)
Panagiotis Charalampopoulos (King's College London, UK)
Lorenzo Clemente (University of Warsaw, Poland)
Ugo Dal Lago (University of Bologna, Italy)
Debarati Das (Pennsylvania State University, USA)
Samir Datta (Chennai Mathematical Institute, India)
Jakub Gajarský (Masaryk University and University of Warsaw, Czech Republic/Poland)
Anna Gál (University of Texas at Austin, USA)
Sumegha Garg (Rutgers University, USA)
Mayank Goswami (City University of New York, USA)
Florian Horn (Université Paris Cité, IRIF, CNRS, France)
Dušan Knop (Czech Technical University, Czech Republic)
Hanna Komlos (Max Planck Institute for Informatics, Germany)
Stephan Kreutzer (TU Berlin, Germany)
Bruno Loff (University of Lisbon, Portugal)
Wolfgang Merkle (Heidelberg University, Germany)
Igor Carboni Oliveira (University of Warwick, UK)
Kristýna Pekárková (AGH University of Krakow, Poland)
Thomas Place (University of Bordeaux, LABRI, France)
Cécilia Pradic (Swansea University, UK)
Jakub Przybyło (AGH University of Krakow, Poland)
Colin Riba (ENS de Lyon, LIP, France)
Kilian Risse (Lund University, Sweden)
Robert Robere (McGill University, Canada)
Michał Skrzypczak (University of Warsaw, Poland)
Paweł Sobociński (TalTech, Estonia)
Henning Urbat (FAU Erlangen-Nürnberg, Germany)
Pavel Veselý (Charles University, Czech Republic)
Philip Wellnitz (National Institute of Informatics, Japan)
Sarah Winter (Université Paris Cite, IRIF, CNRS, France)
James Worrell (University of Oxford, UK)
Standa Živný (University of Oxford, UK)

==========================================

[Hol-info] LSFA 2026, deadline extension

[Alexandre M. <ma...@ua...>]

----------------------------------------------------------------------------------------
LSFA 2026 - Call for Papers      [Extended deadline!!!]

21st International Symposium on Logical and Semantic Frameworks with Applications
- LSFA 2026 -
18 - 19 July 2026
Lisbon, Portugal
https://lsfa-workshop.github.io/2026/

----------------------------------------------------------------------------------------

Logical and semantic frameworks are formal languages used to represent logics, languages and systems.
These frameworks provide foundations for the formal specification of systems and programming languages,
supporting tool development and reasoning.
We are inviting formal submissions on the following topics, but not limited to:

Automated deduction
Applications of logical and/or semantic frameworks
Computational and logical properties of semantic frameworks
Formal semantics of languages and systems
Implementation of logical and/or semantic frameworks
Lambda and combinatory calculi
Logical aspects of computational complexity
Logical frameworks
Process calculi
Proof theory
Semantic frameworks
Specification languages and meta-languages
Type theory

The program committee is chaired by Valeria de Paiva, Topos Institute, Berkeley and
Thaynara de Lima, Federal University of Goiás, Goiânia.


*** Formal Paper Submissions ***

Contributions should be written in English and submitted in the form of:
- full papers (with a maximum of 16 pages excluding references) or ;
- short papers (with a maximum of 6 pages excluding references).

They must be unpublished and not submitted simultaneously for publication elsewhere.
The papers should be prepared in latex using EPTCS style.
https://style.eptcs.org/
The submission should be in the form of a PDF file uploaded to HotCRP.
https://submissions.floc26.org/lsfa/
If software or data is relevant to a paper, a link that provides access
to the software/data must be provided to enable reproduction of results.

Following LSFA traditions, besides Proceedings, we are considering
publishing a Special Issue LSFA 25+26 (more details regarding past
publications at https://lsfa-workshop.github.io/).

*** Important Dates ***

  - Abstract deadline:             April 17, 2026
  - Full paper deadline:           April 24, 2026
  - Notification of acceptance:    May 25, 2026
  - Conference:                    July 18-19, 2026

-------------------------------------------------------
Alexandre Madeira
http://sweet.ua.pt/madeira/

[Hol-info] [Vardi-list] Accommodation for Vardi in Lisbon, Portugal - July 13-25, 2026 - Building II - ISCTE (fwd)

[Moshe V. <va...@ri...>]

Dear Colleague:

If you get an email like the one below, in connection with FLoC'26, please 
be aware that this is a SCAM!

Sheesh,
Moshe



---------- Forwarded message ----------
Date: Tue, 24 Mar 2026 14:33:33 +0000
From: Global Travel <ope...@gt...>
To: va...@ri...
Subject: Accommodation for Vardi in Lisbon, Portugal - July 13-25,
     2026 - Building II - ISCTE

Good day Vardi,

Kindly inform us of your arrival and departure dates in Lisbon to secure 
the space for your stay this July for the conference.

If the itinerary isn't confirmed yet, it's a flexible reservation that can 
be modified or cancelled without any additional fees.

We would appreciate your reply to enable us to proceed with your reservation.

Kindly note that reservations are completely flexible and refundable until 14  days before the arrival date.

Best Regards,

Contact the Global Travel Team via our Support Centres:
United Kingdom Office : (+44) 20 8123 9190
Canada Office : (+1) 833 833 2107

Our team is ready to assist!

[Hol-info] AI for Math Summer Fellowship -- Copilots for Isabelle (Sheffield / Copenhagen / London): application deadline April 10

[Andrei P. <and...@gm...>]

Dear Colleagues,

We are pleased to advertise an AI for Math Summer Fellowship
opportunity on the project "Copilots for Isabelle: Learning Logical
Structure for a Better Proving Experience".

The general call and application details (including an application
link) can be found here:

https://docs.google.com/document/d/1tXlT2A2NyLi_N-Fn1Q5zwG6J0b8Cwhzj/edit

Please note that the application deadline is April 10, and the
internship will run for 10 weeks, from June 15 to August 21, 2026.

In this project, the selected fellow will work with researchers at the
University of Sheffield, University of Copenhagen, and King’s College
London on developing AI-based copilots for the Isabelle proof
assistant. The aim is to leverage the rich structure of interactive
proofs to build intelligent tools that assist with proof development,
documentation, and automation.

The fellowship offers the opportunity to work on topics such as:
-- generating polished proofs from informal or partial drafts,
-- automatically producing documentation for Isabelle/ML code,
-- adapting and tuning LLMs for proof tasks.

The position is open to undergraduate, master’s and PhD students, and
can be carried out in Sheffield, Copenhagen, or London (with support
for travel if needed).

Please see the attached project description for further details.

Best wishes,
Andrei, Dmitriy and Mohammad

[Hol-info] PhD posiiton in Computer Science - Verified Microarchitectural Security

[Roberto G. <rob...@kt...>]

Dear colleagues,
The School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology (Stockholm, Sweden) is seeking a highly motivated PhD student in Computer Science, with a focus on formal verification, hardware/software security, and microarchitectural side-channel analysis.

Full details about the position, eligibility requirements, and how to apply are available here:
https://www.kth.se/lediga-jobb/907809

The position is part of the research project µVerif: Rigorous Security Analysis of Computer Microarchitecture, jointly supervised by Associate Professor Roberto Guanciale (https://www.kth.se/profile/robertog) and Assistant Professor Hamed Nemati (https://hnemati.github.io). The successful candidate will be embedded in a strong and collaborative research environment spanning system security, formal methods, and low-level software and hardware verification, and will be affiliated with both research groups.

Modern processor architectures rely on aggressive performance optimisations, such as speculative and out-of-order execution, which, while highly effective for performance, introduce subtle and severe security vulnerabilities (e.g., Spectre-class attacks). These vulnerabilities fundamentally challenge the assumption that software-level security guarantees hold on real hardware.

The project focuses on securing modern processor microarchitectures. Aggressive optimisations such as speculative and out-of-order execution, which significantly improve performance, introduce serious security vulnerabilities (e.g., Spectre-like attacks). These vulnerabilities break the traditional assumption that security properties verified at the software level hold on real hardware.

This project aims to bridge the gap between formal program analysis and security on real hardware by: Developing formal models of speculation and microarchitectural information flow; Automatically extracting security-relevant models from RTL; Evaluating the techniques on open-source RISC-V processor cores. The long-term goal is to enable scalable, rigorous, and hardware-relevant verification of security properties for real-world systems.

The PhD student is expected to:
- Conduct research in formal methods and computer security.
- Develop formal models of microarchitectural behaviour and speculation.
- Design and implement analysis and model-extraction tools based on SMT solving and symbolic reasoning.
- Apply the developed techniques to open-source processor designs (e.g., RISC-V).

We are looking for candidates with a strong background in computer science, and a particular interest in formal methods, security, or computer architecture.

We would greatly appreciate it if you could share this announcement with potentially interested candidates.

Please feel free to contact me for informal inquiries.

Best regards,
Roberto Guanciale
Associate Professor
KTH Royal Institute of Technology
Stockholm, Sweden
rob...@kt...

[Hol-info] Fwd: 2026 Alonzo Church Award, Call for Nominations

[Marcelo F. <mar...@cl...>]

The 2026 Alonzo Church Award for Outstanding Contributions to Logic and
Computation

CALL FOR NOMINATIONS

Deadline 2026 April 17

INTRODUCTION

An annual award, called the Alonzo Church Award for Outstanding
Contributions to Logic and Computation, was established in 2015 by the ACM
Special Interest Group for Logic and Computation (SIGLOG), the European
Association for Theoretical Computer Science (EATCS), and the European
Association for Computer Science Logic (EACSL).  The award is for an
outstanding contribution represented by a paper or by a small group of
papers published within the past 25 years.  This time span allows the
lasting impact and depth of the contribution to have been established. The
award can be given to an individual, or to a group of individuals who have
collaborated on the research. For the rules governing this award, see <
https://siglog.org/alonzo-church-award/>, <
https://www.eatcs.org/index.php/church-award/>, and <
https://www.eacsl.org/alonzo-church-award/>.

THE 2025 AWARD

The 2025 Alonzo Church Award was given to Paul Blain Levy for his
fundamental study of effectful λ-calculi through the Call-by-Push-Value
(CBPV) calculus, which has had major impact on logical calculi, programming
language semantics, and their applications to computer science.

ELIGIBILITY AND NOMINATIONS

The contribution must have appeared in a paper or papers published within
the past 25 years.  Thus, for the 2026 award, the cut-off date is January
1, 2001.  When a paper has appeared in a conference and then in a journal,
the date of the journal publication will determine the cut-off date.  In
addition, the contribution must not yet have received recognition via a
major award, such as the Turing Award, the Kanellakis Award, or the Goedel
Prize.  (The nominee(s) may have received such awards for other
contributions.)  While the contribution can consist of conference or
journal papers, journal papers will be given a preference.

Nominations for the 2026 award are now being solicited.  The nominating
letter must summarise the contribution and make the case that it is
fundamental and outstanding.  The nominating letter can have multiple
co-signers.  Self-nominations are excluded.  Nominations must include: a
proposed citation (up to 25 words); a succinct (100-250 words) description
of the contribution; and a detailed statement (not exceeding four pages) to
justify the nomination.  Nominations may also be accompanied by supporting
letters and other evidence of worthiness.  Nominations for the 2026 award
are automatically considered for all future editions of the award, until
they receive the award or the nominated papers are no longer eligible.

PROCEDURE AND DEADLINE

Nominations to the 2026 Alonzo Church Award, taking the form of a single
PDF file, should be sent by 2026 April 17 to Marcelo Fiore <
mar...@cl...>.

AWARD COMMITTEE

The 2026 Alonzo Church Award Committee consists of the following five
members: Mikolaj Bojanczyk, Thomas Colcombet, Anuj Dawar, Marcelo Fiore
(Chair), and Alexandra Silva.

[Hol-info] FSCD workshops at FLoC

[<ge...@cs...>]

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

GaLoP: Games for Logic and Programming Languages

GALOP is an international workshop on formal models for program interaction. It has a
broad interest, in both the foundational aspects of these models as well as their
practical applications.

FULL INFORMATION AT: https://galop-2026.lacl.fr/

- submission deadline: 6 May 2026
- what to submit: an abstract up to 2 pages, describing a talk
- notification: 26 May 2026

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

ITRS: Intersection Types and Related Systems

The ITRS 2026 workshop aims to bring together researchers working on both the theory and
practical applications of systems based on intersection types and related approaches.

FULL INFORMATION AT: https://itrs2026.tu-dortmund.de/

- submission deadline: 15 May 2026
- what to submit: 3-5 pages, excluding bibliography
- notification: 29 May 2026

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

IWC: International Workshop on Confluence

IWC seeks to provide a forum for researchers interested in the topic of confluence to
exchange and share new developments in the field. The workshop will enable discussion on
theoretical results, new problems, applications, implementations and benchmarks, and
share the current state-of-the-art on the development of confluence tools.

FULL INFORMATION AT: https://iwc2026.github.io/

- submission deadline: 20 April 2026
- what to submit: extended abstract or short paper of at most 5 pages
- notification: 26 May 2026

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

LSFA: Logical and Semantic Frameworks, with Applications

Logical and semantic frameworks are formal languages that represent logics and languages,
as well as computational, AI and deductive systems. The LSFA series is a platform that
fosters collaboration, bringing together theoreticians and practitioners.

FULL INFORMATION AT: https://lsfa-workshop.github.io/2026/

- abstract deadline: 30 March 2026
- submission deadline: 4 April 2026
- what to submit: full paper of at most 16 pages
- notification: 4 May 2026

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

LFMTP: Logical Frameworks and Meta Languages: Theory and Practice

This workshop will bring together designers, implementors and practitioners to discuss
various aspects impinging on the structure and utility of logical frameworks, including
the treatment of variable binding, inductive and co-inductive reasoning techniques and
the expressiveness and lucidity of the reasoning process.

FULL INFORMATION AT: https://lfmtp.github.io/lfmtp-page/workshops/2026/

- abstract deadline: 21 April 2026
- submission deadline: 28 April 2026
- what to submit: full papers (at most 15 pages), system descriptions
(at most 10 pages)
   and work in progress reports (at most 8 pages)
- notification: 29 May 2026

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

TGD: Tribute to Gilles Dowek

----------------------------------------------------------------------------
                   Call for talk proposals
                Tribute to Gilles Dowek
             July 18, 2026, Lisbon, Portugal
https://deducteam.gitlabpages.inria.fr/tribute-to-gilles/
----------------------------------------------------------------------------

This workshop aims at celebrating Gilles Dowek's influence in logic and computer science.

We welcome short or long talk proposals on the connections between logic, computation,
and possibly physical theories, reviews of work done by Gilles or with him, or of results
obtained thanks to Gilles' influence or related to Gilles' work. Topics include, but are
not limited to, logical frameworks, proof systems interoperability, ecumenical proof
libraries, automated deduction, quantum programming languages, and physics-inspired
models of computation.

- Submission website: https://submissions.floc26.org/tgd
- Submission deadline: 3 May 2026
- Notification: 15 May 2026

----------------------------------------------------------------------------

[Hol-info] Second CfP: Festschrift and Workshop in Honor of David Basin (Deadline: 21st May 2026)

[Achim D. B. <adb...@0x...>]

Dear Fellow Researchers!

Our dear colleague and friend David Basin is turning 65 in December 2026 and this has to be celebrated! We therefore organize a Festschrift and a Fest to celebrate his birthday and his extensive research contributions! 

The Fest/celebration itself will be held as a one-day event on the 15th of January 2027 at ETH Zürich. We have already checked that David is available. You do not have to keep it a secret - on the contrary, it is great if you share this message with anybody who might like to contribute!

We hereby cordially invite you to contribute an article to the Festschrift and present it at the Fest. We welcome contributions in all areas close to David's research and interests, including but not limited to security, privacy, formal methods, logic, automated reasoning, model checking, theorem proving, software engineering, bridge, juggling, biking and more. The articles will be lightly reviewed by the Festschrift committee, and the proceedings will be **published by Springer Heidelberg in the LNCS series**. David will of course love to receive a research article from you, but also short personal articles that celebrate the history and friendship with David will be very much appreciated.

We would like to set a deadline for submissions at the 21st of May 2026 via our submission site <https://easychair.org/conferences/?conf=feschi2027>. Articles should be formatted in Springer’s LNCS style and not exceed 5 pages for personal articles and 16 pages for scientific articles. If you have a work that you would like to contribute that does not fit into this page limit, it might be possible, but please reach out to us first. 

There will be no participation fee for the Fest and coffee breaks, lunch, and dinner will be included. Travel and accommodation costs are at the expense of the participants. We are happy to provide hotel suggestions for Zürich.   

Submission Information:

* Format: 16 pages in LNCS format, templates available at:
  <https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines>
* Submission: 
  <https://easychair.org/conferences/?conf=feschi2027>
* Website (under construction) with updates and further information: 
  <https://feschi2027.github.io/>
* Timeline:
  * Submission:   21 May 2026
  * Notification: end of June 2026 (to be confirmed)
  * Camera Ready Copy: early September 2026 (to be confirmed)


Please let us know if you have any questions!

Best wishes
Achim D. Brucker (University of Exeter)
Sebastian Mödersheim (Danmarks Tekniske Universitet)
Christoph Sprenger (ETH Zürich)
Luca Viganò (King’s College London)





  
--  
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter  
           https://www.brucker.ch | https://logicalhacking.com/blog  
                         @adbrucker | @logicalhacking

[Hol-info] PhD Position in Bridging the Gap Between Mathematical Numbers and Software Systems (Deadline: 2026-03-22)

[Achim D. B. <adb...@0x...>]

We are seeking an enthusiastic PhD candidate with a strong background
in computer science, software engineering, mathematics, or closely
related fields. Expertise in formal methods such as program reasoning,
programming language semantics, model checking, theorem proving, or
computational logic is essential.
      
Mathematical models, e.g., describing physical systems or
cryptographic algorithms, rely on ideal numbers. For instance,
mathematical integers are infinite and mathematical reals continuous
and infinite. Computers work with finite approximations that are
bounded (i.e., there is a smallest and largest number) and
discrete. This "digital gap" between mathematical models and actual
systems is a challenge when implementing safety-critical or
security-critical systems: for example, autonomous aircraft or
self-driving cars require high-precision representations of their
position to avoid collisions. Hence, not considering the approximation
of the approximative representation of numbers in computers can result
in crashes that can endanger the life of humans. Moreover, many
security-critical systems, not limited to cryptographic algorithms,
rely on the correct handling of over- and underflows in integer
computations. Actually, underflow- and overflow bugs are a root cause
for a large number vulnerabilities exploited by cyber security
criminal, e.g., for stealing digital currencies worth several billion
of dollars. While this is not a new problem (e.g., already in 1982, an
float conversion error in a trading systems at the Vancouver Stock
Exchange resulted in a loss of several millions of US dollars), an
integrated development method preventing such bugs is still not
available.
      
This PhD project will address this challenge by developing a rigour
approach for developing systems relying on precise representations of
numbers, using the interactive theorem prover Isabelle/HOL. The PhD
project can focus on 
1) the formalisation of concrete representations of machine numbers
   (e.g., IEEE754, POSIT, Decimal Floating Point, Fixed Point
   Arithmetic), their (algebraic) properties, and relationship to
   abstract mathematical numbers;
2) the formalisation and verification of numerical or cryptographic
   algorithms, establishing a reusable verified library, or
3) the development of an end-to-end refinement approach from
    mathematical models to machine representations.
      
The PhD will be jointly supervised by Prof. Dr. Achim Brucker
(<a.b...@ex...>) and Prof. Dr. Burkhart Wolff
(<bur...@un...>), leading to a joint
degree from the University of Exeter and the University of
Paris-Saclay.
      
Information about the programme can be found at
* <https://www.exeter.ac.uk/study/pg-research/funding/phdfunding/paris-saclay/>
* <https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&site=PSaclay>

All applications have to be made via the ADUM system:
<https://adum.fr/as/ed/voirproposition.pl?langue=en&matricule_prop=71068&site=PSaclay>,
latest on the 22nd of March 2026.

Best,
Achim (and Bukrhart)


  
--  
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter  
           https://www.brucker.ch | https://logicalhacking.com/blog  
                         @adbrucker | @logicalhacking

[Hol-info] Call for Participation: Workshop on AI and Theorem Provers in Mathematics (AITPM)

[Achim D. B. <adb...@0x...>]

The Workshop on AI and Theorem Provers in Mathematics (AITPM) will explore with leading experts some of the recent developments related to the use of AI and theorem provers in mathematics as well as the perspectives for such future use.

- Workshop website: https://aitpm.github.io/
- Venue: Online 
- Attendance is free.
- Registration: https://forms.office.com/e/c7gth3Rb6Q
- Date:  8. - 10. April 2026

## Speakers

- Kevin Buzzard (Imperial College)  
- Minhyong Kim (International Centre for Mathematical Sciences, Edinburgh)
- Yang-Hui He (London Institute for Mathematical Sciences)
- Paola Iannone (University of Edinburgh)
- Shinichi Mochizuki (Research Institute for Mathematical Sciences Kyoto)
- Leonardo De Moura (Amazon Web Services)
- Lawrence Paulson (University Cambridge)
- Chelsea Edmonds (University of Western Australia)
- Patrick Massot (University Paris Saclay)

## Programme Schedule  (to be confirmed)

The preliminary schedule of the workshop is:

* April 8th 2026 
  * 08:00-09:00 Kevin Buzzard
  * 09:15-10:15 Paola Iannone
  * 10:45-11:45 Lawrence Paulson
  * 12:00-13:00 Discussion/panel session
* April 9th 2026
  * 08:00-09:00 Chelsea Edmond
  * 09:15-10:15 Yang Hui Heen 
  * 10:45-11:45 Shinichi Mochizuki 
  * 12:00-13:00 Discussion session
* April 10th 2026
  * 15:00-16:00 Patrick Massot
  * 16:15-17:15 Leonardo De Moura
  * 17:45-18:45 Natarajan Shankar (tbc)
  * 19:00-20:00 Discussion/panel session and closure

All times are BST (i.e., London, observing daylight saving time).

## Organisers

- Mohamed Saidi (Department of Mathematics and Statistics, University of Exeter)
- Barrie Cooper (Department of Mathematics and Statistics, University of Exeter)
- Gihan Marasingha (Department of Mathematics and Statistics, University of Exeter)
- Achim D. Brucker (Department of Computer Science, University of Exeter)
- Diego Marmsoler (Department of Computer Science, University of Exeter)


  
--  
Prof. Achim Brucker | Chair in Cybersecurity & Head of Group | University of Exeter  
           https://www.brucker.ch | https://logicalhacking.com/blog  
                         @adbrucker | @logicalhacking

[Hol-info] AITP 2026 - Call for Contributions

[Josef U. <jos...@gm...>]

CALL FOR CONTRIBUTIONS

Artificial Intelligence and Theorem Proving,
AITP 2026
August 30 - September 4, 2026, Aussois, France

http://aitp-conference.org/2026

Deadline: May 5, 2026
https://easychair.org/conferences/?conf=aitp2026

BACKGROUND
Large-scale semantic processing and strong computer assistance of
mathematics and science is our inevitable future. New combinations of
AI and reasoning methods and tools deployed over large mathematical
and scientific corpora will be instrumental to this task.  The AITP
conference is the forum for discussing how to get there as soon as
possible, and the force driving the progress towards that.

TOPICS

- AI, machine learning and big-data methods in theorem proving and
mathematics.
- Collaboration between automated and interactive theorem proving, in
  particular their AI/ML aspects.
- Common-sense reasoning and reasoning in science, relations to general AI.
- Alignment and joint processing of formal, semi-formal, and informal
   libraries, Formal Abstracts.
- Methods for large-scale computer understanding of mathematics and science.
- Combinations of linguistic/learning-based and semantic/reasoning methods
- Formal verification of AI and machine learning algorithms, explainable AI
.


SESSIONS

There will be several focused sessions on AI for ATP, ITP,
mathematics, relations to general AI (AGI), Formal Abstracts,
linguistic processing of mathematics/science, modern AI and big-data
methods, and several sessions with contributed talks. The focused
sessions will be based on invited talks and discussion
oriented. AITP'26 is planned as an in-person conference.


CONFIRMED PARTICIPANTS/SPEAKERS/PANELISTS (TBC)

Michael R. Douglas, Stony Brook University
Mario Carneiro, Chalmers University and University of Gothenburg
Simon Frieder, University of Oxford
Thibault Gauthier, AI4REASON
Ben Goertzel, SingularityNET
Georges Gonthier, INRIA
Sean Holden, University of Cambridge
Jan Jakubuv, Czech Technical University in Prague
Mikoláš Janota, Czech Technical University in Prague
Moa Johansson, Chalmers University and University of Gothenburg
Cezary Kaliszyk, University of Melbourne
Peter Koepke, University of Bonn
Konstantin Korovin, The University of Manchester
Michael Kinyon, University of Denver
Miroslav Olsak, University of Cambridge
Auguste Poiroux, EPFL and Math Inc
Aarne Ranta, Chalmers University and University of Gothenburg
Michael Rawson, University of Southampton, UK
Stephan Schulz, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Christian Szegedy, AletheAI
Josef Urban, AI4REASON and University of Gothenburg
Robert Veroff, University of New Mexico
Andrei Voronkov, Easychair and University of Manchester
Zsolt Zombori, Alfréd Rényi Institute of Mathematics


INVITED TALKS (TBC)

Simon Frieder, AIMO and all that (TBC)
Ben Goertzel, TBA
Michael Kinyon, TBA
Auguste Poiroux, (Auto-)Formalization of the Fields Medal Sphere Packing
Results (TBC)
Christian Szegedy, TBA
Robert Veroff, Automating the search for proofs of open conjectures
Andrei Voronkov, TBA


CONTRIBUTED TALKS
We solicit contributed talks. Selection of those will be based on
extended abstracts/short papers of 2 pages formatted with easychair.cls.
Submission is via EasyChair (
https://easychair.org/conferences/?conf=aitp2026).
The extended abstracts are considered non-archival.
The contributed talks have to be presented in-person.


DATES
Submission deadline: May 5, 2026
Author notification: June 20, 2026
Conference registration: TBA
Camera-ready versions: TBA
Conference: August 31 - September 5, 2026


PROGRAM COMMITTEE (TBC)

Guillaume Baudart, INRIA
David Cerna, Czech Academy of Sciences
Michael R. Douglas (co-chair), Stony Brook University
Ulrich Furbach, University of Koblenz
Thibault Gauthier, Czech Technical University in Prague
Aishik Ghosh, Georgia Tech
Georges Gonthier, INRIA
Thomas C. Hales (co-chair), University of Pittsburgh
Sean Holden, University of Cambridge
Mikoláš Janota, Czech Technical University in Prague
Moa Johansson, Chalmers University and University of Gothenburg
Cezary Kaliszyk (co-chair), University of Melbourne
Michael Kinyon, University of Denver
Peter Koepke, University of Bonn
Konstantin Korovin, The University of Manchester
Bartosz Piotrowski, IDEAS NCBR
Michael Rawson (co-chair), University of Southampton, UK
Stephan Schulz (co-chair), DHBW Stuttgart
Sho Sonoda, RIKEN AIP
Martin Suda, Czech Technical University in Prague
Josef Urban, AI4REASON and University of Gothenburg
Zsolt Zombori, Alfréd Rényi Institute of Mathematics


LOCATION AND PRICE

The conference will take place from August 30 to September 4 2026
in the CNRS Paul-Langevin Conference Center
(https://www.caes.cnrs.fr/sejours/centre-paul-langevin/) located in
the mountain village of Aussois in Savoy.  Dominated by the "Dent
Parrachée", one of the highest peaks of La Vanoise, Aussois is located
on a sunny plateau at 1500 m altitude, offering a magnificent panorama
of the surrounding mountains and a direct access to the park of La
Vanoise in summer and downhill ski slopes or cross country slopes in
winter. The total price for accommodation, full board and registration for
the five days will be around 650 EUR.

ARRIVAL/DEPARTURE

Aussois is less than 2h from the airports of Lyon, Geneve, Chambery,
Annecy, Grenoble and Turin. There are trains and buses from these
airports. Aussois is 7km from the Modane TGV station with direct
trains from/to Paris. We will organize a bus for the participants from
there to Aussois. Further buses to these airports / station can be
found at http://www.altibus.com/ .

ORGANIZERS
Georges Gonthier, Cezary Kaliszyk and Josef Urban

[Hol-info] LSFA 2026 Second Call for Papers

[Alexandre M. <ma...@ua...>]

----------------------------------------------------------------------------------------
LSFA 2026 Second Call for Papers

21st International Symposium on Logical and Semantic Frameworks with Applications
- LSFA 2026 -
18 - 19 July 2026
Lisbon, Portugal

https://lsfa-workshop.github.io/2026/

----------------------------------------------------------------------------------------

Logical and semantic frameworks are formal languages used to represent logics, languages and systems.
These frameworks provide foundations for the formal specification of systems and programming languages,
supporting tool development and reasoning.
We are inviting formal submissions on the following topics, but not limited to:

Automated deduction
Applications of logical and/or semantic frameworks
Computational and logical properties of semantic frameworks
Formal semantics of languages and systems
Implementation of logical and/or semantic frameworks
Lambda and combinatory calculi
Logical aspects of computational complexity
Logical frameworks
Process calculi
Proof theory
Semantic frameworks
Specification languages and meta-languages
Type theory

The program committee is chaired by Valeria de Paiva, Topos Institute, Berkeley and Thaynara de Lima, Federal University of Goiás, Goiânia.


*** Formal Paper Submissions ***

Contributions should be written in English and submitted in the form of:
- full papers (with a maximum of 16 pages excluding references) or ;
- short papers (with a maximum of 6 pages excluding references).

They must be unpublished and not submitted simultaneously for publication elsewhere.
The papers should be prepared in latex using EPTCS style.
https://style.eptcs.org/
The submission should be in the form of a PDF file uploaded to HotCRP.
https://submissions.floc26.org/lsfa/
If software or data is relevant to a paper, a link that provides access
to the software/data must be provided to enable reproduction of results.

Following LSFA traditions, besides Proceedings, we are considering
publishing a Special Issue LSFA 25+26 (more details regarding past
publications at https://lsfa-workshop.github.io/).

*** Important Dates ***

  - Abstract deadline:             March 30, 2026
  - Full paper deadline:           April 4, 2026
  - Notification of acceptance:    May 4, 2026
  - Conference:                    July 18-19, 2026

-------------------------------------------------------
Alexandre Madeira
http://sweet.ua.pt/madeira/