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 美國西北大學電機工程與資訊科學系
熱烈報名中!