程式語言理論

編程語言理論（英語：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的指令集)。

運行時系統

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