




个人介绍
我是IvorySeagull,毕业于北京大学
编程语言:熟悉Rust、c++ 了解Python, Java, HTML/CSS/JavaScript
专业知识:精通计算机体系结构,阅读过整本《计算机体系结构:量化研究方法》,熟悉计算机系统设计理念,如操作系统的虚拟化,并行,可持久性与计算机网络的分层架构,可靠数据传输与拥塞控制
曾担任北京大学《计算机系统导论》(CMU 15‑213)的小班助教,这门课是信科学生系统方面的入门课,涉及体 系结构(流水线,缓存),操作系统(虚拟内存,文件IO),网络并发以及编译链接等计算机基本知识
工作经历
2024-07-01 -至今匿名开发
负责公司项目的Rust语言开发工作,包括需求分析、设计、编码、测试和维护。 参与项目技术方案的讨论和制定,对项目架构和性能优化提出建议。 与团队成员协作,确保项目进度和质量。 撰写技术文档,为团队提供技术支持。 跟进Rust语言及相关技术栈的最新动态,进行技术研究和分享。
教育经历
2020-09-01 - 2024-07-01北京大学信息与计算科学本科
技能

面向高性能计算比赛中的功率控制,需要检测程序运行时的状态来及时调整功率。 该项目是用rust编写的cli软件,用来部署多个节点上跑程序的参数,同时检测程序输出的log来判断程序的运算情况,调整CPU和GPU频率来使得总体功率在比赛要求的范围内。


大部分定理证明系统都依赖于对形式化语言的解析,生成抽象语法树(Abstract Syntax Tree,AST)并进行类型检查。通常,符号绑定在作用域内进行,每个作用域都是通过解析特定编程语言编写的程序而得到的。 然而,为了实现一个命令式且不依赖特定语言的证明系统,我们需要以某种方式存储“作用域”的信息。通过语言解析获得的作用域类似于依赖类型论的范畴语义中的上下文范畴的对象,即上下文。本文通过类比上下文范畴的定义设计了上下文结构,并用该结构存储某个上下文中已经构造出来的项。 系统的主要功能通过操作上下文结构来实现。这极大地提高了构造证明的灵活性,但同时也增加了书写的复杂性
