Code from the past couple of posts on context semantics is now available on Planet.
PLaneT Package Repository : PLaneT > dvanhorn > dilbert.plt
Think of a program as a big graph, constructed out of the pieces of its syntax. Using λ-calculus syntax as an example: an application (@) links to its context and two subexpressions; an abstractions (λ) links to its expression context, subexpression, and variable binding; a bound variable occurrence links to its expression context and [...]
The denotation of λs.λz.s(sz) in the geometry of interaction.
(letrec ((＊ (λ (c) (cons π1 c)))
(π23
(λ (c)
(π21
[...]
I just came across the TLCA List of Open Problems, which includes 20 unsolved problems in the areas of:
Typed and untyped lambda-calculi as models of computation.
Proof-theory: Natural deduction, sequent calculi, cut elimination and normalization. Propositions as types, linear logic and proof nets.
Semantics: Denotational semantics, game semantics, realizability, categorical models.
Programming languages: Foundations of functional and object-oriented [...]
Patrick Cousot’s celebrated thesis has been scanned and is available for download (in French). Thanks to Jan Midtgaard for the link.
A new book on digraphs is out by Turing Award winner, Robin Milner: The Space and Motion of Communicating Agents, Cambridge University Press, 2009. The prologue is available from Milner’s notes on the bigraphical model and the Ubiquitous Abstract Machine.
Wednesday, January 16, 2008
Harry Mairson is teaching a semantics graduate course and the reading list looks very enjoyable, if you’re into that sort of thing. As Harry said on the first day, the course is really more about computational logic and proof theory than semantics, but due to various reasons, it’s being offered under the auspices of [...]