已于2023年05月21日更新
Updated on 21 May 2023
An image of Yue Li in winter 2021, by Zhou Xiaoyan.
Dr Yue Li
黎越 博士
论文发表 按场合 按年份 学术报告 学位论文 博客、软件 工作经历 教育经历 业余爱好
Publication by venue by year Talks Degree Theses Blogs & Code Employment Education Hobbies

研究兴趣

  • 逻辑/关系式编程语言，比如：Prolog, miniKanren, OCanren, λ-Prolog
  • 函数式编程语言，比如：Scheme, Haskell, OCaml
  • 汇编语言
  • 形式逻辑理论和应用
  • 其他任何感兴趣的话题，比如法律。

Research Interests

  • Logic/relational programming languages, such as: Prolog, miniKanren，OCanren, λ-Prolog
  • Functional programming languages, such as: Scheme, Haskell, OCaml
  • Assembly
  • Formal Logic - Theory and Application
  • Any other interesting topics, such as law.

论文发表（按场合）
Publication (by venue)

期刊
Journal

  1. Komendantskaya, Ekaterina and Li, Yue. " Productive corecursion in logic programming. 逻辑编程里可以生产数据的余递归 " Theory and Practice of Logic Programming 17 (2017): 906-923. 逻辑编程理论与实践（中国计算机学会推荐国际学术期刊C类） [doi]

大会
Conference

  1. Basold, Henning and Komendantskaya, Ekaterina and Li, Yue. " Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. 统一的余归纳：Horn子句逻辑余递归证明搜索的基础 " 28th European Symposium on Programming (ETAPS/ESOP), 8-11 April 2019, Prague （中国计算机学会推荐国际学术会议B类） [web] [arXiv] [doi]

工作坊
Workshop

  1. Li, Yue and Komendantskaya, Ekaterina. " Coinductive Uniform Proofs: An Extended Abstract. " PARIS 2018: Workshop on Programming And Reasoning on Infinite Structures [pdf] [web]
  2. Komendantskaya, Ekaterina and Li, Yue. " Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract." HCVS 2018: The 5th Workshop on Horn Clauses for Verification and Synthesis. [pdf] [web]
  3. Li, Yue. " Models of Coinductive First-order Horn Clauses. " ARW 2018: The 25th Automated Reasoning Workshop [pdf] [web]
  4. Li, Yue. " Structural Resolution with Co-inductive Loop Detection. " CoALP-Ty 2016: Workshop on Coalgebra, Horn Clause Logic Programming and Types. [pdf] [doi] [code]

论文发表（按年份）
Publication (by year)

2019

  1. Basold, Henning and Komendantskaya, Ekaterina and Li, Yue. " Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses." 28th European Symposium on Programming (ESOP), 8-11 April 2019, Prague [web] [arXiv] [doi]

2018

  1. Li, Yue and Komendantskaya, Ekaterina. " Coinductive Uniform Proofs: An Extended Abstract. " PARIS 2018: Workshop on Programming And Reasoning on Infinite Structures [pdf] [web]
  2. Komendantskaya, Ekaterina and Li, Yue. " Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract." HCVS 2018: The 5th Workshop on Horn Clauses for Verification and Synthesis. [pdf] [web]
  3. Li, Yue. " Models of Coinductive First-order Horn Clauses. " ARW 2018: The 25th Automated Reasoning Workshop [pdf] [web]

2017

  1. Komendantskaya, Ekaterina and Li, Yue. " Productive corecursion in logic programming." Theory and Practice of Logic Programming 17 (2017): 906-923. [doi]

2016

  1. Li, Yue. " Structural Resolution with Co-inductive Loop Detection. " CoALP-Ty 2016: Workshop on Coalgebra, Horn Clause Logic Programming and Types. [pdf] [doi] [code]

学术报告
Talks

2023

  1. ProLaLa @ POPL 2023. Formalising Criminal Law in the Catala Programming Language. 初探基于Catala编程语言的美国佛罗里达州刑法的计算机形式化 （中国计算机学会推荐国际学术会议A类-分会场）[abstract][slides]

2021

  1. JetBrains Research Mini-Conference 2021. Reimplementation of OCanren Reifiers using Light-weight Higher-kinded Polymorphism. 探索用“轻量高种多态”技巧实现OCanren语言锐化组件的可行性和利弊 （JetBrains研究院年终报告） [pdf][code]
  2. JetBrains Research Rus: Semantics of First-order Horn Clause Logic. 一阶Horn字句逻辑的最大不动点与最小不动点语义 （JetBrains研究院入职报告） [video]

2019

  1. HWUCS 2019: Computer Science Seminar Series. Coinductive Uniform Proof and its Soundness. "统一证明"形式证明系统的余归纳拓展及其正确性 （赫瑞瓦特大学计算机学院博士生年度报告）Heriot-Watt University. Edinburgh, Scotland. [web]

2018

  1. PARIS @ LICS 2018: Workshop on Programming And Reasoning on Infinite Structures. Coinductive Uniform Proof and its Soundness. "统一证明"形式证明系统的余归纳拓展及其正确性 University of Oxford. Oxford, England. （中国计算机学会推荐国际学术会议A类-分会场） [pdf] [web]
  2. ARW 2018: Automated Reasoning Workshop. Semantics of First-order Horn Clause Logic. 一阶Horn字句逻辑的最大不动点与最小不动点语义 University of Cambridge. Cambridge, England. [pdf] [web]

2017

  1. ICLP 2017: The 33rd International Conference on Logic Programming. Productive corecursion in logic programming. 逻辑编程里可以生产数据的余递归 Melbourne, Australia. [pdf] [web]
  2. STP 2017: Scottish Theorem Proving Seminar. Productive corecursion in logic programming. 逻辑编程里可以生产数据的余递归 University of Glasgow. Glasgow, Scotland. [pdf] [web]

学位论文
Degree Theses

  1. Li, Yue. " A Proof-Theoretic Approach to Coinduction in Horn Clause Logic. " PhD Thesis. Heriot-Watt University. September 2019 博士论文： Horn子句逻辑余归纳的证明理论 [pdf]
  2. Li, Yue. " Coinductive Uniform Proof. " PhD 2nd Year Technical Report. Heriot-Watt University. 2018 博士年度报告二："统一证明"形式证明系统的余归纳拓展 [pdf]
  3. Li, Yue. " Comparative Study of Search Strategies for Term-Matching and Unification Based Resolution in Prolog. " CoALP Project Report. Heriot-Watt University. 2017 博士年度报告一：研究比较Prolog编程语言里基于项匹配与基于合一的搜索策略 [pdf] [code] [web]
  4. Li, Yue. " Implementing Unification Algorithms in Haskell. " MSc Thesis. University of Dundee. 2015 硕士论文：用Haskell编程语言实现合一算法 [pdf] [code]

博客、软件
Blogs & Code

2023

  1. Blog: Logical Operations on The ASCII Symbols 0 and 1 [HTML]
  2. Code: Generating a 0 to 520 Binary Factorial Table Using x86 Assembly [HTML, CODE]
  3. Blog: On Overflow of Unsigned Integer Multiplication [HTML, PDF]
  4. Blog: On Binary Integer Subtraction with the x86 SUB Instruction [HTML]

2022

  1. Code: A Florida DUI fine calculator. 佛罗里达州醉驾/毒驾罚款计算器原型机 [HTML]
  2. Code: A web interface for 2022 Florida Criminal Punishment Code Scoresheet. 2022版佛罗里达州刑事惩罚条例积分量刑表网页版原型机 [HTML]
  3. Code: Untyped_unify - a library for first-order unification of OCaml runtime values. 针对OCaml编程语言运行时数值的一阶合一算法 [Code]
  4. Code: OInspect - a textual inspector for OCaml runtime value representation. OCaml编程语言运行时数值查看器 [Code]
  5. Blog: Who's complement? 研究二进制整数的二补法为什么叫“二补法”[PDF]
  6. Blog: The RStream data structure for tabling in OCanren. 学习理解OCanren编程语言底层的一个名为RStream的基本数据结构 [PDF]
  7. Code: On Monadic Reifiers. 研究用单子编程风格实现OCanren语言的锐化组件会有什么效果 [Code]

2021

  1. Blog: Solution to a Textbook Exercise: Area of a Triangle on a Cartesian Plane 解一个练习题，练习分类讨论：推导二维平面上给定顶点坐标求三角形面积的公式 [PDF]
  2. Blog: Comparing Monads in Haskell and in OCaml 比较Haskell编程语言和OCaml编程语言里单子的异同 [HTML]

2020

  1. OCanren语言教程

    A tutorial for Ocanren, the typed embedded relational programming langauge.

工作经历

  • 2022年9月至2023年1月 岗位名称：Catala程序员。单位名称：赫瑞瓦特大学。导师：叶卡捷琳娜·科敏达茨卡娅 教授。单位地址：英国 爱丁堡市。
  • 2020年4月至2022年4月 岗位名称：博士后研究员。 单位名称： JetBrains研究院 编程语言和工具实验室。导师： 德米特里·布利切夫 副教授。 单位地址：俄罗斯 圣彼得堡市。

Employment

  • September 2022 to January 2023 Catala Programmer. Heriot-Watt University, Edinburgh, UK. Supervisor: Prof. Ekaterina Komendantskaya.
  • April 2020 to April 2022 Postdoc Researcher. JetBrains Research, St. Petersburg, Russia. Supervisor: Dr Dmitri Boulytchev.

教育经历

  • 计算机科学博士 授予单位：赫瑞·瓦特大学。校址：英国 苏格兰 爱丁堡市。 学习年限：2016年09月至2019年08月。 博士导师：(正导师) 叶卡捷琳娜·科敏达茨卡娅 副教授 和（副导师）马克·劳森 教授。答辩日期: 2019年08月20日。答辨委员会成员：约翰·鲍尔 教授，安德鲁·爱尔兰 教授 和 阿尔伯特·伯格 教授
  • 计算机科学与国际商务硕士 授予单位：邓迪大学。校址：英国 苏格兰 邓迪市。学习年限： 2014年至2015年。硕士导师：叶卡捷琳娜·科敏达茨卡娅 高级讲师
  • 通信工程学士 授予单位：湖南大学。 校址：中国长沙。 学习年限：2010年至2014年，其中2013-2014学年在英国邓迪大学交流学习。毕业设计导师：埃里克·阿贝尔 教授

Education

  • PhD in Computer Science Heriot-Watt University, UK. September 2016 - August 2019. Supervisors: Dr Ekaterina Komendantskaya and Prof. Mark V. Lawson. Viva Voce passed on 20 August with Prof. John Power, Prof. Andrew Ireland and Prof. Albert Burger.
  • MSc with Distinction in Computer Science and International Business University of Dundee, UK. 2013-2015. Supervisor: Dr Ekaterina Komendantskaya.
  • BEng in Telecommunication Engineering Hunan University, Changsha, China. 2010-2014. I visited the Univesity of Dundee during the 2013-2014 academic year, where Prof. Eric Abel supervised my degree project.

业余爱好

Hobbies

  • A Chinese translation of the foreword of the book Edinburgh LCF.
  • A slightly math-flavored introduction to the idea of the batch enrolment system for high school admission adopted in the city of Haikou, the capital of the Chinese tropical island province Hainan, as of autumn of 2021.
  • I translated A History of OCaml from English into the simplified Chinese language during the New Year holiday of 2021.
  • I translated Landmark patent case broke Selden's lock on auto industry from English into the simplified Chinese language during the New Year holiday of 2021.
谷歌字体 Google Font