本課程將講授程式語言領域之入門理論與知識，希望培養學生以型式邏輯進行清晰思考的能力，了解邏輯與程式語言、型別系統的密切關係，以及型別系統在程式語言中扮演的角色，使學生能以遞迴／迭構方式理解並解決程式設計問題，能運用軟體工具輔助邏輯推理及證明程式正確性，並具備進一步探索程式語言相關領域的知識基礎。
邏輯程設是從型式邏輯發展出的軟體寫作方法，源於 1960 年代後期：相對於命令式程設描述如何一步步地解決問題、函數程設將問題對應至數學概念，邏輯程設另闢蹊徑，將問題表示為邏輯式，滿足此式之變數值即為問題的解答，並有泛用的求解方法。理想上，這能讓軟體設計師專心描述想完成的任務「是什麼」，然後將「如何完成」的考量交由電腦處理。一般來說這是無法實現的夢想，但對於特定種類的問題，邏輯程設仍可提供極其優雅的解法；型式上也不一定要使用完全的邏輯程式語言，亦可使用嵌於其他語言之中的領域特定語言。
這門課將以 Datalog 語言來介紹邏輯程設。Datalog 是個特別簡潔的語言，其設計是以一階述詞邏輯的一部份為基礎，再加入遞迴定義。學員將學到如何寫作 Datalog 小程式以及除錯，解決如圖論上兩點是否連通和文法解析等問題，並從「邏輯」及「操作」（程式執行）兩個角度理解這些程式。我們會特別討論在語言中加入遞迴所生的能力，以及語言中允許「否定」時產生的複雜後果。
有了以上基本知識，我們接著會探討 Datalog 與資料庫和 SQL 資料查詢語言（號稱每位程式設計師的第二語言）之間的關聯。最後我們會看 Datalog 一些較新的應用，例如軟體安全性和程式分析，讓學員體驗為何 Datalog 以及整個邏輯程設的方向至今仍然重要。
本課程以 Haskell 為工具，概述函數程式設計相關的一些必備知識，以便與其他課程銜接。由歸納法開始，我們將談資料結構與函數的歸納定義，發現函數的定義可依循資料結構的定義。而若欲證明該函數的性質，又可使用歸納法，其證明可依循函數的定義。接著我們會談到摺（fold）的觀念，發現摺可視為一種歸納法的抽象。
數學證明建立於有效的推論結構之上， 而型式邏輯學的目的是以精確簡潔的符號表達這些推論結構，並研究其性質。這門課介紹直構（intuitionistic）命題邏輯（propositional logic）和一階邏輯（first-order logic），聚焦於自然演繹系統（natural deduction），討論型式邏輯學裡基本的語法（syntactic）和語意（semantic）證明方法，並點出邏輯與計算的密切關係，最終引導至依值型別。透過對推論結構的型式化學習，這門課也為其他課程所需的數學證明基礎作好準備，特別是結構迭構原則（structural induction principles）的理解和使用。
現今許多語言如 Haskell、Agda 都會以 λ-算則（λ-calculus，其中 λ 唸作 lam-da /ˈlæmdə/）的變形作為語言的模型，因此在課程中我們將從數學角度探討 λ-calculus 以及程式語言各種基本概念跟性質。例如定義何謂計算以及計算上相等的程式證明相關性質；加入型別討論並證明一個有型別沒有副作用的程式是如何能保證計算時一定會算出結果；除了學理上的興趣外，我們也會討論具體實務上應用於許多語言中解決程式碼重複的語言特性—多型（polymorphism）。