单项范畴内数据结构的可扩展编程语言方向博士研究员
PhD in Extensible Programming Languages for Data Structures in Monoidal Categories
原帖优先：申请材料、截止时间与资格以原帖和学校官方说明为准。
AI 中文速览
- 研究内容
- 本项目旨在搭建理论计算机科学中算法与复杂性理论、逻辑与编程语言理论两大分支之间的桥梁，并应用于机械化证明助手的有效实现。具体包括设计并实现一个新的函数式编程语言，使其既能通过线性与非线性类型构造器进行扩展，又能在用户定义的单项范畴中进行解释，最终产出原型编程语言及相关数学基础。
- 申请条件
- 原文未说明具体申请条件。
- 待遇
- 奖学金提供2026/7年度的学费资助和每年21,805英镑的生活津贴。
- 申请方式
- 原文未说明具体的申请方式与截止日期（注：元数据截止日期为2026-12-08）。
由 gemini-2.5-flash-lite 生成，博士岗判定置信度 100%。
岗位信息
- 截止
- （Europe/London） 剩 40 天
- 学科
- 计算机科学
- 合同类型
- 雇佣合同
- 原文薪资
- GBP 21,805 / 年（税前）
- 税后月薪（估）
- ¥13,700；房租后 ¥5,400
- 估算假设
- 单身、无子女、雇佣合同的粗略估算，以学校 offer 为准；扣除率 18%；汇率日期 2026-10-01
- 原帖发布
- 本站收录
- 内容更新
- 来源
- jobs.ac.uk（英国博士项目及学术招聘） · 最近核对 2026-10-28
- 详情核验
判定依据（原文摘录）
- 这是一个博士培养机会
PhD in Extensible Programming Languages for Data Structures in Monoidal Categories
- 提供学费与生活津贴资助
The studentship will provide funding of fees and a stipend per annum for 2026/7
原文
This project will build a bridge between the two strands of theoretical computer science, (a) algorithms and complexity theory and (b) logic and programming language theory, and to put the resulting bridge into practical applications such as in the efficient implementations of mechanized proof assistants. Algorithm designers have developed a wealth of sophisticated techniques for organising and processing data. In parallel, logicians and programming language theorists have developed linear type systems, which check how computational resources are used, and mathematical interpretations of these systems in structures called monoidal categories.
The key observation underlying this project is that many existing algorithms can be expressed in suitable linear type systems. Interpreting them in different monoidal categories can therefore yield new algorithms and data structures, allowing established designs to be adapted rather than developed from scratch. Concretely, the student will design and implement a new functional programming language that at the same time (1) can be extended with linear and non-linear type formers and (2) can be interpreted in user-defined monoidal categories. These categories can be either defined internally in the language itself or alternatively another proof assistant such as Isabelle. The project will investigate the design space of such a system, including whether to develop a standalone language or embed it within an existing proof assistant.
A central application will be the efficient implementation of proof assistants based on dependent type theory, such as Lean, Rocq and Agda. For example, interpreting catenable lists (a data structure supporting efficient concatenation) in the monoidal category of endofunctors on types yields a representation of syntax trees with efficient variable substitution. Substitution is a fundamental operation in type theory, so improving its implementation could reduce the cost of checking proofs. Expected outcomes include a prototype programming language, mathematical foundations for its interpretation mechanisms, and potentially a more efficient implementation of a proof assistant based on dependent type theory. Together, these outcomes will establish a connection between two traditionally distinct strands of theoretical computer science, yielding practical advances in the development of secure and efficient software.
Location
University of Exeter, Streatham Campus £21,805. The studentship will provide funding of fees and a stipend per annum for 2026/7