程式語言理論

程式語言理論（英語：Programming language theory）是電腦科學的一個分支，研究程式語言的設計、實現、分析、描述和分類及其各自的特點。它屬於電腦科學，既依賴又影響着數學、軟件工程、語言學，甚至認知科學。

λ演算在程式語言理論中有舉足輕重的地位，因此程式語言理論的非官方標誌是一個小寫的「λ」字母。

歷史

從某種角度來看，程式語言理論的歷史，甚至比程式語言本身的發展更久遠。儘管阿隆佐·邱奇與斯蒂芬·科爾·克萊尼在1930年代發明的Lambda演算被一些人認為是世界上第一門程式語言，但其初衷是用於對計算進行建模，而不是作為一種程式設計師向電腦系統描述演算法的手段。許多現代的函數式程式設計語言都聲稱自己是為Lambda演算提供了「一點包裝」，並能輕鬆地以其解釋。

世界上第一門程式語言是由康拉德·楚澤於1940年代設計的Plankalkül，但其直到1972年才廣為人知，更是到1998年才被實現。Fortran則是第一門大獲成功的高階程式語言，由約翰·巴科斯領導的IBM研究者們在1954-1957年間實現。Fortran的成功使一些科學家聯合起來研究一種「通用的」電腦語言，並最終帶來了ALGOL 58；麻省理工學院的約翰·麥卡錫則開發了Lisp，其為第一門源自學術界而取得成功的程式語言。隨着1960年代這些起初的嘗試獲得成功，程式語言逐漸成為熱門的研究對象，並延續至今。

子學科及相關領域

程式語言理論中存在着幾個研究領域,或者對程式語言理論產生了深遠的影響，其中許多有相當大的重疊。此外，PLT還利用了數學的許多其他分支,包括可計算性理論、類型論和集合論。

形式語意學

在計算理論中，形式語意學是關注計算的模式和程式語言的含義的嚴格的數學研究的領域。

語言的形式語意是用數學模型去表達該語言描述的可能的計算來給出的。

形式語意學（formal semantics），是程式設計理論的組成部分，以數學為工具，利用符號和公式，精確地定義和解釋電腦程式設計語言的語意，使語意形式化的學科。

提供程式語言的形式語意的方法很多，其中主要類別有：

• 指稱語意學，着重於語言的執行結果而非過程，包括域理論；
• 操作語意學，例如抽象機（象SECD抽象機），着重於描述語言的過程；
• 公理語意學，如 謂詞變換語意學和代數語意學。

類型論

類型論提供了設計分析和研究型別系統的形式基礎。實際上，很多電腦科學家使用術語「類型論」來稱呼對程式語言的類型語言的形式研究，儘管有些人把它限制於對更加抽象的形式化如有類型lambda演算的研究。

程式分析

程式分析是指自動分析一個程式的包括正確性、健壯性、安全性和活躍性等特徵的過程。 程式分析主要研究兩大領域：程式的最佳化和程式的正確性。前者研究如何提升程式效能並且降低程式的資源佔用，後者研究如何確保程式完成預期的任務。

比較程式語言分析

比較程式語言分析旨在根據程式語言的特點將其分類為不同類型，程式語言的大類通常被稱為程式設計範式。

泛型和元程式設計

是指某類電腦程式的編寫，這類電腦程式編寫或者操縱其它程式（或者自身）作為它們的數據，或者在執行時完成部分本應在編譯時完成的工作。

領域特定語言

指專注於某個應用程式領域的電腦語言。

編譯原理

編譯原理是編寫編譯器的理論。編譯器的操作傳統上分為語法分析(掃描和解析)、語意分析(確定程式應該做什麼)、最佳化(根據某些指標改行程序的效能，通常是執行速度)和代碼生成(用某種目標語言生成和輸出等價的程式(通常是CPU的指令集)。

執行時系統

指一種把半編譯的執行碼在目標機器上執行的環境，介乎編譯器及直譯器的執行方式。包括虛擬機器、垃圾回收和外部函數介面。