邏輯、語言與計算暑期研習營
Formosan Summer School on Logic, Language, and Computation, 20247/1-7/12（暫定） 09:00-17:00
Formosan Summer School on Logic, Language, and Computation, 2024本課程將講授程式語言領域之入門理論與知識，希望培養學生以型式邏輯進行清晰思考的能力，了解邏輯與程式語言、型別系統的密切關係，以及型別系統在程式語言中扮演的角色，使學生能以遞迴／迭構方式理解並解決程式設計問題，能運用軟體工具輔助邏輯推理及證明程式正確性，並具備進一步探索程式語言相關領域的知識基礎。
FLOLAC 2024 很榮幸邀請到劍橋大學 Neel Krishnaswami 教授擔任特別講師，講題待定。
本課程以 Haskell 為工具，概述函數程式設計相關的一些必備知識，以便與其他課程銜接。 由歸納法開始，我們將談資料結構與函數的歸納定義，發現函數的定義可依循資料結構的定義。 而若欲證明該函數的性質，又可使用歸納法，其證明可依循函數的定義。 接著我們會談到摺 (fold) 的觀念，發現摺可視為一種歸納法的抽象。
數學證明建立於有效的推論結構之上， 而型式邏輯學的目的是以嚴謹符號表達這些推論結構並研究其性質。 這門課聚焦於命題直構邏輯 (propositional intuitionistic logic) 的自然演繹系統 (natural deduction)，討論型式邏輯學裡基本的語法 (syntactic) 和語意 (semantic) 證明方法，並點出邏輯與計算的密切關係，銜接至依值型別課程。 透過對推論結構的型式化學習，這門課也為其他課程所需的數學證明基礎作好準備。
現今許多語言如 Haskell、Agda 都會以 λ-算則 （λ-calculus，其中 λ 唸作 lam-da /ˈlæmdə/）的變形作為語言的模型，因此在課程中我們將從數學角度探討 λ-calculus 以及程式語言各種基本概念跟性質。例如定義何謂計算以及計算上相等的程式證明相關性質；加入型別討論並證明一個有型別沒有副作用的程式是如何能保證計算時一定會算出結果；除了學理上的興趣外，我們也會討論具體實務上應用於許多語言中解決程式碼重複的語言特性—多型（polymorphism）。