2016 “逻辑、语言与计算”暑期研习营
2016 Formosan Summer School on Logic, Language, and Computation
SINICA IIS / NTUIM / NTUCSIE / NTUEE
* 研习营简介
“逻辑、语言与计算”暑期研习营希望培养学员独立进行
基础计算科学研究之能力。从第二年起，本研习营在两
大主题 — 程式语言与形式验证之间轮替。
今年（偶数年）之主题为程式语言，正式学分班课程名称
为“程式语言理论与型态系统”。
本课程将讲授程式语言与形式验证领域之入门理论与知识，
包含逻辑、λ-calculus、函数编程 (functional programming)、
Martin-Löf 型别、依值型别(dependent type)等等，
希望培养学生以形式逻辑进行清晰思考的能力，了解逻辑与
程式语言、型别系统的密切关系，以及型别系统在程式语言中
扮演的角色，使学生能以归纳、递回方式理解并解决程式设计
问题，能运用软件工具辅助逻辑推理并证明程式之正确性，并
具备在程式语言相关领域进行研究的能力。
* 日期: 2016 年 07 月 04 日 至 2016 年 07 月 15 日
* 时间: 每周一至周五 上午 9:10 - 下午 4:20
* 地点: 台湾大学管理学院 壹号馆102教室
* 课程资讯: http://flolac.iis.sinica.edu.tw
本课程为台湾大学暑期第一梯次选修课，欢迎校际选修。
本课程为暑期密集课程，上课时间为自7/4至7/15之每周一至周五
全日且须全程参与。学生网络选课前须先至以下网址填写报名资料，
经台大资管系依授课教师之规定进行筛选，筛选通过之学生方能
上网选修本课程：http://flolac.iis.sinica.edu.tw/register
欲旁听者, 即日起至 6/16(四) 24 时前可填送报名表
http://goo.gl/forms/BWwiBjiJTBYs6YKD3
报名超额时，将依所填之修课理由筛选。
※参加者请自备电脑, 可先安装 Haskell 及 Agda
* 研习营课程
函数编程 Functional Programming 陈恭 政大资讯科学系
穆信成 中研院资科所、台大资管系
演算与型别 Lambda Calculus and Types 陈亮廷 夏威夷大学马诺阿分校
资讯与电脑科学系
基础逻辑 Elementary Logic 柯向上 日本国立情报学研究所
Martin-Löf 型别理论 柯向上 日本国立情报学研究所
依值型别编程 Dependently Typed Programming 穆信成 中研院资科所、台大资管系
特别讲座：概率编程与塑模初探
The taste of probabilistic programming and modeling
Oleg Kiselyov 日本东北大学电気・情报系
邀请演讲：程式语言设计实务
Pragmatics of Programming Language Design
Robby Findler 美国西北大学电机工程与资讯科学系
热烈报名中!