Gilles Dowek died on the 21st of July 2025, aged 58. He was diagnosed with lung cancer in early 2022. The sad news of his illness spread in the scientific community in the spring of that year, as he decided to let it be known. He fought the terrible illness with admirable courage, but had to succumb after over three years of resistance, leaving the automated reasoning community deeply saddened by such a premature loss.
Gilles Dowek was a research director at INRIA, where he founded and led the Deducteam unit, and a professor at Ecole Normale Supérieure Paris-Saclay. During his career, Gilles made numerous contributions to automated reasoning, logic, theoretical computer science, philosophy, and education.
Gilles started as a student of Herbrand Award winner Gérard Huet, defending a thesis entitled "Démonstration Automatique dans le Calcul des Constructions" ("Automated Theorem Proving in the Calculus of Constructions") at Université Paris Diderot in 1991. He proceeded to develop a research program centered on deduction in higher order logic, solving several key problems about higher-order matching and higher-order unification. His chapter on "Higher-Order Unification and Matching" in the Handbook of Automated Reasoning (2001) summarized this part of his research.
Together with Thérèse Hardin and Claude Kirchner, Gilles Dowek initiated the paradigm of deduction modulo, a powerful generalization of the classical concepts of unification and rewriting modulo an equational theory. With his PhD student Denis Cousineau, Gilles proved in 2007 that all functional pure type systems can be expressed in the lambda-Pi calculus modulo rewriting.
Gilles was concerned with balancing the advantages and disadvantages of the existence of the many different proof systems that are developed and used in the automated reasoning community. As mathematics becomes computerized, the variety of proof systems may even challenge the universality of mathematical truth. Thus, Gilles applied his leadership to start and promote the development of the Dedukti logical framework to encode and translate proofs from one proof system to another. To this end, he also inspired the creation of the EuroProofNet COST action (2021-2025).
Gilles was a brilliant speaker, and many certainly remember the breadth and elegance of his IJCAR invited talk "From the universality of mathematical truth to the interoperability of proof systems," given at Haifa, Israel, during the 2022 Federated Logic Conference. Gilles was already ill at that time, and, sadly, had to limit his conference participation, but for those who had the chance, his conversation during coffee break after his invited talk was as pleasant and gifted as always.
Gilles was also an excellent teacher and supervised or co-supervised many PhD students. He authored several books presenting topics in computer science, logic, and philosophy to the general public. His commitment to teaching and his love for computer science led him to engage in promoting the teaching of computer science in high school, contributing to the definition of the corresponding curriculum. His many and diverse accomplishments were recognized by several awards from the French Academy of Sciences.
Together with Alessandro Armando and Peter Baumgartner, Gilles Dowek was Program Co-Chair of IJCAR 2008, hosted by Peter Baumgartner in Sydney, Australia. Then, he served as Program Chair of RTA-25 at the 2014 Federated Logic Conference during the Vienna Summer of Logic. From 2021 to 2022, he was vice leader of Working Group 4 on proof libraries in the above mentioned EuroProofNet COST action.
Everyone who met him will miss his kindness, humour, and hindsight. His passing is a great loss for the automated reasoning community and beyond.
Peter B. Andrews, an American mathematician and Professor Emeritus at Carnegie Mellon University, passed away on April 21, 2025, at the age of 87. Andrews was a leading figure in the theory and applications of higher-order logic and automated reasoning.
Peter Andrews received his Ph.D. in Mathematics from Princeton University in 1964, where he was advised by the highly influential logician Alonzo Church. Andrews joined the Mathematics Department at Carnegie Mellon University in Pittsburgh in 1963 and remained there for 49 years, retiring in 2012.
Andrews's research was motivated by a desire to develop tools that could enhance human reasoning with a vision for the eventual formalization of virtually all mathematical, scientific, and technical knowledge, as well as the development of automated reasoning tools to assist in managing this knowledge. He made progress on this vision by focusing his work primarily on automated deduction within Church's version of higher-order logic based on the Simple Theory of Types.
A major achievement in his career was leading the development of TPS (Theorem Proving System), an automated theorem prover for higher-order classical logic. A subsystem, ETPS (Educational Theorem Proving System), was created to help students learn logic by interactively constructing natural deduction proofs. Andrews worked on this system with his research assistants from 1974 until his retirement.
Andrews also made significant contributions to the foundations of symbolic logic. He is notable for identifying a gap in Jacques Herbrand's proof of the eponymous Herbrand's theorem for first-order logic and corresponding with Burton Dreben about it. This collaboration led to a joint paper with Dreben and St\aa l Aanderaa in 1963, which provided a counterexample to a key lemma in Herbrand's proof. It was later discovered that Kurt G\"odel had privately noted a similar error decades earlier, though he did not publish it. Andrews also noted an error in Leon Henkin's definition of general models for higher-order logic and provided a fix for it.
His book ``An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof,'' praised for its clear and concise presentation of logic, is one of the few textbooks that covers both the syntactic and semantic sides of higher-order logic using Church's Simple Theory of Types.
In recognition of his significant contributions to automated deduction, Peter Andrews received the Herbrand Award in 2003. A Festschrift titled "Reasoning in Simple Type Theory" was published in 2008 in honor of his 70th birthday.
Peter is survived by his wife of nearly 40 years, Catherine Clair ``Cate'' Andrews, his sons, Lyle Andrews and Bruce (Tobi) Andrews, and his former wife, Linda Fitch. He will be missed.
The Federated Logic Conference (FLoC) 2026 will bring together the world's leading researchers in logic and computer science. It will be hosted at the Institut Universitaire de Lisbonne (ISCTE), Lisbon, Portugal. The FoPSS summer school co-located with FLoC.
The program includes the following conferences and workshops:
Researchers and practitioners are invited to submit proposals for workshops on topics in the field of computer science, related to logic in the broad sense. Each workshop proposal may be affiliated with one of the FLoC 2026 conferences, or it may be submitted as a general FLoC 2026 workshop without reference to a specific conference.
Important Dates
More information is available on the conference's web page.
Nominations for four CADE trustee positions were being sought, in preparation for the elections to be held after CADE-30.
The following candidates were nominated and their statements, in alphabetical order, are below:
The elections will take place soon after the release of the newsletter and use the CIVS platform.
In the last three years, I was CADE president. If I am re-elected, I will continue trying to ensure that CADE keeps on being the main conference for all research in the area of automated deduction. Therefore, the scope of CADE should remain as broad as possible. CADE should be open to any aspect of automated deduction and it should cover everything from theoretical results and practical contributions up to applications of automated reasoning.
I also think that it is very important to attract tool submissions, and to organize tool competitions co-located with CADE. (Since its foundation in 2004, I have been active in the termination competition, which took place during IJCAR/CADE several times.)
I think the current organization of CADE as a stand-alone event every second year, within IJCAR every other year, and within FLoC every four years is still a very good solution to guarantee the visibility of CADE on its own, while keeping in close contact with neighboring meetings and fields.
Following the poll among the CADE community, I negotiated with LIPIcs to ensure that the proceedings of CADE, as well as of IJCAR, TABLEAUX, and FroCoS will all be published as open access publications with LIPIcs from 2027 onwards.
To attract as many participants as possible and to allow students to attend the conference, I think CADE should aim at affordable conference fees and continue the very good tradition of Woody Bledsoe travel grants for students.
My own research is concerned with different aspects of automated deduction. Therefore, I have been attending and publishing papers at CADE since 1994. In particular, I am working on techniques and tools to analyze properties like termination or complexity of programs automatically.
I was one of the PC chairs of IJCAR 2010, PC chair of RTA 2005, Steering Committee chair of RTA (2005-2007), Area Editor of ACM TOCL (since 2013), SC member of FSCD (since 2022), and I served many times on the PCs of CADE, IJCAR, RTA, LPAR, FSCD, and several other conferences in the field. I was CADE trustee from 2010-2011, 2014-2020, and 2022-2025, and CADE president since 2022.
I am honoured and excited to be nominated once again to serve on the CADE's Board of Trustees. I have contributed both research and tool papers to CADE and IJCAR, served as a PC member several times, and helped with the organisation of the first edition of CADE in South America. I also have experience as a PC member, chair, SC member and organiser for other conferences in our field.
My research is focused on both the theoretical foundations and practical aspects of implementing proof methods for non-classical logics and their combinations. CADE and IJCAR are (and should remain) welcoming venues for research encompassing a broad range of logics and techniques. I feel at home here and I am deeply committed to this community. As an enthusiastic implementer, I advocate for increasing the number of system and tool paper submissions, and for introducing demo sessions for tools at the conference. This is important not only in my field, but more generally, as it encourages and celebrates the hard work involved in producing these tools.
I strongly believe that a better geographical distribution of conference sites for CADE would be beneficial to our community. It would help to stimulate research, disseminate knowledge about automated reasoning, and also attract talented individuals from regions that are currently not well represented in our field. We should remain sensitive to the fact that funding in those areas is often limited, and both researchers and students may have difficulties with meeting travel expenses and registration fees. I therefore support continuing the Bledsoe Award to support students, while also exploring options for reduced registration fees for participants in less favoured regions.
Thank you for considering my nomination. I am looking forward to the opportunity to continue contributing to our community.
I am a strong proponent of Open Access publications to give all researchers access to CADE findings. That is why my PC-co-chair Geoff Sutcliffe and conference co-chair Marijn Heule took the initiative to make CADE-28 Open Access. Listening to extended community input, CADE now fortunately has a longer term Open Access plan beyond individual conferences, which, of course, should be monitored carefully to keep it successful.
CADE should continue its traditional strength of being particularly warm and welcoming to young researchers, which is also a role that the automated reasoning school can help facilitate. This summer school is a great opportunity to enable PhD students to pick up interesting background and grow into an international young scientists community.
The third challenge is how to help spread the voice of automated deduction in the broader logic community and the scientific community beyond. I believe this is is important, because automated deduction has a lot to offer in the significant topics of logic.
My background: I am the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology (KIT) and founded the Logical Systems Lab at Carnegie Mellon University. My research characterizes the logical foundations of cyber-physical systems and answers the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. I pursue this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees, such as in our KeYmaera theorem provers.
I have contributed as an author to CADE/IJCAR (where the largest percentage of my papers are published), shared my views on logic and proofs in an invited talk at IJCAR 2016, served on several CADE/IJCAR PCs, and have been co-chair of CADE-28 in 2021. I serve on the editorial board of the Journal of Automated Reasoning, Acta Informatica, and the ACM Formal Aspects of Computing.
My research covers various aspects of automated reasoning, including theory and applications. I have been attending CADE and IJCAR regularly, and I served on several of their PCs. I was program co-chair of CADE-23 (with Nikolaj Bjørner), program co-chair of IJCAR 2020 (with Nicolas Peltier), and conference chair of FroCoS 2011. I was honored to serve as a CADE trustee ex-officio (as CADE-23 program co-chair) and from 2011 to 2014.
CADE and IJCAR have the crucial role of stimulating important research in the area of automated reasoning; they are the major forum for discussing all aspects of automated theorem proving, including theory, implementations and applications. To ensure CADE's leading position in the field it is important to make clear that every area of automated reasoning is welcome at CADE. As a CADE trustee, I would work towards ensuring that the scope of CADE is kept as broad as possible.
I support encouraging tool submissions and submissions that demonstrate the impact of new or existing methods and tools on solving relevant problems. In this context, I think that artifact evaluation and making the tools available to the community is very important.
I believe that the current cycle of conferences (CADE alternating with IJCAR, and IJCAR as a part of FLoC every four years) is the right way to continue, since this guarantees the visibility of CADE while allowing close contact, convergence and interaction with related conferences within IJCAR, as well as interaction with the conferences in FLoC. To enhance the awareness of the importance of the research on automated reasoning, it is important to also strengthen the connection to top conferences in related areas outside FLoC (ETAPS conferences, IJCAI, ISSAC, POPL).
To attract participants, I think CADE should aim at having affordable conference fees. Although physical presence at a conference is desirable and very important, I believe that the possibility of registration at a lower fee for online participation, or the possibility of following online at least part of the talks should be seriously considered.
The future of the automated reasoning community relies on students and young researchers. Therefore we will have to continue finding ways to attract the best students and provide a stimulating atmosphere for them at CADE. Lower registration fees for students and Woody Bledsoe travel awards are important, since they make participation of young researchers easier. Organizing summer schools co-located with CADE would be a further possibility of attracting students at an even earlier phase, in which they start looking for research topics. In addition, mentoring workshops, or application-oriented events co-located with CADE could increase the impact of the conference on researchers at the beginning of their careers.
It has been an honor to serve in the CADE board of trustees from 2022 to now. During that time, I have been an active supporter of the move to LIPIcs that will finally occur at CADE 2027. I have also been involved in the organisation of several CADE and IJCAR in succession, as PC member and as workshop or publicity chair and workshop organizer. Thanks to IJCAR 2024 taking place in Nancy, preceded by the SAT/SMT/AR summer school that I co-chaired, I also got to appreciate the amount of planning and efforts required to organize the events that make our community alive.
These last few years my research interests have mostly been on the formalization of theoretical frameworks related to AR in Isabelle/HOL. This has brought me closer to the world of interactive theorem proving, that is ever present at CADE. I am also working on various other fun projects including higher-order SMT instantiation, abduction, that I keep returning to under different forms since my PhD days, and more exotic and/or applied topics such as applying theorem provers to quantum string diagram transformations.
In the past and in the future, one of the points I have paid and will continue to pay attention to is the communication and interactions between the different components of our community. As the (former) AAR newsletter editor, I was often contacting organizers of conferences and workshops to ask for CfPs before newsletter deadlines. Now, as part of the steering committee of the SAT/SMT/AR summer school, I am committed to making this event happen each year in the best possible conditions that is, in my opinion, coordinated with one of its related conferences, to contribute to bringing the state of the art of automated reasoning to new generations of researchers.
For the same reason, I am very favorable to the alternance between CADE and IJCAR with FLoC occurring every four years, and if there is a possibility of co-location on CADE years, I plan to favor that option other things being equal.
I really enjoy the balance between theory and practice at CADE, as well as the friendly and open atmosphere of our community. As a CADE trustee, I will strive to preserve these strengths of ours.
I feel honored to be nominated for the CADE Board of Trustees. Working mainly on saturation-based proof calculi and systems, I consider CADE my home conference. I had my first CADE paper in 1996, visited almost every CADE since 1990, participated in 10 of the last 13 CADE and IJCAR program committees, and co-chaired CADE-30.
I am generally happy with the development of CADE in the last decades. The regular alternation between CADE and IJCAR, the co-locations with other conferences, and the large range of workshops are important to foster cooperations with researchers from neighboring communities. Measures to support and promote young scientists help to keep the field of automated deduction alive and should be continued. To remain the leading conference in our field, the spectrum of possible topics for CADE must stay broad and theoretical papers, practical papers, and application papers must be equally welcome. In order to attract scientists from outside Europe, it is also important that CADE takes place on other continents on a regular basis.
This joint event brings together three major theorem-proving conferences: the 15th International Symposium on Frontiers of Combining Systems (FroCoS 2025), the 16th International Conference on Interactive Theorem Proving (ITP 2025), and the 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2025). The conferences will be co-located in Reykjavik, along with two ITP satellite workshops on Rocq and Lean.
Invited Speakers
Registrations are available here.
More information is available on the conference's web page.
FMCAD 2025 is the twenty-fifth in a series of conferences on the theory and applications of formal methods in hardware and system verification. It provides a leading forum for researchers in academia and industry to present and discuss methods, technologies, theoretical results, and tools for reasoning formally about computing systems. Topics include verification, specification, synthesis, and testing in computer-aided system design.
The conference will also feature the FMCAD Student Forum, the Hardware Model Checking Competition (HWMCC 2025), and VSTTE 2025.
ScheduleRegistrations are available here.
More information is available on the conference's web page.
The International Symposium on Distributed Computing (DISC) is an international forum on the theory, design, analysis, implementation and application of distributed systems and networks.
The conference program includes keynote talks, 14 technical paper sessions, and five affiliated workshops:
More information, including local details, accommodation, and the detailed program, is available on the conference web page.
SEFM 2025 will take place in the historic city of Toledo, Spain, Toledo is a historic city located in central Spain, known for its rich cultural heritage and stunning architecture. The conference will feature an exciting scientific program, distinguished keynotes, and several co-located workshops.
Keynote Speakers
Workshops
Registration is now open here, with early registration available until September 30, 2025. More details are available on the conference's web page.
Knowledge Representation and Reasoning (KR) is a well-established and vibrant field of research within Artificial Intelligence. KR builds on the fundamental thesis that knowledge can often be represented in an explicit declarative form, suitable for processing by dedicated symbolic reasoning engines. This enables the exploitation of knowledge that would otherwise be implicit through semantically grounded inference mechanisms. KR has contributed to the theory and practice of various areas of AI, including agents, automated planning, robotics and natural language processing, and to fields beyond AI, including data management, semantic web, verification, software engineering, computational biology, and cybersecurity.
The KR conference series is the leading forum for timely, in-depth presentation of progress in the theory and practice of the representation and computational management of knowledge.
KR 2025 will include three special thematic tracks (KR&R in Planning & Scheduling, KR and Constraints, KR in the Wild), a Video Track, a Recently Published Research Track, tutorials, workshops, and a Doctoral Consortium.
Registrations are available here.
More information is available on the conference's web page.
The forty-first Agda Implementors’ Meeting (AIM XLI) will take place in Angers, France, hosted at La Bulle en Bois, a collaborative Third Place combining coworking, local food, and a fablab.
The meeting will feature:
The venue offers:
Registration is free but mandatory. The soft registration deadline is October 24, 2025. Due to limited capacity (30 participants), registration may close earlier, so please register soon.
More information is available on the meeting's web page.
STACS 2026 will consist of two tracks, A and B. Track A focuses on algorithms, data structures, and complexity, while track B focuses on automata, logic, semantics, and theory of programming.
Authors are invited to submit papers presenting original and unpublished research on theoretical aspects of computer science. Topics covered by the tracks include, but are not limited to, the following:
Important Dates (AoE)
More information is available on the conference's web page.
SAC has gathered scientists from different areas of computing over the last thirty years. The forum gives participants an opportunity to interact with different communities sharing an interest in applied computing.
Track on Knowledge Representation and Reasoning (KRR)
The KRR track covers an important field of research in Artificial Intelligence. Knowledge Representation and Reasoning is a trending topic (for instance, its Argumentation-theory subfield). A similar dedicated conference is the International Conference on Principles of Knowledge Representation and Reasoning, but all the major AI conferences (AAAI, IJCAI, AAMAS, ECAI) have KRR among their topics of interest. This track will be a venue for researchers and practitioners working on the fundaments and applications of reasoning, and on the cross-fertilization among different approaches (e.g., Argumentation and Belief Revision).
Knowledge Representation and Reasoning (KRR) focuses on designing computer representations that capture information about the world to solve complex problems. Its goal is to build intelligent behavior from the top down, focusing on what an agent needs to know, how this knowledge can be represented symbolically, and how automated reasoning procedures can make it available. In KRR, knowledge is represented in a declarative form, suitable for reasoning engines.
Topics of interest include (but are not limited to):
Track on Software Verification and Testing (SVT)
The Software Verification and Testing track aims to contribute to the challenge of improving the usability of formal methods in software engineering. The track covers areas such as formal methods for verification and testing, based on theorem proving, model checking, static analysis, and run-time verification. We invite authors to submit new results in formal verification and testing, as well as development of technologies to improve the usability of formal methods in software engineering. We also welcome detailed descriptions of applications of mechanical verification to large scale software.
Topics of interest include (but are not limited to):
Student Research Competition (SRC)
Graduate students are also invited to submit abstracts of original, unpublished, and in-progress work related to this track as part of the SRC.
Important Dates
More information is available on the conference's web page.
The iFM PhD symposium provides PhD students with an opportunity to present and discuss their research in the fields of theory, implementation, integration, or application of formal methods. It is open to PhD students and young researchers up to two years after completion of their PhD.
The symposium offers an excellent opportunity to introduce your work to fellow researchers in an international setting, receive feedback from senior researchers in the field, and exchange knowledge and experiences with other PhD students working on related topics.
Talk proposals should be 2–3 pages in Springer LNCS format and should outline the problem being addressed, its relevance, the solution you are working on, your research approach, and your expected contribution. They should include a brief literature survey, indicate progress to date and current stage of research, and be written by the applicant as sole author (but may cite joint work).
Important Dates (AoE)
More information is available on the conference's web page.
The International Symposium on Artificial Intelligence and Mathematics (ISAIM) is a biennial meeting that fosters interactions between mathematics, theoretical computer science, and artificial intelligence. Submissions of recent results are invited, with a particular emphasis on the foundations of AI and mathematical methods used in AI. Papers describing applications are also encouraged, provided the focus is on principled lessons learned. Traditionally, ISAIM attracts participants from diverse disciplines, providing a unique forum for scientific exchange. The three-day Symposium includes invited speakers, presentations of technical papers, and special topic sessions.
Special SessionsA confirmed special topic session on Cooperation, Competition, and Complexity in AI Planning and Learning will be organized by Alan Kuhnle and Guni Sharon (Texas A&M University). Proposals for additional Special Sessions are welcome. Please send a 1-2 page description and expected participants to Martin Golumbic by October 31, 2025.
Topics of interest include, but are not limited to:
More information is available on the symposium's web page.
ETAPS 2026 is the twenty-ninth edition of the primary forum for academic and industrial researchers working on topics relating to software science. ETAPS consists of four main conferences, accompanied by satellite workshops and other events taking place during the weekend before the main conferences.
Main Conferences (April 13-16, 2026)
More information is available on the conference's web page.
The FormaliSE conference series promotes work at the intersection of the formal methods and software engineering communities, providing a venue to exchange ideas, experiences, techniques, and results. The three-day Symposium includes invited speakers, presentations of technical papers, and special topic sessions.
Topics of interest include, but are not limited to:
FormaliSE 2026 will also feature an Artifact Evaluation track, encouraging authors to submit supporting material such as software, data sets, or machine-checkable proofs to foster reproducibility and reuse. Accepted papers with successfully evaluated artifacts will receive artifact badges in recognition of their quality.
Important Dates (AoE)More information is available on the conference's web page.
TAP 2026 is a new special track at the 27th International Symposium on Formal Methods, providing a dedicated forum for researchers, practitioners, and tool developers to present advances in combining software testing and formal verification.
Topics of interest include, but are not limited to:
Important Dates (AoE)
More information is available on the track's web page.
FLOPS aims to bring together practitioners, researchers, and implementers of declarative programming, to discuss theoretical advances, their implementations in language systems and tools, and applications in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming.
Topics of interest include, but are not limited to:
FLOPS promotes cross-fertilization among different styles of declarative programming. Submissions of system descriptions and declarative pearls are especially encouraged.
Important Dates (AoE)More information is available on the conference's web page.
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires advanced technologies to address their specification, design, verification, validation, and certification. The NASA Formal Methods Symposium is a forum to foster collaboration between theoreticians and practitioners from NASA, other government agencies, academia, and industry, with the goal of identifying challenges and providing solutions towards achieving assurance for such critical systems. The focus of this symposium is on formal techniques for software and system assurance for applications in space, aviation, robotics, and other NASA-relevant critical systems.
The suggested, but not exclusive, list of topics for submission is:
Important Dates (AoE)
More information is available on the conference's web page.
Advances in Modal Logic is an initiative aimed at presenting the state of the art in modal logic and its various applications. It consists of a conference series together with volumes based on the conferences. AiML 2026 is organized by the Institute of Logic, Language and Computation (ILLC) of the University of Amsterdam. Information about the AiML series can be found at aiml.net.
Important Dates (tentative)
More information is available on the conference's web page.
The workshop aims to provide a forum for all auto-active program verifiers and their related techniques. There is an established group of verification-aware programming languages that have native support for specifications and proofs, and are equipped with an auto-active static program verifier. Examples include Dafny, SPARK, F*, Why3, Viper, and Whiley.
Topics of interest include, but are not limited to:
Important Dates
More information is available on the workshop's web page.
This workshop celebrates three decades since the publication of the first papers on UPPAAL and the release of the tool itself. Researchers, practitioners, and educators are invited to submit contributions to this commemorative event. Authors are invited to submit original research papers, case studies, and educational experiences.
Topics of interest include, but are not limited to:
Important Dates
More information is available in the workshop's web page.
The RocqPL workshop series (formerly CoqPL) provides an opportunity for programming languages researchers and practitioners with an interest in Rocq to meet and interact with one another and with the Rocq development team. The workshop features discussions of upcoming features, talks and demonstrations of current projects, feedback sessions for future changes to Rocq, and community-building activities.
Topics of interest include (but are not limited to):
The workshop format will be community-driven. Abstracts for talks and proposals for demonstrations are solicited, and the final program will include experiment reports, panel discussions, and invited talks. To foster open discussion of cutting-edge research, no papers will be published. However, presentations may be recorded and made publicly available.
Important Dates
More information is available on the workshop’s web page.
WoLLIC is an annual international forum on interdisciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers.
Topics of interest include (but are not limited to):
Important Dates
More information is available on the workshop’s web page.
Under the auspices of the Association for Logic, Language, and Information (FoLLI), the European Summer School in Logic, Language, and Information (ESSLLI) runs every year. Except for 2021, when the school was virtual, it runs in a different European country each year. It takes place over two weeks in the summer, hosts approximately 50 different courses at levels that run from foundational to introductory to advanced, and attracts around 400 participants from all over the world. In 2026, ESSLLI returns to Prague after exactly 30 years.
Since 1989, ESSLLI has been providing outstanding interdisciplinary educational opportunities in the fields of Computer Science, Cognitive Science, Linguistics, Logic, Philosophy, and beyond. It comes from a community which recognizes that advances in our common areas require the contributions of multiple interrelated disciplines.
The main focus of ESSLLI is the interface between linguistics, logic and computation, with special emphasis on human linguistic and cognitive ability. Courses, both introductory and advanced, cover a wide variety of topics within the combined areas of interest: Logic and Computation, Computation and Language, and Language and Logic. Workshops are also organized, providing opportunities for in-depth discussion of issues at the forefront of research, as well as a series of invited evening lectures.
Topics and Format
Proposals for courses and workshops at ESSLLI 2026 are invited in all areas of Logic, Linguistics and Computer Science. Cross-disciplinary and innovative topics are particularly encouraged.
Each course and workshop will consist of five 90 minute sessions, offered daily (Monday-Friday) in a single week. Proposals for two-week courses should be structured and submitted as two independent one-week courses, e.g. as an introductory course followed by an advanced one. In such cases, the ESSLLI Program Committee reserves the right to accept just one of the two proposals.
Categories
Proposal Guidelines
Course and Workshop proposals can be submitted by no more than two lecturers/organizers and can be presented by no more than these two lecturers/organizers. Two is actually the preferred number of lecturers/organizers, to secure the course/workshop against unexpected unavailability. All instructors and organizers must possess a PhD or equivalent degree by the submission deadline.
Course proposals should mention explicitly the intended course category. Proposals for introductory courses should indicate the intended level, for example as it relates to standard textbooks and monographs in the area. Proposals for advanced courses should specify the prerequisites in detail.
Important Dates (AoE)
More information is available on the proposal's webpage
The EACSL will support one Logic and Computation course or workshop addressing topics of interest to Computer Science Logic (CSL) conferences. The selected course or workshop will be designated an EACSL course/workshop in the programme. If you wish to be considered for this, please indicate it in your proposal.
POPL provides a forum for the discussion of fundamental principles and important innovations in the design, definition, analysis, transformation, implementation, and verification of programming languages, programming systems, and programming abstractions.
Tutorials for POPL 2026 are solicited on any topic relevant to the POPL community. We particularly encourage submissions of introductory tutorials that make the research presented at POPL more accessible to the participants.
Tutorials will be held on Jan 11–13, 2026. The expected length of a tutorial is 3 hours, including questions and discussion (Q&A).
Important Dates
More information is available on the POPL 2026 Tutorials web page.
FM 2026 is the 27th international symposium on Formal Methods in a series organized by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The FM symposia have been successful in bringing together researchers and industrial users around a program of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral research.
We are inviting proposals for tutorials to complement the main FM 2026 symposium. The primary goal of these tutorials is to convey ideas with a focus on pedagogy over technical innovation. They offer a valuable platform for participants to discuss technical challenges, exchange research concepts, explore educational strategies, and demonstrate or investigate practical applications. Tutorials should be designed to be broadly accessible and pedagogically oriented, clarifying key concepts, building intuition, and ensuring ease of understanding. They aim to attract new researchers, serve as bridges to practitioners, and disseminate useful ideas widely. These may be driven by fundamental academic interests, or by needs from specific application domains.
We encourage a diversity of topics relating to different ways of developing and using formal methods as well as all theoretical aspects of software engineering, including complex applications. Although tutorials focused on tools are a traditional choice, tutorials covering techniques are also welcome. Authors interested in proposing different types of tutorials are encouraged to contact the chairs for guidance. Overall, we welcome a broad range of tutorial topics, as long as they are relevant to the interests of the formal methods community. Moreover, we also invite topics at the intersection of machine learning and formal methods due to the growing interest in AI and machine learning-based software development.
Accepted tutorial papers will be published in the conference proceeding volume. Authors of these papers will be allocated a presentation slot during the tutorial sessions prior to the main conference. When submitting tutorial papers, authors should indicate their preferred presentation length, which can be either half a day or a full day.
Important Dates
More information is available on the FM 2026 Tutorials web page.
This special issue of the Annals of Mathematics and Artificial Intelligence (AMAI) is devoted to formal computational aspects of geometry. Geometry is a privileged field of investigation for various domains of computer science, from image processing to geometric modeling, artificial intelligence, education, automated proof in geometry, and semantic indexation of multimedia databases.
This special issue of AMAI is devoted to formal computational aspects of geometry. Computer supported geometry can be investigated in several different ways. At the beginning of the 1960s, the seminal work of Gelernter in the domain of automated proof was about synthetic geometry as taught in school. Then, in the late 1970s, a kind of revolution occurred with the work of Wu, consisting in translating geometry into algebra and in using pseudo-division to perform proofs of a high-level theorem in both Euclidean and hyperbolic geometries. Subsequently, much work has been done continuing that geometry/algebra relation by considering other aspects of geometry, like differential geometry, distance geometry, discovering geometric theorems in figures with dynamic geometry software or from graphical figures, etc.
Moreover, several researchers studied the foundations of geometry through various sets of axioms; this way, the classical axiomatic approaches of Hilbert and Tarski have been formalized, as well as computational origami or incidence geometry. Outside the domain of automated and formalized proof, computer supported geometry is also encountered almost everywhere in geometric modeling -- for instance with geometric constraint solving, declarative modeling, or topological modeling -- and also in computational geometry or combinatorial geometry.
For this special issue of AMAI, we are seeking original contributions on various aspects of computer supported geometry. Relevant topics include (but are not limited to):
Important Dates
Submissions should be made via the AMAI Editorial Manager website, selecting the issue Special Issue on ADG 2025: Formalisation of geometry, automated and interactive geometric reasoning.
Proof-theoretic semantics (P-tS) offers a foundational shift in logic, prioritizing inference over truth conditions and emphasizing the centrality of proof in the assignment of meaning. This inferential perspective is naturally aligned with computational approaches, yet the intersection of P-tS and computation remains comparatively underexplored.
This special issue of the Journal of Logic and Computation seeks to fill that gap by bringing together work at the interface of logic, computer science, and philosophy. We invite contributions that illuminate how computational interpretations of logic interact with proof-theoretic approaches, both conceptually and practically.
Topics of interest include, but are not limited to:
Submission deadline is March 31, 2026. For more information and submission instructions, see here.
The SCML publishing forum is dedicated to research combining Symbolic Computation (SC) and Machine Learning (ML) as two major approaches to artificial intelligence. We particularly welcome work on the application of ML to SC, the application of SC to ML, and hybrid combinations of the two. Submissions must explore the interaction between SC and ML rather than standalone work in either area.
Topics of interest include, but are not limited to:
SCML primarily solicits original research papers but also accepts surveys and position papers offering new perspectives on the interaction of SC and ML.
More information, including the Steering Committee and Editorial Board, is available on the SCML web page.
POPL 2026 will host an ACM Student Research Competition (SRC), where undergraduate and graduate students can present their original research before a panel of judges and conference attendees. The competition consists of three rounds:
POPL invites students to participate in the SRC to showcase their research and receive feedback from the programming languages research community. Submissions must be authored solely by the student and present original, unpublished work. In case of collaborative projects, the student’s individual contributions must be made clear.
Important Dates
More information is available on the competition's web page .
The 3rd World Logic Prizes Contest is a competition between winners of national logic prizes from many countries, taking place during the 8th UNILOG (World Congress and School on Universal Logic) in Cusco, Peru. Each winner will have their paper published in Logica Universalis and 30 minutes (including discussion) to present their winning work. A jury of around 10 prominent logicians from around the world will select the winner of the Universal Logic Prize.
This contest is part of the project "A prize of logic in every country", promoted by the Logica Universalis Association (LUA). Currently, 21 countries are registered, and it is still possible to register new countries here.
The 1st World Logic Prizes Contest took place at UNILOG 2018 in Vichy, France, and the 2nd at UNILOG 2022 in Crete. New prizes for the 3rd edition include:
More information is available on the contest's web page.
Supported by a generous ERC Advanced Grant and a Villum Investigator Grant from Villum Fonden, the Center for Basic Research in Program Verification (CPV) in the Logic and Semantics group at the Department of Computer Science, Aarhus University, has several postdoc and PhD openings.
The research topics at CPV include extensions of higher-order concurrent separation logics (such as the Iris logic), e.g., to reason about distributed systems; probabilistic program logics; logical relations for relational reasoning about safety, liveness, and security properties; formal modeling of low-level capability machines and secure compilation; program logics for relaxed memory models; category-theoretic models of type theory and their application to program semantics.
To apply for a postdoc position (deadline: September 22, 2025), see here.
To apply for a PhD position (next deadline: November 1, 2025), see here.
Please contact Lars Birkedal for more information.
The University of Birmingham is recruiting a number of academics at assistant/associate professor level in the School of Computer Science. More information about the positions can be found here.
The Theory of Computation group at Birmingham is world-renowned, and the university has been actively recruiting new researchers for some years. More information about the group is available here.
The position is open until September 30, 2025. Please encourage interested students, postdocs, and colleagues to apply. For informal enquiries, contact Dr Anupam Das or any other member of the group.
This PhD is part of the ANR project TAPAS (Time-Aware Proof ASsistants), which aims at a sound methodology for the design of trustworthy cyber-physical systems (CPS) from requirements to code deployment, supported by an open-source modeling, validation and verification framework. The objective of this PhD is to provide approaches to verification benefiting from both model checking Parametric Timed Automata and the Event-B methodology.
A complete description can be found here.
Candidates should apply by sending an email to the PhD supervisors: Laure Petrucci and Frédéric Mallet including:
The PhD is expected to start on October 1, 2025, or later depending on the selected applicant’s availability.
The IMDEA Software Institute in Madrid invites applications for multiple positions at different career stages. Opportunities are available forfully funded PhD students as well as for tenure-track (Assistant Professor) faculty.
PhD PositionsIMDEA is seeking PhD candidates in the broad area of formal verification and cyber-physical systems design. The goal is to develop foundations and algorithms for the design of real-world cyber-physical systems with rigorous correctness guarantees.
Applicants must hold a Master’s degree in Computer Science and be motivated to work on problems at the intersection of theory and practice.
The PhD is expected to start on March 1, 2026, or earlier depending on the selected applicant’s availability. The application deadline is October 3, 2025 A complete description and application portal can be found here. For inquiries, please contact Kaushik Mallik.
Tenure-Track Faculty PositionsIMDEA is also inviting applications for tenure-track (Assistant Professor) faculty positions. The Institute is particularly interested in candidates in the areas of:
Exceptional candidates in other areas related to the Institute’s research scope will also be considered. Tenure clock adjustments and fast tracking can be discussed depending on career stage.
Applicants must hold a doctoral degree in Computer Science or a closely related field by the expected start date. Candidates should demonstrate an excellent research record and the ability to work independently as well as collaboratively.
Applications must be submitted through the IMDEA careers portal, selecting reference “2025-09-faculty-call”. The application deadline is November 14, 2025.
The Logic and Theory Group at the Institute of Computer Science, University of Bern, invites applications for a one-year postdoctoral position in the project Non-wellfounded and Cyclic Proof Theory. The starting date is negotiable, and an extension of a few months may be possible.
This SNSF-funded project investigates fixed points, recursive definitions, and proofs by induction, which are essential concepts in mathematics and computer science. A novel approach to formal proofs, non-wellfounded and cyclic proofs, has recently gained attention. These proofs provide a formal counterpart to proofs by infinite descent, with proof branches that are not well-founded but still satisfy global soundness conditions. The project aims at developing a deeper understanding of the structural properties of such proof systems.
Candidates should hold or expect a PhD and have a strong background in logic. The application deadline is October 17, 2025. Applications should be sent by e-mail to Prof. Thomas Studer.
Applications should include:
The University of Bern offers a stimulating research environment in an international team, with excellent research facilities. Bern is ideally located in the middle of Switzerland and Europe, providing rich cultural and outdoor opportunities.
The Computer Sciences Department at the University of Wisconsin–Madison invites applications for a Ph.D. position at the intersection of programming languages and quantum computing. Given the rapid experimental progress and growing public interest in the practical realization of quantum computers, this is a unique opportunity to join a research community working to bridge theory and practice.
The research group and the broader quantum computing group at UW–Madison share an interest in working with students to build the emerging software stack for quantum computation. Successful Ph.D. applicants should bring extensive experience in at least one of the following areas and be ready to pick up the others:
To learn more about the Ph.D. program and how to apply, please see the department website. Students interested in this topic should apply under the Programming Languages category. The application deadline is December 15, 2025.
We are hiring a postdoctoral researcher to work on the formal verification of security properties at the software/hardware interface (e.g., compilers, OS, and hardware components). The position is part of the PEPR SECUREVAL project, hosted in the Inria SUSHI team at CentraleSupélec Rennes (IRISA Lab), France.
Topics may include:
Requirements: Strong background in formal methods and proof assistants (Coq, Isabelle, etc.). Knowledge in security, compilers, OS, or hardware design is a plus.
The position is for two years and is expected to start in Fall 2025. More details are available here
Apply by sending your CV, PhD info, and recommendation letters to Pierre Wilke and Guillaume Hiet.
As part of the University of Oxford's expansion in Computer Science, the Department of Computer Science is delighted to announce 7 faculty positions for recruitment in the 2025–2026 academic year (to start on September 1, 2026). Outstanding candidates in all areas of Computer Science are invited to apply.
The University of Oxford uses the grade of Associate Professor for most of its academic appointments, and these posts can also come with the title of Full Professor. The positions are suitable for both early-career researchers and more established academics.
Positions available:
Thedeadline is strict: December 17, 2025, at 12 noon. For more information and to apply, please see the official job posting.
The Systems Software Research Group at Virginia Tech invites applications for a one-year postdoctoral position. The group has several ongoing projects at the intersection of system security, formal methods, type systems, theorem proving, and verified compilation.
High-level description of projects:
Preferred Qualifications:
The start date and duration are flexible. We welcome motivated applicants who are enthusiastic about building verified systems and formal reasoning. If you are interested, please reach out to Prof. Binoy Ravindran with a CV.
We are looking for a strong post-doc who wants to do research at the foundation of programming language theory, in program verification and separation logic, with a focus on Rust. Candidates should bring solid experience in formal methods and PL theory. Prior knowledge of separation logic, Rocq, or Rust is greatly appreciated.
Interested candidates should email Ralf Jung. Please explain why you are interested in a post-doc in this field and what your prior experience is. Also include a CV and possible contacts for recommendation letters.
The starting date is flexible. The position is fully funded for two years at the standard ETH post-doc salary level, and comes with teaching requirements (thesis supervision, TA'ing courses); an extension could be possible depending on the funding situation at that time. For more information about ETH Zürich, see here.
If you have any questions, please do not hesitate to get in touch!
The National Institute of Informatics (NII) and the Research Organization of Information and Systems (ROIS) are recruiting postdoctoral researchers to work on formal methods and programming languages for the formal verification of Trusted Execution Environment (TEE) architectures. This position is particularly suited for programming languages or program verification researchers seeking a new application domain at the intersection of systems programming, security, and hardware, with opportunities to develop new theory accordingly.
Relevant techniques (not limited to) include:
Experience in modeling or verifying low-level languages (C, Rust, assembly languages, Verilog), systems software, or hardware will also be highly valued.
Further details, scope, and application instructions can be found on the application webpage.
I had a paper in the Springer LNCS this spring which was carefully prepared with the macro package for Springer Computer Science proceedings. As most of you might know, an accepted paper is forwarded to Straive, an Indian company who does what they call proof editing and type setting on behalf of Springer. The result is sent to the corresponding author who is asked to approve the produced version or to send corrections otherwise. Straive put 27 bugs into the paper which made almost 1.3 bugs per page, viz. wrong use of capital letters, non-standard hyphenations and missing separation of lines. Some (but not all) headings and captions where provided with an additional period whereas a period at the end of a sentence had been removed. The paper had 2 tables with centered entries, some of them were left aligned, other right aligned and some remained centered (counting as 2 bugs) after Straive had put it hands on it. The layout was poor as the modified paper hat some pages with empty space. Finally, spurious spaces had been inserted at several places. I sent my corrections and asked for the corrected version which I never received, simply because nothing had been corrected and the paper with all the Straive bugs went to print.
At the same time, I had a paper in Springer's Journal of Automated Reasoning (JAR) which also went to Straive. After a while, I got the proof edited and type setted version with 122 bugs being introduced by Straive (it were more as I discovered later). There were also required corrections: I used Sec. as abbreviation for Section which Straive replaced with Sect. and the Acknowledgement had been relocated to a position conforming to the JAR standards—nothing else needed a change. But where did all the other changes came from? Why did the Straive people put their hands on the TEX-source?
However, whereas I had to grant the publication rights to Springer before I saw the spoiled version of the LNCS paper, I was asked to grant the publication rights (and—more important—to care for payment) later. Hence I refused to sign the forms until a bug free version of the paper intended for print were available. This provoked some discussion with Springer as such a procedure does not conform to Springer's publication workflow. But why bother? As I insisted in my position, a sequence of 6 iterations begun. Each time I got a new “corrected” version, I had to scan the whole paper to check whether the identified bugs had been removed and to mark the new bugs Straive had put into the “correction”. I send my corrections back after 4 working days at most, but the whole process lasted over 3 month. In total, I identified 255 bugs which Straive had put into the paper (making more than 5.3 per page), and 240 had been corrected (as I could live with the remaining 15 bugs and did not want to risk the insertion of new bugs if I insist in a further correction), to wit
\mathit{...} with
$...$ in particular so that e.g. \mathit{fail} now
was displayed as $fail$).
Maybe my recent experiences with Springer was extreme, but I hardly believe that I am the only victim of the Straive people and Springer's non-existent quality control. If others have made similar experiences, the community should think of whether it would be better if its flagship journal and the main conference proceedings would be published elsewhere. Also the requirement of having printed journals and conference proceedings belongs to the pre-internet era. It is enough to put an accepted paper for free download on the server of some internationally recognized institution like Dagstuhl and to rise a publication fee of e.g. 50–100 € /US $ for authors to cover the administration expenses of such an online journal.
We all have enough duties in our daily work and need no additional burden by correcting the bugs others put into our papers. Future authors and conference chairs would benefit from a change.