最新消息

07/19	公布「課程問卷」。
07/19	上傳與更新練習以及解答。
07/08	上傳與更新課程教材。
07/05	緊急通知：07/16 與 07/17 兩天下午課程互調。
06/05	公布「特別演講」題目！
06/04	感謝大家報名修課！我們已將修課報名結果寄至大家報名時填的 email 信箱。沒收到的同學請盡快和我們聯繫。
05/26	更新課程頁面內容！
05/14	公布「課程列表」 、「報名資訊」 與「重要時程」！
04/24	「課前準備」內容更新！
03/11	請各位同學注意「課前準備」！
03/10	網站上線！

宗旨

「邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力。從第二年起，本研習營在兩大主題 — 程式語言與形式驗證之間輪替。今年（偶數年）之主題為程式語言，正式學分班課程名稱為「程式語言理論與型態系統」。

本課程將講授程式語言與形式驗證領域之入門理論與知識，包含邏輯、λ calculus、函數編程 (functional programming)、依值型別(dependent type)等等，希望培養學生以形式邏輯進行清晰思考的能力，了解邏輯與程式語言、型別系統的密切關係，以及型別系統在程式語言中扮演的角色，使學生能以歸納、遞迴方式理解並解決程式設計問題，能運用軟體工具輔助邏輯推理並證明程式之正確性，並具備在程式語言相關領域進行研究的能力。

自 2012 年起，本研習營正式成為台灣大學暑修課程，針對大學部學生開課，但亦歡迎研究生選修。台灣大學學生請填寫學生用報名表單。有學籍之其他學校學生可透過校際選修選課。無學籍之社會人士也可旁聽。更多細節請參考報名資訊頁。

本研習營為台灣大學資管系暑修課程，中英文課名與課號等資訊如下：

• 程式語言理論與型態系統
• Programming Language Theories and Type Systems
• 課號: IM5040
• 識別碼: 725 U3500

「邏輯、語言與計算」暑期研習營曾在 2007、 2008、 2009、 2010、 2011、 2012、 2013、 2014、 2015、 2016、 2017 年舉辦，今年為第十二屆。

時間地點

• 日期：2018 年 7 月 09 日 (週一) 至 7 月 20 日 (週五)，共計 10 天。
• 時間：每週一至週五早上 09:10 至下午 16:20。
• 地點：台灣大學管理學院一號館 102 教室。

課表

07/09	07/10	07/11	07/12	07/13
F	F	L	F	L
L	λ	λ	λ	T

07/16	07/17	07/18	07/19	07/20
π	π	π	π	Exam
L	F	λ	T

• F : 函數編程 Functional programming
• L : 邏輯 Logic
• λ : λ 演算與型別 λ-calculus and types
• π : 並行計算模型與訊程型別 Models of concurrent computation and session types
• T : Talk & Tutorial
• Exam : 期末測驗

報名方法與時間

請參考報名資訊頁與行事曆。

主辦單位

• 中央研究院資訊科學研究所
• 臺灣大學資訊管理學系
• 臺灣大學資訊工程學系
• 臺灣大學電機工程學系

聯合主辦。

課程委員

• 陳恭 Kung Chen, 政治大學資訊科學系
• 莊庭瑞 Tyng-Ruey Chuang, 中央研究院資訊科學研究所
• 穆信成 Shin-Cheng Mu, 中央研究院資訊科學研究所、台灣大學資訊管理學系
• 蔡益坤 Yih-Kuen Tsay, 台灣大學資訊管理學系
• 王柏堯 Bow-Yaw Wang, 中央研究院資訊科學研究所
• 陳亮廷 Liang-Ting Chen, 英國斯旺西大學電腦科學系
• 柯向上 Hsiang-Shang Ko, 日本国立情報学研究所

課務統籌

• 張少娟 Shao-Chuan Chang, 中央研究院資訊科學研究所
• 韓愷真 Kai-Jan Han, 中央研究院資訊科學研究所

聯絡資訊

如果有任何報名或是課程的問題，請寄信來 flolac(at)iis.sinica.edu.tw 我們會儘快給予答覆與協助。

助教資訊

待公布。