清华主页 EN
导航菜单

程序语言的形式语义

来源: 03-17

时间:13:30 - 16:55, every Thursday, 3/17/2022 - 6/9/2022

地点:1118&Zoom ID:638 227 8222,密码:BIMSA

组织者:蒋瀚如

主讲人:蒋瀚如

 要:

形式语义是进行程序语言研究的基础。本课程将介绍程序设计语言的形式语义,涵盖的内容包括λ演算、命令式语言的操作语义和Hoare逻辑、分离逻辑等。本课程还将介绍如何在Coq定理证明工具中形式化程序语言的语义并作推理。


预备知识:

基本的编程经验


参考书目:

1. Benjamin C. Pierce, et al. Software Foundations. 2. John C. Reynolds. Theories of Programming Languages.


主讲人简介:

蒋瀚如于2019年在中国科学技术大学取得计算机科学与技术博士学位,2019-2020年在鹏城实验室量子计算研究中心担任助理研究员,2020年加入BIMSA任助理研究员。他的主要研究方向为程序语言理论、编译器的形式化验证和量子计算中的程序语言问题。作为并发程序分离编译验证工作CASCompCert的主要完成人,获得程序语言领域顶级会议PLDI 2019Distinguished Paper Award


返回顶部
相关文章
  • 自然语言处理中的算法和建模II

    摘 要:Natural Language Processing (NLP) is an important research area in Artificial Intelligence. NLP mainly studys how to use computer technology to process linguistic texts. The specific research problems in NLP includes recognition, classification, extraction, transformation and generation of lexical, syntactic, semantic and pragmatic information. This seminar will introduce the basic conc...

  • 求真书院2022秋讨论班信息

    01 算术几何 Arithmetic Geometry内容: 暂定 Bhatt “Lecture notes on perfectoid spaces”时间: 周五晚上六点到九点地点: 理科楼某间空教室语言: 汉语,板书英语先修要求: 基本的代数几何,代数数论 (非阿域)组织者: 蒋昕童二维码:02 函数式编程与交互式定理证明Functional Programming and Interactive Theorem Proving内容: 函数式编程(Lean、F#、Haskell程序设计)与交互式定理证明(数学命题的形式化与计算机证明)时间:...