CADE and FSCD 2027 will take place in Nijmegen, the Netherlands. Proposals are invited for workshops of interest to either community.
Proposals should include:
Proposals for other colocated events, such as poster sessions or competitions, should be submitted in the same way.
The available dates are in principle:
However, on request, we may also schedule workshops / poster sessions / competitions during their affiliated conference (22-25 August for CADE and 23-26 August for FSCD) instead of before/after.
Important Dates (AoE)
Proposals must be limited to three pages and submitted to Cynthia Kop. 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 IJCAR 2026.
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.
I'm very happy to be nominated to the CADE Board of Trustees. I have been attending CADE and IJCAR almost every year since 2014, publishing regularly and serving on the PC. My research is focused on SMT solving and its applications, so CADE has always been a natural home for me. I have also organized the PxTP, SC^2, and SMT workshops co-located with CADE/IJCAR, as well as served on the Bill McCune PhD Award committee.
My platform is that CADE needs to grow, and that we should face why it is not when automated reasoning is becoming more popular and impactful. One issue is the standing in rankings such as CORE, by which many of us are evaluated. Moreover there is competition from larger and higher-ranked conferences, with papers that would be a better fit at CADE going to these venues instead. I will strongly advocate for taking steps towards increasing the prestige and size of CADE, so we can try to reverse this trend.
As a trustee I will also prioritize easier access for students and researchers with less funding. The Woody Bledsoe award and more reasonably priced open access are examples of initiatives I find excellent for our community.
I joined the CADE board of trustees in 2023, and I am honoured to be nominated for a second term. CADE and IJCAR are among the main conferences that I regularly attend. I have published at both conferences, been on the PCs of CADE and IJCAR several times in the last years, and served on the expert committees for the Bill McCune PhD award every year since its inception in 2020.
My research is firmly rooted in automated reasoning and deduction. My main areas of interest are push-button termination analysis, inference of complexity bounds and checking program equivalence in various computation formalisms. 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, and I have contributed to the higher-order program verification tool Cora.
Currently, I am serving as Publicity Chair in the Steering Committee of the 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. This form of co-location reduces the need for frequent long-distance travel with its downsides on individual level in the short term (time and money must be spent) and on planetary level in the medium term (air travel causes significant greenhouse gas emissions). Therefore, I am very pleased that FSCD and CADE are co-locating in Nijmegen in 2027, and I would advocate for further co-location of CADE/IJCAR with related conferences such as FSCD, SAT, ITP, or CAV in the coming years.
While CADE should continue to be an in-person conference, I would like to encourage the additional option of online participation and, where needed, also presentation. 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 care responsibilities, limited access to funding or safe travel options, being a taught student considering going into research, or simply being interested only in specific presentations. To strike a balance between widening access and keeping local organisation manageable, an upstream channel from the remote audience to the conference room would not be necessary since remote participants can contact authors for follow-up questions by e-mail; offering a one-way live video stream can go a long way. FSCD has good experiences with this model, with 95 registrations for the (free) video stream and up to 15 concurrent online participants at FSCD 2026.
There have been concerns that an in-person conference with an online option might dissuade many professional researchers from attending in person. However, the lively in-person interaction at CADE/FSCD 2023 (and at later FSCDs) suggests 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 this 'lightweight hybrid' option 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.
Regarding the landscape of conferences in automated reasoning, I think that the current alternation of CADE + FroCoS + TABLEAUX as separate events in odd years with IJCAR in even years is a sensible model. It allows for a breadth of different venues in automated reasoning while simultaneously providing a regular point for the whole community to meet. As topics from automated reasoning are also represented at larger AI conferences (e.g., IJCAI), the visibility of our community in related fields is ensured without changing the nature of the automated reasoning/deduction conference landscape.
I believe that CADE should be open to new developments in applications of automated deduction and combinations of techniques from other fields, such as machine learning. One example is the increased integration of theorem provers (e.g., Lean) into mathematicians' research. Another example is the interplay between deduction-based techniques to verify claims by machine-learning-based systems or, conversely, the use of machine-learning-based systems as heuristics for deduction-based systems to explore their search space. The openness of CADE to these developments could be reflected, e.g., by inviting PC members whose research connects automated deduction to other areas.
Finally, I am in favour of continuing the CADE initiatives that support young researchers who are trying to establish themselves in the CADE community and in academia. Current initiatives include 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. These awards help to kickstart the academic career of a promising researcher in the CADE community towards a permanent position, and I consider them an excellent way of supporting the next generation of researchers in our field.
I am very pleased to be nominated as a candidate trustee. CADE is where my friends, colleagues, and research interests are. If elected, I will help CADE succeed in any way I can.
I have a 'varied' research record, nonetheless centred around automated deduction. In particular I am involved with the TPTP World and the classical first-order theorem prover Vampire. I am also interested in applications of automated reasoning and in translations between systems.
I would change little about CADE's positioning or size. However, large language models are a new kind of automated deduction - weird, expensive, unreliable, but new - we should be rightly sceptical but curious about this new development while preserving a focus on traditional automated deduction and symbolic AI.
My main focus as a trustee would be reducing barriers to participation, for which I believe cost is a significant factor. CADE is by no means the most expensive conference, but for many potential participants it is still a significant hurdle. Student awards like Woody Bledsoe go some way to help, but we can always do more. I would take a marginal-gains approach to cutting costs wherever possible.
My research covers various aspects of automated reasoning. I have been attending and publishing papers at CADE and IJCAR regularly since 1999, and I served many times as a PC member of CADE and IJCAR. I was one of the PC chairs of CADE-23 and of IJCAR 2020 and conference chair of FroCoS 2011. I was CADE trustee from 2010 to 2011 (ex oficio), and from 2011 to 2014.
As a CADE trustee, I would work towards ensuring that CADE remains the main conference in the area of automated reasoning and that its scope remains as broad as possible. CADE should continue to cover all aspects of automated reasoning, including theory, implementations, tools and applications.
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 as a major forum for discussing all aspects of automated theorem proving, 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 have affordable conference fees. Although physical presence at a conference is very important, I believe that the possibility of online participation (with lower registration fees), or the possibility of following online at least part of the talks should be seriously considered.
As a CADE trustee, I would work towards increasing the attractivity of CADE for young researchers. For this, low registration fees for students and Woody Bledsoe travel awards are very important. Organizing summer schools, mentoring workshops, and application-oriented events co-located with CADE would further increase the impact of the conference on researchers at the beginning of their careers.
Most of you know me already, as either "the TPTP guy", or "the guy who runs CASC", or "the guy who emails out conference announcements". I have been attending CADE/IJCAR since about 1990, and have thus seen the growth, the things that don't work, and ideas that do work. I was a CADE trustee 2004‑2010 and 2011‑2017. I maintain the CADE and IJCAR web sites. CADE is doing well enough, and now it has an opportunity to develop further in the context of new AI tools and techniques. I support theory in the context of practice, and practice in the context of application. I will continue to promote that balance at CADE. I will represent your opinions as a trustee, balanced with my experience with CADE/IJCAR and knowledge of automated deduction.
The ICTAC conference series aims at bringing together researchers and practitioners from academia, industry, and government to present research and exchange ideas and experiences within theoretical aspects of computing through methods and tools for system development. ICTAC also aims to promote research cooperation between developing and industrial countries.
Key highlights:
The early registration deadline is September 25, 2026.
More information is available on the conference's web page.
The ACL2 Workshop series is the major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work on ACL2 and the other theorem provers in the Boyer-Moore family.
The workshop will take place in person at the SRI International headquarters. In addition to in-person participation, the workshop will support online participation for all talks and presentations. The workshop will be the 20th in the series of ACL2 workshops, which occur approximately every 18 months. It will feature technical papers as well as rump sessions that discuss ongoing research. The workshop invites users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend.
We invite submissions of papers on any topic related to ACL2 and its applications, and we strongly encourage submissions related to other theorem provers or formal methods that are of interest to the ACL2 community. Suggested topics include but are not limited to new results in the following areas:
The early registration deadline is September 30, 2026.
More information is available on the workshop's web page.
Machine Learning (ML) became the enabling technology of several applications. There is an enormous interest in adopting them to support critical tasks such as error/intrusion/anomaly detection, image classification or even object detection and trajectory planning to support autonomous driving. However, components that operate in critical systems must be assessed so that the encompassing system complies with adequate safety and security requirements before they are deployed and used in their operational environment without generating catastrophic hazards to the health of citizens, the environment, or the infrastructures. The absence of safety/security guarantees, or even a quantitative estimation of their robustness against specific events (e.g., unknown or zero-day attacks, adversarial attacks, out-of-distribution data) may be considered unacceptable by certification bodies, holding their deployment into real critical systems.
Unfortunately, the current maturity of research is still far from guaranteeing a safe, secure and robust operation of ML algorithms in many domains. Therefore, this track calls for contributions that aim at making a step towards a safe, secure and robust operation of ML components through (non-exhaustive list):
Important Dates (EST):
More information is available on the conference's web page.
The STACS conference Symposium on Theoretical Aspects of Computer Science takes place each year since 1984, alternately in Germany and France, and is dedicated to theoretical computer science in all its aspects.
STACS 2027 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.
Topics of interest include (but are not limited to):
Track A: Algorithm Design, Data Structures, and Complexity
Track B: Automata, Logic, Semantics and Theory of Programming.
Important Dates (AoE)
More information is available on the conference's web page.
ETAPS 2027 is the thirtieth edition of one of the primary fora for academic and industrial researchers working on topics relating to software science. ETAPS is a confederation of four annual conferences accompanied by satellite workshops taking place during the weekend before the main conferences (April 10–11, 2027).
A new development in 2027 is the introduction of iFS (International Conference on Foundations and Formal Methods for Software and Systems), formed through the merger of FASE and iFM.
Main Conferences (April 12–15, 2027)
Important Dates (AoE)
More information is available on the conference's web page.
FSEN is an international conference that aims to bring together researchers, engineers, developers, and practitioners from academia and industry to present and discuss their research work in the area of formal methods for software engineering. Additionally, this conference seeks to facilitate the transfer of experience, adaptation of methods, and where possible, foster collaboration among different groups. The topics of interest cover all aspects of formal methods, especially those related to advancing the application of formal methods in the software industry and promoting their integration with practical engineering techniques.
Topics of interest include, but are not restricted to, the following:
Important Dates (AoE)
More information is available on the conference's web page.
FormaliSE brings together the formal methods and software engineering communities to exchange ideas, experiences, techniques, and results, with the goal of fostering the development and application of formal methods that are both practically useful and capable of supporting high-quality software engineering.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the conference's web page.
AILA aims to advance the foundations, methods and applications of logic in artificial intelligence. It promotes the integration of logic with contemporary AI as a pathway towards more reliable, interpretable, accountable and trustworthy intelligent systems, particularly at a time when AI is increasingly expected to reason, explain, verify and act responsibly in complex real-world environments.
AILA provides an international forum for researchers and practitioners to exchange frontier ideas, present rigorous research, share practical insights, and build collaborations on the theory and practice of logic for artificial intelligence. The conference welcomes contributions on fundamental logical theories, formalisms and methods; the use of logic in AI, including logical approaches to machine learning, large language models, knowledge graphs, neuro-symbolic AI, automated reasoning, knowledge representation, verification, explanation, decision-making, safety, accountability and trust; and logic-based applications in areas such as decision support, fraud detection, cybernetics, precision medicine, trustworthy AI, and other intelligent systems.
Contributions should emphasise the role of logic, formal methods, or logical reasoning in AI. Papers whose primary focus is on AI techniques or applications without a substantial logic component are outside the scope of the conference. AILA welcomes original contributions on the theory, methods and applications of logic in artificial intelligence.
Topics of interest include, but are not limited to:
Important Dates (AoE)
More information is available on the conference's web page.
TFP is an international forum for researchers with interests in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results and other contributions.
Please be aware that TFP has several submission deadlines. The first is for authors who wish to have their full paper reviewed prior to the symposium. Papers that are accepted in this way must also be presented at the symposium. The second is for authors who wish to present their work or work-in-progress at the symposium first without submitting to the full review process for publication. These authors can then take into account feedback received at the symposium and submit a full paper for review by the third deadline.
Topics of interest include, but are not limited to:
Important Dates (AoE)
More information is available on the conference's web page.
The ThEdu'26 workshop took place on 29 July 2026 as a satellite event to FLoC in Lisbon, featuring ten presentations that captured the audience's interest and sparked lively discussions.
As in previous years, we would therefore like to encourage the speakers at ThEdu’26 to expand their extended abstracts into full papers – and we warmly invite anyone interested in the topic who was unable to attend ThEdu’26 to publish their full paper in the post-proceedings. All papers will be peer-reviewed in accordance with EPTCS standards
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering, and mathematics. This volume of EPTCS intends to bring together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. AI is raising new questions in the field of education, particularly in maths teaching and in software supporting it.
Topics of interest include:
Important Dates (AoE)
More information is available on the workshop's web page.
NWPT is a series of annual regional-scope workshops on programming theory, targeted especially at younger researchers. This is a nice opportunity to present recent results and/or work-in-progress, and to meet colleagues from the Nordic and Baltic countries. We encourage PhD students and postdocs in particular to contribute.
Topics of interest include (but are not limited to):
Important Dates (AoE)
More information is available on the workshop's web page.
Formal Aspects of Computing welcomes submissions that contribute to the fields of formal methods, symbolic AI, subsymbolic AI, and their synergies towards dependable, explainable, and thus trustworthy systems. A key benefit of formal methods and symbolic AI is in their formal rigor, providing guarantees but usually requiring concise formal modeling and computationally expensive reasoning. Differently, subsymbolic and data-driven AI provides outstanding performance in many applications, but might lead to unsound results. This special issue addresses how formal methods can contribute to and benefit from intersymbolic AI, combining symbolic and subsymbolic AI towards performant reasoning with formal guarantees.
The special issue welcomes submissions in the fields of formal methods and artificial intelligence. Relevant areas include but are not limited to the following topics:
Important Dates (AoE)
Early submissions will likely receive reviews and notifications ahead of the general timeline.
For questions and further information, please contact Clemens Dubslaff.
More information is available on the special issue web page.
The purpose of this Special Issue is to promote and disseminate recent advances in unification and closely related topics, focusing on both theoretical developments and practical aspects.
Unification is concerned with the problem of making two terms equal, finding solutions for equations or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc.
This special issue focuses on the topics of unification in a broad sense, which include, but are not limited to, the following:
This special issue is related to the research presented in the last two editions of the International Workshop on Unification — UNIF 2025 and 2026. Submissions of high quality works on unification that were not presented at these workshops are also welcome. Thus, participants of UNIF, as well as other authors, are invited to submit contributions.
Important Dates (AoE)
More information is available on the special issue web page.
Within the DIDI project, a joint project between Eurac Research, Bolzano, Italy and the University of Innsbruck, Austria, there is an opening for a three year PhD student position. The position will be hosted at the Theoretical Computer Science Group, University of Innsbruck, Austria.
We are looking for a strong candidate interested in one (ideally a combination) of the following areas (i) machine learning; (ii) natural language processing; (iii) programming languages and (iv) verification. Your responsibility within the DIDI project would be the development of novel techniques on (explainable and reliable) generative AI employable in natural language processing. These methods should be applicable to the analysis of the multilingual media landscape in South Tyrol, supporting research on the role of media within the German-, Italian-, and Ladin-speaking communities and their contribution to intercultural dialogue and exchange.
It is expected that you write a dissertation in this area, publish in international, relevant conferences; supervise students and participate in public events.
The application deadline is September 30, 2026. Applications, including a CV, a short letter of motivation, and three references, as well as informal inquiries, should be sent to Georg Moser.
More information is available on the position's web page.
A fully funded PhD position is available, jointly supervised by Kaushik Mallik and Alessio Mansutti, at the IMDEA Software Institute in Madrid, Spain. The PhD topic focuses on foundational research at the intersection of machine learning and formal verification. Machine learning has shown significant potential for a wide range of synthesis tasks, including controller and program synthesis. The goal of the PhD research is to develop a general learning-enabled synthesis framework that combines the flexibility of machine learning with the rigorous correctness guarantees of formal methods. The project will focus on Skolem function synthesis as a general formulation of synthesis problems, with applications across different domains, including controller synthesis, program synthesis, and solving partial differential equations.
Applicants need to have a recent master's degree in CS or mathematics and the willingness to work in problems in the intersection of theory and practice.
The ideal starting date is between January 1 and March 1, 2027. The application deadline is September 30, 2026. Interested candidates should apply via the job posting. For further questions, contact Kaushik Mallik or Alessio Mansutti.
SDU Centre for Software Technology in Vejle, part of the Software Engineering units at SDU situated at the Maersk Mc-Kinney Moller Institute, University of Southern Denmark (SDU), invite applications for one or more positions within software engineering and software technology. The positions are open from beginning of 2027, and the specific start date will be agreed with the successful candidates.
The focus of the SDU Centre for Software Technology is research and education in software engineering, interactive technology and artificial intelligence. We see these areas complementing each other to make way for the engineering of the next generation of reliable, intelligent and interactive software solutions. We are particularly interested in software operated in real life, systems that adapt at runtime, span embedded devices, edge infrastructure and the cloud, that people work with and trust, and that increasingly answer to regulation. This includes understanding how AI technologies and data-informed software development with a human-centred perspective can change the engineering of products and software infrastructures.
The positions are open in any of the software engineering and software technology research areas of interest to the centres, which include:
The application deadline is September 30, 2026, at 23:59 CET/CEST. For more information or to apply, see the job posting. If you are interested in learning more about the position, please contact Torben Worm, Mikkel Baun Kjærgaard, or Mahyar Tourchi Moghaddam.
Several PhD and postdoc positions relating to formal verification and quantum computing/quantum cryptography are available in Dominique Unruh's group, the Chair for Quantum Information Systems at RWTH Aachen, Germany. Open PhD projects include:
Other similar projects are possible too. Postdocs are also welcome to apply on these or similar topics, providing their own research proposal. Please apply before end of September 2026.
Applications for PhD and postdoc positions should be sent to unruh-application@qis.rwth-aachen.de. More information, including the full list of open positions and application instructions, is available on the group's web page.
The TCS-group of the Institute for Logic, Language and Computation (ILLC) at the University of Amsterdam is looking for an Assistant Professor to work on machine learning for formal reasoning and verification.
The position of Assistant Professor (Universitair Docent, UD) will be embedded within the Institute for Logic, Language and Computation (ILLC). The ILLC promotes curiosity-driven research and serves as a meeting point for computer scientists from traditional research fields ranging from AI, computer science, and mathematics to linguistics, cognitive science, and philosophy.
We are seeking candidates working at the intersection of artificial intelligence, machine learning, and formal reasoning. Relevant areas include, but are not limited to, automated reasoning, interactive theorem proving systems, formal verification, formalized mathematics, neuro-symbolic methods, and AI-assisted mathematical or logical reasoning.
We particularly welcome candidates whose work connects modern AI and machine learning with formal proof systems, interactive theorem provers, or proof assistants such as Lean, Rocq, or Isabelle. At the same time, we also encourage applications from researchers whose work engages more broadly with logic, reasoning, and theoretical computer science.
The application deadline is October 7, 2026. More information is available on the position's web page.
Are you interested in working in formal verification and programming language techniques applied to quantum systems, with the support of competent and friendly colleagues in an international environment? Are you looking for an employer that invests in a sustainable working environment and offers safe, favourable working conditions? We welcome you to apply for a PhD position at the Department of Information Technology, Uppsala University.
The project lies at the intersection of formal verification, programming languages, and quantum computing. As quantum hardware continues to scale, the software stacks used to control quantum devices are becoming increasingly sophisticated. Modern quantum programs often involve hybrid architectures in which classical control logic interacts closely with quantum circuits, for example in the implementation of quantum error correction and repeat-until-success circuits. Implementing these techniques often requires intermediate measurements of quantum states, with the measurement outcomes used to drive classical control logic. Scalable and automated verification of programs with these features is beyond the capabilities of the current state-of-the-art tools.
Candidates should have a background in mathematics, excellent problem-solving skills, high motivation, an interest in programming, and good communication skills in English. Experience or coursework in formal methods, programming language theory or semantics, logic, automata theory, automated theorem proving, or quantum computation is considered an asset. The position starts on January 15, 2027, or by agreement.
This project investigates scalable verification techniques for quantum programs, with a focus on developing mathematically grounded methods that can provide strong guarantees about program behavior while remaining practical for large systems.
Possible directions of the project include:
The project aims to contribute both theoretical insights and software artifacts, advancing the state of the art in quantum program verification.
The application deadline is November 15, 2026. For more information or to apply, see the job posting. For informal inquiries, contact Ramanathan Thinniyam Srinivasan.
As part of our expansion, the Department of Computer Science at the University of Oxford is seeking to appoint two full-time Associate Professors or Professors of Computer Science to start on 1 September 2027.
Each post is associated with a college, one with a Tutorial Fellowship at Wadham, the other with an Official Studentship at Christ Church (the Christ Church equivalent of a Tutorial Fellowship). Duties will include undertaking original research in Computer Science, securing funding to support the Department’s research activities, together with teaching and supervision responsibilities for the Department of Computer Science and the College, and Trustee duties (as a member of the Governing Body) at the College.
Applicants should hold a doctoral degree in Computer Science or a closely related discipline, have the ability to teach across a range of Computer Science subjects, and will also have a proven research track record of internationally high quality in Computer Science. Applicants should be able to demonstrate a high standard of research potential and achievement depending on experience, and the ability to enthuse and inspire students at both undergraduate and graduate level through tutorials, classes, lectures, and supervision.
The University of Oxford uses the grade of Associate Professor for most of its academic appointments. Appointments to Associate can include those at the start of their careers directly from PhD, as well as more established researchers.
The application deadline is December 16, 2026, at 12 noon UK time. No late applications will be considered. For more information or to apply, see the job offer, or contact the HR Team.
The Department of Computer Science at TU Braunschweig, Germany, is establishing a new research group on Formal Methods for Trustworthy Systems and AI, offering several PhD positions. Topics of interest include formal verification, symbolic methods, and automated reasoning, with applications in AI and explainability. The positions are full-time.
Candidates are required to have a very good Master's degree in computer science, mathematics, or a closely related field, a strong background in theoretical computer science, motivation to conduct theoretical research with applications in practice, and proficiency in English, with willingness to learn German. Good programming skills in Rust and knowledge of automated reasoning, model checking, and logics are considered a plus.
Interested candidates are requested to send a short letter of motivation and curriculum vitae, transcripts of records, and their Bachelor's and Master's theses (or a draft of the latter) to Clemens Dubslaff, head of the group.
The Huawei Programming Languages team at the Huawei Edinburgh Research Centre is looking to hire a Programming Languages Research Engineer to perform original research, research transfer, and engineering work on programming languages, and to support cooperation with the School of Informatics, University of Edinburgh.
Responsibilities include analyzing key technologies and requirements for both system-level and high-level languages, designing and developing new compiler frameworks for concurrency and control, and building tooling for agentic programming, verification, and validation. Unlike in previous years, when the team focused on programming languages and compilers, it is now also opening up to verification and validation researchers.
Candidates should have comprehensive experience, knowledge (i.e., of theory, applications, compilation, verification, and tooling) of modern programming languages covering the object-oriented and functional spectrum, a research track record in Programming Languages and Compilers and/or verification and validation, excellent programming, research, and analytical skills, familiarity with functional programming concepts and techniques, in particular as related to concurrency and control, and the ability to pick up and develop new technologies.
For queries, contact Dan Ghica, Director of the Programming Languages Laboratory, or apply directly at the job posting.
The Queen's Laboratory for Safety Critical Software Engineering (CritLab) is looking to hire a postdoctoral researcher for full-time work in the area of Formal Methods. In this project, the postdoc would work with an industrial partner on developing defense-related software technology for interoperability between heterogeneous systems. The length of the position is flexible.
CritLab is an inclusive environment with many opportunities for growth, located on the main campus of beautiful Queen's University in Kingston, Ontario, Canada. A successful applicant has a solid research background and interests outside work. Eastern Ontario is a wonderful place if you enjoy lakes and trees.
To apply, follow the instructions for applying for supervision on the CritLab web page and include a two-page research statement on how your work intersects with high-criticality systems. Experience in Formal Methods will be considered important for the position.
More information is available on CritLab's web page.
IRIF is opening a postdoctoral position on gradual and semantic typing for Elixir's module system, working directly with José Valim (creator of Elixir) and the Elixir core team. The goal is to extend the semantic-subtyping-based type system already shipping in the official Elixir compiler to cover its module system, treating modules and values within a single, unified type-theoretic framework.
Two intertwined challenges are on the table: bringing gradual typing to modules, and reconciling existential types with the semantic subtyping framework, with a direct path from theory to a compiler used by tens of thousands of developers at companies such as Apple, Discord, PepsiCo, BBC, Adobe, and Spotify.
The position is for 12 months (extendable), starting November 1, 2026 (negotiable, though only to a later date). A PhD in Computer Science is required, with a strong background in functional languages and type systems expected.
For the full description, scientific context, and how to apply, see the position's web page. For enquiries, contact Giuseppe Castagna.
The FOCS Lab at the National University of Singapore (NUS) is recruiting postdoctoral researchers and PhD students for a newly funded project on foundations for testing and verifying concurrency in Go. Go combines message passing through channels with shared memory, locks, and atomic operations. Reasoning about programs that mix these mechanisms is challenging: their behaviour depends on both the ordering of concurrent operations and the guarantees of the underlying memory model. The project aims to establish formal foundations for this reasoning and develop algorithms and tools for finding concurrency bugs in Go programs.
Potential research directions include:
Candidates interested in foundational theory, algorithm design, or the development and evaluation of research tools are welcome, with relevant backgrounds including programming language semantics, type systems, concurrency, program analysis, verification, logic, and automata theory. Postdoctoral candidates should have completed, or be nearing completion of, a PhD in a relevant area; prospective PhD students should have a strong background in computer science or mathematics and an interest in research. Successful candidates will join the FOCS Lab at NUS, with opportunities to collaborate with other faculty, including those in the Programming Languages and Software Engineering (PLSE) group, and for international research collaboration.
For an initial enquiry, contact Umang Mathur with a CV, a brief description of your research interests, your preferred start date, and an indication of whether you are interested in a postdoctoral or PhD position; informal enquiries are welcome. More information is available on the FOCS Lab's web page.
Loris D'Antoni (UC San Diego) shared a new funding opportunity for researchers working broadly on code translation (verification, testing, semantics, etc.). See the Verified Code Translation Research Awards for details.