Nominations for three CADE trustee positions were being sought, in preparation for the elections to be held after CADE-29.
The following candidates were nominated and their statements, in alphabetical order, are below:
My research focuses on the automation of higher-order logic. I work mainly on the proof assistant Isabelle/HOL and the automatic theorem prover Zipperposition. My goal is to make proof assistants less laborious to use by improving their build-in automation and by integrating automatic provers.
I have a history of service in the community. I have chaired IJCAR, CPP (Certified Programs and Proofs), ITP (Interactive Theorem Proving), and TAP (Tests and Proofs). I have also served as a CADE trustee from 2016 to 2019 and, ex officio, in 2021 and 2022. I have attended most installments of CADE and IJCAR since 2009 and consider it my home conference.
As a CADE trustee, I would work towards ensuring that CADE and IJCAR remain open to a wide range of deduction techniques and feature a healthy mixture of theory and practice. I believe this is best achieved by having at least two program chairs who have complementary backgrounds.
I would also argue in favor of systematizing the CADE practices. Program chairs should have clear guidelines and templates they can work with. Important matters such as the use (or not) of rebuttals should be settled by the board of trustee, instead of being left to each year's chairs to decide. A permanent repository of knowledge for use by program chairs should be set up, containing instructions about processes, template emails, etc.
Finally, we must increase the conference's impact and prestige. According to the CORE index (which has an impact on many researchers' careers), CADE and IJCAR are ranked A ("excellent conference"). There are specific measures we could take to obtain the top grade, A* ("flagship conference"). I would be in favor of doing what it takes to achieve this.
I am honoured by the nomination to serve on the CADE board of trustees. CADE and IJCAR are among the main conferences that I regularly attend. I have published at both conferences, been on the PC of CADE-29 in 2023, and served on the expert committees for the Bill McCune PhD award since its inception in 2020.
My own research is firmly rooted in automated reasoning and deduction, with push-button termination analysis, inference of complexity bounds and checking program equivalence in various computation formalisms as my main foci. Thus, my research connects the use of methods and tools in automated deduction (e.g., SAT and SMT solvers) with applications in program analysis. I am one of the main developers of the program verification tool AProVE.
I am currently serving as Publicity Chair in the Steering Committee of the neighbouring International Conference on Formal Structures for Computation and Deduction (FSCD). I think that the co-location of CADE and FSCD in Rome in 2023 with 24 joint registrations has been a big success: it has allowed for cross-fertilisation between our closely related communities and for reducing the need for frequent long-distance travel with its downsides on individual level in the short term and on planetary level in the medium term. Therefore, I would advocate for further co-location of CADE with related conferences such as FSCD or CAV in the coming years.
In a similar vein, I strongly believe that the option of hybrid participation and also presentation as implemented at CADE/FSCD in Rome should be upheld. This lowers the entry barrier for participants and authors who cannot spend financial and time resources on a week far away from home obligations. Reasons may include being a parent or carer, living in the developing world, being a taught student considering going into research, or simply being interested only in specific presentations.
There have been concerns that the online option of a hybrid event might dissuade many professional researchers from attending in person. However, the lively in-person interaction at CADE/FSCD in 2023 seems to indicate that these concerns are unfounded. At the same time, an observation at FSCD 2023 was that 10% of the presentations would not have been possible without the option for remote presentation. This shows that a hybrid event can increase the quality of the programme and broaden the reach of the conference without detrimental effects on the overall conference experience for in-person participants.
In regards to the publication model of CADE, I consider making the conference proceedings available as open-access publications, as in 2023, to be the right way forward. To keep the financial entry barrier for authors low and to ensure that the quality of submission remains the sole criterion for publication, I think that it is important that funding by CADE for authors to cover open-access fees should continue to be available as needed. Here a sensible balance needs to be struck between attendance fees paid by all participants and open-access publication fees paid by the authors.
Finally, I am in favour of initiatives that support young researchers who are trying to establish themselves in the CADE community and in academia. This includes the Woody Bledsoe Student Travel Award for making attendance of CADE possible for students and the Bill McCune PhD award for distinguishing the contributions of a recent PhD thesis in automated reasoning, thus helping to kickstart the academic career of a promising researcher in the CADE community towards a permanent position.
As a previous member of the CADE Board of Trustees I appreciate its importance in securing good conference locations, appointing PC Chairs, constituting award committees, ensuring the success of various other activities in our area and providing leadership and representation for the area of automated reasoning. I have experience in chairing the CADE, FroCoS and TABLEAUX conferences and am PC-CoChair of IJCAR 2024. I am also founding organiser of the PAAR workshop series and am Editorial Board member/Associate Editor of the Journal of Automated Reasoning, the Artificial Intelligence Journal and the Journal of Artificial Intelligence Research.
This varied experience gives me a broad perspective on issues and concerns in our community and will allow me to continue be a strong advocate for the interests of automated deduction, its future and integrity in all our processes. I would be honoured to serve on the CADE Board of Trustees for another term.
My background: My main research involves the development and theoretical analysis of reasoning methodologies and automated reasoning tools as well as applying these in areas such as artificial intelligence, knowledge representation, agent-based systems and mathematics. At present a very strong focus of my work is the development of tools 1) for forgetting, content extraction, abductive learning and query answering in the context of ontology-based languages, and 2) for tableau synthesis, uniform interpolation and automated correspondence theory in the context of non-classical logics.
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, and participated in 8 of the last 11 CADE and IJCAR program committees.
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
There seems to be a general consensus that moving to open access CADE proceedings was the right decision, both because it improves the accessibility of our research and because some funding agencies insist on it. When we look at the details, however, we encounter conflicting interests. While for some authors the visibility of the publication and the publisher's prestige are paramount, others place a greater emphasis on low publication fees and would prefer do not feel screwed by the publisher's copy editors. We must find a reasonable compromise in this matter.