Synthetic Computability

Andrej Bauer has made available his tutorial slides on Synthetic Computability, which he gave at the Mathematical Foundations of Programming Semantics #23 conference last month.

He motivates the idea of a synthetic theory, with reference to Hyland's construction of Eff (the effective topos), and tackles the ideas lying behind synthetic domain theory, one of the most rarefied areas of PL semantics, as accessibly as I have seen it done.

Highly theoretical, highly recommended. Via Bauer's announcement at his Mathematics and Computation weblog.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

No effective topos here

Uhm, let me correct this a little bit:

  • The tutorial does not explain the effective topos at all. It just states that the effective topos is a model of what I am doing.
  • I do very little of what would be called "synthetic domain theory". For the real stuff, have a look instead at Alex Simpson's lecture Beyond classical domain theory from the same tutorial. It's excellent stuff.

Iteration #2

I've tweaked the story: is it OK now? I was first exposed to synthetic domain theory through a long seminar that Thomas Streicher gave to the Oxford PRG in the mid 90s: about no other talk do I recall enduring such a high degree of mental exertion. I would have got much more out of that seminar with much less pain had I the chance to read such an excellent introduction as your lecture slides. Hope that explains the second point, the first is probably a result of reading too much discussion of Kripke in the last few days, thus becoming confused about the differences between referring to, describing and explaining something...

Those lectures of Simpson are new to me, but I have always found Simpson's teaching materials on the semantics of programming languages to be excellent.