钟晟

我现在已作为应用科学家入职AWS!
我已经从麦吉尔大学获得博士学位!我的博士导师是Brigitte Pientka教 授。我此前在滑铁卢大学读计算机的数学硕士,导 师是Ondřej Lhoták教授。本科在复旦大学
现在,我主要学习编程语言,形式证明和类型理论,用到CoqAgda等工具。我的研究方向 属于计算机科学和数学的交叉方向,涉及到探索计算机的数学本质。其中,类型理论是非经典数 学理论,是不同于集合论的数学基础,是一种构造数学。在哲学里,这类数学被称作数学直觉主 义。我本人认为这个翻译相当烂。
我的学习范围非常广泛,每个阶段的学习内容都不尽相同。尽管当前学习的是相当理论化的数学 和计算机,但是在工作时主要是调试分布式程序提升实时效率;也没少调过奇怪的bug,是非常 工程化的。本科后两年主要学习控制理论和机器人学。计算机科学的基础是本科时自学的。初高 学过数学、物理和化学竞赛,有一些奖。
我从2020年九月开始拿加拿大自然科学与工程研究会(NSERC)的奖学金。
我反对996工作制 996.icu


教育背景

麦吉尔大学

加拿大,魁北克,蒙特利尔

哲学博士
计算机科学

Grade: 4.0/4.0

Thesis: Foundations and Applications of Modal Type Theories (code) (slides)

研究不同类型的模态类型论及其在元编程领域的应用

Abstract

Over the past few decades, type theories as mathematical foundations have been extensively studied and are well understood. Many proof assistants implement type theories and have found important applications to provide critical security guarantees. In these applications, users often write meta-programs, programs that generate other programs, to implement proof search heuristics and improve their work efficiency. However, as opposed to the deep understanding of type theories, it remains unclear what foundation is suitable to support meta-programming in proof assistants. In this thesis, I investigate modal type theories, a specific approach to this problem. In modal type theories, modalities are a way to shallowly embed syntax into the systems, so users can write meta-programs that manipulate syntax through these modalities.
I explore two different styles of modal systems. In the first part, I investigate the Kripke-style systems, which faithfully model the familiar quasi-quoting style of meta-programming. I develop an explicit substitution calculus and scale it to dependent types, introducing Mint. I prove strong normalization of Mint, which implies its logical consistency, using an untyped domain model.
Nevertheless, the Kripke-style systems only support composition and execution of code, and they cannot easily support a general recursion principle on the structure of code. To support such a general recursion principle, I develop the layered style, where a system is divided into nested layers of sub-languages. The layered style scales quite naturally to dependent types, introducing DeLaM. DeLaM allows users to compose, execute and recurse on dependently typed code. I prove that DeLaM is weakly normalizing and its convertibility problem between types and terms is decidable. Hence, DeLaM provides a type-theoretic foundation to support type-safe meta-programming in proof assistants.

Courses:
  • COMP 550 Natural Language Processing (report)
  • COMP 520 Compiler Design (report) (code)
  • COMP 596 Topics in Computer Science 3 (Theoretical Foundations of Reliable Meta-programming) (report)
  • COMP 700 Comprehensive Examination (report)
  • IFT 6172 Semantics of programming languages (蒙特利尔大学) (report) (code)
  • COMP 701 Thesis Proposal and Area Examination (report) (slides)
09 / 2019 - 11 / 2024

滑铁卢大学

加拿大,安大略省,滑铁卢

数学硕士
计算机科学

Grade: 94.4%

Thesis: Decidability and Algorithmic Analysis of Dependent Object Types (DOT) (code) (slides)

研究DOT运算子的(不可)判定性和算法性质。

Abstract

Dependent Object Types, or DOT, is a family of calculi developed to study the Scala programming language. These calculi have path dependent types as a feature, and potentially intersection types, union types and recursive types. So far, the study of DOT calculi mostly focuses on the soundness proof, which does not directly contribute to development of compilers. This thesis presents a detailed investigation of decidability and algorithmic properties of the family of DOT calculi.
In decidability analysis, the undecidability of subtyping of several calculi is formally established, including the D<: and D∧ calculi. Prior to this investigation, the undecidability of subtyping of all DOT calculi including D<: was open. Decidability analysis puts emphasis on a particular form of subtyping rules, called normal form. It turns out that a normal form definition is not only as expressive, but also more suggestive than the original definition. A conceptual device, called small-step analysis, is introduced to assist converting a usual definition of subtyping to its normal form definition. Moreover, decidability analysis gives direct contributions to the algorithmic analysis, by revealing two decidable fragments of D<: in declarative form, called the kernels. Decidability analysis also suggests a novel subtyping algorithm framework, stare-at subtyping. Stare-at subtyping and an existing algorithm are shown to be sound and complete w.r.t. their corresponding kernels.
In algorithmic analysis, stare-at subtyping is extended to other calculi, with more features than D<:, including D∧, μDART and jDOT. In μDART and jDOT, bi-directional type assignment algorithms are developed. The algorithms developed in this thesis are all shown to be sound with respect to their target calculi and terminating.
During the development of the algorithms, analysis shows a number of ways in which the Wadlerfest DOT calculus does not directly correspond to the Scala language, while substantially increases the difficulties of algorithmic design. jDOT, therefore, is developed as an alternative formalization of Scala.

Courses:
  • CS 341 Algorithms
  • CS 745 Computer-Aided Verification
  • CS 766 Theory of Quantum Information (report)
  • ECE 653 Software Testing, Quality Assurance and Maintenance
  • CS 860 Advanced Topics in Algorithms and Complexity (report)
09 / 2017 - 08 / 2019

复旦大学

上海

理学学士
电子工程

Grade: 3.35/4.0

09 / 2010 - 07 / 2014



教学活动

麦吉尔大学

加拿大,魁北克省,蒙特利尔

助教

COMP 360, Algorithm Design (算法设计)
COMP 302, Programming Languages and Paradigms (编程语言和范式)
COMP 527, Logic and Computation (逻辑和计算)
COMP 523, Language-based Security (基于语言的安全)

09 / 2019 - present

滑铁卢大学

加拿大,安大略省,滑铁卢

助教 / Instructional Apprendice

CS 241, Foundation of Sequentual Programs (顺序编程基础)
CS 343, Concurrent and Parallel Programming (并发和并行编程)

09 / 2017 - present

其他活动

POPL 2023

artifact evaluation committee member

2022 秋天

ICFP 2021

artifact evaluation committee member

2021 夏天

HoTT Spring School (EPIT)

学生

2021

ICFP 2020

artifact evaluation committee member

2020 夏天

POPL 2020

学生志愿者

01/19/2020-01/25/2020

Oregon Programming Languages Summer School

学生

带奖学金

2019

DeepSpec Summer School

学生

带奖学金

2018

工作经验

亚马逊云科技

美国,华盛顿州,西雅图

Applied Scientist II
11 / 2024 - present

亚马逊云科技

美国,明尼苏达,明尼亚波利斯

Applied Scientist Intern
05 / 2023 - 08 / 2023

亚马逊云科技

美国,麻省,波士顿

Applied Scientist Intern
06 / 2022 - 09 / 2022

亚马逊云科技

加拿大,魁北克省,蒙特利尔

Applied Scientist Intern
05 / 2020 - 08 / 2020

摩根士丹利

加拿大,魁北克省,蒙特利尔

Summer Analyst Intern
05 / 2018 - 08 / 2018

摩根士丹利

加拿大,魁北克省,蒙特利尔

Java / Scala Developer
10 / 2015 - 07 / 2017

Nexsan Technologies

加拿大,魁北克省,Dorval

Software Developer
08 / 2014 - 10 / 2015

国双科技

上海

.Net实习工程师
05 / 2014 - 06 / 2014

Virtuos

上海

QA实习
07 / 2013 - 08 / 2013

勤学奖金

Postgraduate Scholarships-Doctoral

Natural Sciences and Engineering Research Council (NSERC)

09 / 2020 - 08 / 2023

Doctoral (B2X) Research Scholarship

Fonds de recherche du Québec - Nature et technologies (FRQNT)

09 / 2020 - 08 / 2024

Trottier Accelerator Award

School of Computer Science, McGill University

09 / 2020 - 08 / 2022

the Charity Exercise Award

School of Computer Science, McGill University

01 / 2020 - 04 / 2020

其他信息

我有时后会在知乎回答编程语言相关的问题。欢迎关注我的知乎帐号(链接在上面)。
讲四门语言。英语较优,雅思8.5;日语一般,日常听说读没啥障碍。
佛山人;不,我不会打咏春

我喜欢玩电子游戏,打羽毛球和看电影。但是读硕以后基本没有闲暇功夫了。