Research Fellow in Data-Parallel Proof Checking for Monoidal Theories

Job Description

Research Fellow in Data-Parallel Proof Checking for Monoidal Theories: Grade: 7

Department: Computer Science: Location: UCL Campus, PPLV Group

Reports to

Fabio Zanasi

Context

UCL Computer Science is a global leader in research, teaching and innovation in experimental computer science. Home to some of the world’s most influential and creative researchers, the department is at the forefront of tackling society’s most complex challenges while educating the next generation of computer scientists.

We are the highest-ranked department in England and second in the UK for computer science research power in the most recent REF, reflecting the real-world impact and excellence of our work. Our teaching is equally distinguished, with a top 5 UK ranking in the QS World University Subject Rankings 2026.

We are equally proud of our work in EDI and outreach, promoting equity, diversity and inclusion across our community and aiming to inspire, empower and engage people from all backgrounds. As the first computer science department in the UK to receive an Athena Swan Gold Award, we are committed to creating a fair, inclusive and supportive environment for all staff and students.

Our impact extends beyond academia through strong partnerships with industry and a track record of innovation, including over $5 billion in combined company value created by UCL Computer Science academics over the past decade.

The successful candidate will conduct research within the Programming Principles, Logic, and Verification (PPLV) group, in connection with the ARIA Safeguarded AI programme. They will join a vibrant research environment with a mix of senior and early-career researchers active in logic, algebra, and categorical methods in computer science, with ample opportunities for collaboration within the wider Safeguarded AI programme, including with other ARIA-funded teams.

Main purpose of the job

The post is held in connection with the Research Project “Data-Parallel Proof Checking for Monoidal Theories”, led by Professor Fabio Zanasi at University College London as part of the ARIA Safeguarded AI programme. The project builds on the Metacat proof checker and related theoretical work developed in the first phase of the programme, with the goal of strengthening the proof-checking core, developing an end-to-end reinforcement-learning theorem-proving prototype, and continuing foundational research on monoidal theories and diagrammatic proof systems, including combinatorial proof representations.

The post holder will contribute both software and theoretical outputs, working towards a feature-complete, well-documented, open-source proof-checking and theorem-proving platform that can support future work within the Safeguarded AI programme, including potential integration with other ARIA-funded teams (such as the Geolog team).

Duties and responsibilities

Conduct original research into string diagrams, monoidal theories and diagrammatic proof systems, including combinatorial proof representations and hypergraph-based rewriting methods.

Investigate how monoidal theories can more adequately represent AI-relevant models of computation, such as probabilistic, approximate, information-theoretic and Bayesian models.

Stabilise and extend the Metacat proof checker to deliver a reliable proof-checking core, including work on proof-checking semantics, binder treatment, unification and proof visualisation.

Apply knowledge in a way which develops new intellectual understanding, and contribute to developing new models, techniques and methods.

Conduct own and original research and disseminate research findings through publications, technical reports, software releases, and presentations at seminars and international conferences.

Maintain and update the software repositories associated with the project to support open-source adoption and integration.

Document the scope, limitations and complexity of the theoretical constructions developed, producing papers, technical reports or notes as appropriate.

Support integration of the resulting software and theoretical outputs into the Safeguarded AI platform, including through collaboration with other ARIA-funded teams where appropriate.

Provide regular evidence of progress against project milestones through technical reports and software releases.

Supervise students on research-related work and provide guidance to PhD and MSc students where appropriate to the discipline.

Undertake management and administration arising from the research.

Contribute to Departmental, Faculty, or UCL-wide working groups or committees as requested.

Carry out any other duties commensurate with the grade and purpose of the post.

General

Follow and actively promote the UCL Ways of Working.

Contribute to Institutional citizenship activities by undertaking voluntary roles such as fire marshal or first aider; sit on committees; assist with student open days; contribute to EDI initiatives; or any other voluntary contribution to the department or across UCL.

Carry out any other duties within the scope, spirit and purpose of the job as requested by the line manager.

This job description may be reviewed and be subject to amendment in consultation with the post holder.

Person Specification

Note to job applicant: copy and paste the following criteria into your “Statement in support of your application” and describe underneath each criteria how you meet it, giving examples. You will be scored on how you meet each criteria.

Essential Criteria: Assessment method (Application form/ Interview / Practical Test)

Qualifications, experience and knowledge

A completed PhD, or close to completion, in Computer Science, Mathematics, or a closely related field, by the post start date.: Application Research expertise and interest in category theory / monoidal categories and string diagrams, or diagrammatic reasoning more broadly.: Application / Interview

Skills and abilities

Ability to present complex technical material to specialist scientific audiences, both orally and in writing.: Application / Interview Research skills (theoretical and empirical, planning and documentary).: Application / Interview Ability to work to deadlines whilst maintaining accuracy and an eye for detail.: Interview

UCL Ways of Working

Commitment to high-quality research.: Application / Interview Ability to work collaboratively and as part of a team in a research community.: Application / Interview Commitment to continuing professional development.: Interview Commitment to UCL’s policy of equal opportunity and the ability to work harmoniously with colleagues and students of all cultures and backgrounds.: Interview Contribution to institutional citizenship activities.: Application

A commitment to UCL’s Code of Practice on Freedom of Speech: Application

Desirable Criteria: Assessment method (Application form/ Interview / Practical Test) Experience developing and maintaining research-grade software (e.g. in a functional, dependently-typed, or systems programming language).: Application / Interview Experience with proof assistants, theorem provers, or automated reasoning systems (e.g. Coq, Lean, Agda, Isabelle).: Application / Interview Experience with machine learning, in particular reinforcement learning.: Application / Interview Experience of working in a research environment; scientific publications and talks at international conferences and workshops.: Application Ability to develop and document software tools to a standard suitable for open-source release.: Application / Interview