报告题目: |
Lambda-calculus and around |
报告人: |
Pierre-Louis Curien |
|
Directeur de Recherche au CNRS
|
报告时间: |
2007-10-29 14:00 |
报告地点: |
软件学院222 |
主办单位: |
软件学院软件理论与系统所 |
简介: |
报告题目：Lambda-calculus and around
l 报告人： Pierre-Louis Curien, Directeur de Recherche au CNRS
l 报告时间：10月29号-11月1号 下午14点-17点
l 报告地点：软件学院222
l 主办单位： 软件学院软件理论与系统所
l 内容简介：
Lambda-calculus arose about 80 years ago as one of the formalisms for
expressing the notion of computable function, and also as a formalism for
higher-order logics. In computer science, it forms the basis of a number of
programming languages, starting with LISP, and nowadays OCAML or Haskell;
it also serves as a language for powerful proof assistants such as CoQ.
The course will review the fundamental theorems of the lambda-calculus
(confluence, finite developments, strong normalization for typed
restrictions, separation). Then, time permitting and according to the
wishes of the audience, we shall discuss implementation issues (Krivine
Abstract Machine, Categorical Abstract Machine), extensions of the
lambda-calculus accounting for control (or exceptions) or references (or
local variables), denotational semantics (or domain theory).
|
|
