CS Frontier Tutorial 是图灵班新开设的系列科研活动，每次邀请老师或学长学姐，概述一个计算机科学中前沿的科研领域和话题，分享在这个领域的见解和收获。不同于某一门专业课第一堂课的 Introduction 或是聚焦某个特定成果的学术报告，我们希望 CS Frontier Tutorial 能帮助同学们了解和深入一个具体的前沿领域。
对于低年级同学
希望能够帮助大家了解各个方向和领域，找到自己的兴趣和热情所在，并且提供一些与导师交流的机会；
对于高年级和研究生同学
可以通过活动开阔眼界，学习到不同领域的方法论，促进交叉领域科研；
对于兴趣导向同学
希望提供一个系统学习和高效讨论的好机会。
第七期教程我们邀请到了北京大学计算机学院程序设计语言实验室2022级博士生曹奕远学长和大家分享“程序语言与证明”这一话题。本次活动会提供晚餐（pizza），欢迎所有感兴趣的同学填写下列问卷报名参加！
第七期
时 间
5月16日（星期五） 6:00pm（含晚餐时间）
地 点
静园五院 204
报告人
曹奕远
计算机学院程序设计语言实验室2022级博士生
主持人
吴天意 图灵班 2022级
听众报名
↑↑扫码报名↑↑
注：报名信息不可作为入校凭证，校外师生请自行解决入校事宜。
报告信息
分享主题
程序语言与证明
内容摘要
本次报告以程序语言与证明的关系为主线，介绍程序语言研究的关键领域，分为三部分：
如何在程序语言中实现证明：探讨程序语言如何辅助和自动化正确的形式化证明构建，而这一需求又如何推动了程序语言构造和类型系统的设计。
如何用程序直接作为证明的表示：介绍程序与直觉主义证明的深层联系，即 Curry-Howard 对应理论，展现程序语言背后的设计哲学。
如何证明程序的正确性：展示论证程序行为符合预期的理论框架和工具实现，并探讨模块化推理命令式程序所需的资源敏感的语义、类型系统和程序逻辑设计。
报告人简介
曹奕远，北京大学计算机学院程序设计语言实验室三年级博士生，导师为胡振江教授。研究兴趣包括程序语言语义、类型系统设计和程序验证，聚焦于通过程序语言技术开发安全、正确且高效的可验证程序。过去和当前工作涉及基于语法糖的语言构造语义提升、时序性质验证的类型系统，以及系统级编程场景下带证明和验证支持的语言设计与实现。
关于我们
我们是北京大学图灵班本科生，作为活动的组织者，我们深感这类有一定深度和广度的 Tutorial 的帮助之大。对我们来说，这类活动对于学术的价值观以及学术眼界的培养很有帮助，并且是一个广泛学习的机会，不会过早地限制自己并且偏安一个领域的学习和研究。
有意愿来分享科研话题的老师或者同学，或者有任何疑问和建议，欢迎联系我们：
cs_research_tc@163.com。
北京大学图灵班科研活动委员会
— 版权声明 —
本微信公众号所有内容，由北京大学前沿计算研究中心微信自身创作、收集的文字、图片和音视频资料，版权属北京大学前沿计算研究中心微信所有；从公开渠道收集、整理及授权转载的文字、图片和音视频资料，版权属原作者。本公众号内容原作者如不愿意在本号刊登内容，请及时通知本号，予以删除。
内容中包含的图片若涉及版权问题，请及时与我们联系删除
评论
沙发等你来抢