中科大-耶鲁 高可信软件联合研究中心

第三届亚太地区形式化方法暑期学校将于2011年8月13日至21日，由中科大—耶鲁高可信软件联合研究中心在苏州举办、中国科学技术大学苏州研究 院协办。暑期学校旨在教授学生证明辅助工具Coq的理论基础和使用方法，并展示Coq在形式方法最前沿研究领域的应用。本暑期学校由中法信息自动化与应用 数学联合实验室（LIAMA）发起，前两届(于2009年与 2010年)在清华大学成功举办。

证明辅助工具Coq 是由法国国立计算机及自动化研究院、巴黎第七大学、巴黎第十一大学、法国国家科学研究中心、法国国立科学技术与管理学院、法国巴黎综合理工大学 联合研究开发的开源免费软件。

Coq系 统提供了一个函数式编程语言与和一个基于高阶逻辑的推理框架，可以用来形式化数学理论，并在其中严格地证明数学定理（如四色定理）；同时也可以在Coq中 形式化计算机程序并证明其性质（如操作系统内核与编译器）。暑期学校将邀请从事定理证明与形式化方法研究的国际专家来讲授如何在Coq中形式化定义理论、 开发程序以及证明程序的性质。课程内容涉及结构化递归编程，归纳证明，数据类型定义与编程，归纳性质等内容。同时还配备了多名具有熟练Coq使用经验的助 教对学员进行实践辅导。 本次授课地点为中科大苏州研究院。苏州又称“东方水城”，是一座历史悠久的文化名城。苏州园林代表了中国私家园林的最高艺术水平，素有“江南园林甲天下， 苏州园林甲江南”之誉。中科大苏州研究院坐落于独墅湖畔，周边风景优美。

招生报名

课程全程使用英文教学。本次暑期学校计划从中国与其它亚洲国家招生学员50名。课程以英文语言讲解，主要面向（但不限于）计算机科学、计算机工程与 数学专业的高年级本科生与研究生或者科研人员。学员课前仅要求掌握基本的编程技能，无其它预备知识要求。本暑期学校即日起接受报名，报名截止日期为5月 30日，报名方式为在线注册申请，网址如下：http://kyhcs.ustcsz.edu.cn/coqschool。由于招生名额有限，我们将会对申请者做进一步筛选，并在6月10日前通知申请者是否被录取。

注册

在线注册系统现在已经开放，并将于2011年五月三十号关闭。详情请登录 http://kyhcs.ustcsz.edu.cn/coqschool 进行报名并填写表格。

鉴于学员人数的限制，如果超过人数，我们将采用排名来决定录取人名单。 我们将会在2011年六月十日通知已录取的学生

重要日期

• 报名申请截止日期: 2011年5月30日
• 录取通知: 2011年6月10日
• 研讨会提交截止 2911年七月十日
• 研讨会录用通知 2-11年七月十五日
• 暑期学校开班日期: 2011年8月13日

更新

2011年6月10日 新! 我们已经对所有参与人员发送通知，请检查您的邮箱。如果你没用收到邮件，可能是因为被您的邮箱系统当成垃圾邮件处理了。 我们在此列出所有参与者名单

2011年6月1日 新! 研讨会提交系统目前开放中

2011年4月10日  在线申请系统即日起接受申请。

2011年3月29日 The online application for school will be opened soon.

2011年3月18日 Provisional Timetable: Aug 13-20

注册费

• 科大学生: 200元
• 非科大学生: 400元
• 其他学员: 800元

该费用包含教材(Coq'Art中文版)，每日午餐和一次集体活动费用。同时我们将免费提供学生宿舍（4人间），如有需要的申请者请在申请时注明。另外，若有需要帮助预定宾馆的申请者也请注明。

在登记处您将获得一份座位表，请按照座位表在教室中选好您的座位

组织单位

中科大—耶鲁高可信软件联合研究中心，中国科学技术大学苏州研究院

联系方式

电子邮件: kyhcs@ustc.edu.cn     电话: +86-512-87161338   or  +86-512-87161322