编程语言理论

编程语言理论 (PLT) 是计算机科学的一个分支，它处理被称为编程语言的形式语言的设计、实现、分析、表征和分类。 编程语言理论与其他领域密切相关，包括数学、软件工程和语言学。 该地区有许多学术会议和期刊。

在某些方面，编程语言理论的历史甚至早于编程语言本身的发展。 由 Alonzo Church 和 Stephen Cole Kleene 在 1930 年xxx发的 lambda 演算被一些人认为是世界上xxx种编程语言，尽管它旨在模拟计算而不是程序员描述算法以 一个计算机系统。 许多现代函数式编程语言都被描述为在 lambda 演算上提供了一层薄薄的外表，并且许多语言很容易用它来描述。

xxx种被发明的编程语言是 Plankalkül，它由 Konrad Zuse 在 1940 年代设计，但直到 1972 年才为公众所知（直到 1998 年才实现）。 xxx种广为人知且成功的高级编程语言是 Fortran，由 John Backus 领导的 IBM 研究人员团队于 1954 年至 1957 年开发。 FORTRAN 的成功导致了一个科学家委员会的成立，以开发一种通用的计算机语言； 他们努力的结果是 ALGOL 58。另外，麻省理工学院的 John McCarthy 开发了 Lisp，这是xxx个起源于学术界并获得成功的语言。 随着这些初步努力的成功，编程语言成为 1960 年代及以后的活跃研究课题。

此后编程语言理论史上的一些其他关键事件：

• Noam Chomsky 在语言学领域发展了 Chomsky 层次结构，这一发现直接影响了编程语言理论和计算机科学的其他分支。

• Simula 语言由 Ole-Johan Dahl 和 Kristen Nygaard 开发； 它被广泛认为是面向对象编程语言的xxx个例子； Simula 还引入了协程的概念。
• 1964 年，Peter Landin 是xxx个意识到 Church 的 lambda 演算可用于对编程语言建模的人。 他介绍了解释 lambda 表达式的 SECD 机器。
• 1965 年，Landin 引入了 J 运算符，本质上是一种延续形式。
• 1966 年，Landin 在他的文章 The Next 700 Programming Languages 中介绍了 ISWIM，这是一种抽象的计算机编程语言。 它对导致 Haskell 编程语言的语言设计具有影响力。
• 1966 年，Corrado Böhm 引入了编程语言 CUCH (Curry-Church)。
• 1967 年，克里斯托弗·斯特拉奇 (Christopher Strachey) 出版了他颇具影响力的讲义集《程序设计语言中的基本概念》，其中介绍了术语 R 值、L 值、参数多态性和临时多态性。
• 1969 年，J. Roger Hindley 发表了组合逻辑中对象的主要类型方案，后来推广到 Hindley-Milner 类型推理算法。
• 1969 年，托尼·霍尔 (Tony Hoare) 引入了霍尔逻辑，这是一种公理语义学形式。
• 1969 年，威廉·阿尔文·霍华德 (William Alvin Howard) 观察到一个高级证明系统（称为自然演绎）可以在其直觉版本中直接解释为称为 lambda 演算的计算模型的类型变体。 这被称为 Curry-Howard 通信。

• 1970 年，Dana Scott 首次发表了他关于指称语义的著作。
• 1972 年，逻辑编程和 Prolog 得以开发，从而使计算机程序可以表示为数学逻辑。
• Alan Kay 领导的 Xerox PARC 科学家团队开发了 Smalltalk，这是一种面向对象的语言，以其创新的开发环境而广为人知。
• 1974 年，John C. Reynolds 发现了系统 F。数理逻辑学家 Jean-Yves Girard 早在 1971 年就发现了它。

• 从 1975 年开始，Gerald Jay Sussman 和 Guy Steele 开发了 Scheme 编程语言，这是一种 Lisp 方言，结合了词法范围、统一的命名空间以及来自 actor 模型的元素，包括一流的延续。
• 巴克斯在 1977 年的图灵奖演讲中抨击了工业语言的现状，并提出了一类新的编程语言，现在称为函数级编程语言。
• 1977 年，Gordon Plotkin 介绍了 Programming Computable Functions，这是一种抽象类型的函数式语言。
• 1978 年，Robin Milner 为机器学习引入了 Hindley–Milner 类型推理算法。 类型理论作为一门学科应用到编程语言中，这种应用在过去的一年里导致了类型理论的巨大进步。