研究兴趣

  • 逻辑/关系式编程语言,比如: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.
  • Coinduction
  • Type theory

论文发表(按场合)
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. [doi]

大会
Conference

  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]

研讨会
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

2021

  1. JetBrains Research Mini-Conference 2021. Reimplementation of OCanren Reifiers using Light-weight Higher-kinded Polymorphism. [pdf][code]
  2. JetBrains Research Rus: Semantics of First-order Horn Clause Logic. [video]

2019

  1. HWUCS 2019: Computer Science Seminar Series. Heriot-Watt University. Edinburgh, Scotland. [web]

2018

  1. PARIS 2018: Workshop on Programming And Reasoning on Infinite Structures. University of Oxford. Oxford, England. [pdf] [web]
  2. ARW 2018: Automated Reasoning Workshop. University of Cambridge. Cambridge, England. [pdf] [web]

2017

  1. ICLP 2017: The 33rd International Conference on Logic Programming. Melbourne, Australia. [pdf] [web]
  2. STP 2017: Scottish Theorem Proving Seminar. 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 [pdf]
  2. 硕士论文 Li, Yue. " Implementing Unification Algorithms in Haskell. " MSc Thesis. University of Dundee. 2015 [pdf] [code]

技术文档
Repors

2022

  1. Using Lazy Evaluation to Improve Monadic Reifiers. This is a set of notes reflecting progressive research about, and technical development of monadic reifiers.
    • Understanding the Monadic Reifiers [Read more]
    • Solving the Problem of Non-terminating Monadic Reifiers for Certain Recursive Types [Read more]
    • On the Systematic Use of Lazy Eavluation for Defining Recursive Reifiers [Read more]
    • Simplifying the Interface of Lazy Reifiers [Read more]

2021

  1. Solution to a Textbook Exercise: An Investigation with Logical Rigor of the Problem of the Area of a Triangle on a Cartesian Plane with One Vertex at the Origin [Read more]

  2. Technical Blog : Comparing Monads in Haskell and in OCaml [Read more]

2020

  1. OCanren语言教程

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

2018

  1. 博士年度报告二 Li, Yue. " Coinductive Uniform Proof. " PhD 2nd Year Technical Report. Heriot-Watt University. 2018 [pdf]

2017

  1. 博士年度报告一 Li, Yue. " Comparative Study of Search Strategies for Term-Matching and Unification Based Resolution in Prolog. " CoALP Project Report. Heriot-Watt University. 2017 [pdf] [code] [web]

工作经历

  • 2020年4月至今 岗位名称:博士后研究员。 单位名称: JetBrains研究院 编程语言和工具实验室。导师: 德米特里·布利切夫 副教授。 单位地址:俄罗斯 圣彼得堡市。

Employment

  • April 2020 to present 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 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