职责：
1.针对量子计算理论与工程的实际需求，参与设计和开发DSL（domain specific language）。
2.参与DSL与量子计算调度系统的核心模块的适配与兼容，并协助日常的维护工作
3.使用形式化验证工具验证DSL的安全性
任职要求：
1.统招全日制硕士及以上学历，计算机、数学、物理、电子工程、自动化等相关专业，具备编程语言及编译器背景者优先，毕业于985、211院校(或同等水平海外院校)者优先。
2.熟悉编译原理，数学逻辑，形式化验证，定理证明的基本原理与理论。有相关课程经验者优先
3.具备编写高效的、规范的、可维护的代码的能力，熟悉软件工程开发流程，熟悉Git代码管理，熟悉Linux下的工作流（ssh，bash脚本，等等）
4.熟悉编译器前端算法（例如parser）的基本原理与实现。有实际开发经验者优先
5.熟悉haskell，ocaml，F#，scalar等函数式编程语言中至少一门
6.有coq，agda，Isabelle，lean4等定理证明器的使用经验者优先