Papers I'm reading

Here is an incomplete selection of some good papers I'm currently reading:

• Constructing Type Systems over an Operational Semantics, Robert Harper.
• A Realizability Interpretation of Martin-Loef Type Theory, Catarina Coquand.

  These two papers give a very nice introduction to developing the metatheory of dependent type systems. Harper's paper is about extensional type theory, and Coquand's is about intensional type theory, but IMO they both demonstrate the benefits of using realizability to formulate the semantics of type theory -- they are both impressively simple, given the complexity of the type theories involved.

• Categorical Glueing and Logical Predicates for Models of Linear Logic, Masahito Hasegawa.

  This is another paper on logical relations, this time for linear logic. This is one of the papers that has made me seriously interested in classical linear logic for the first time. Basically, the "double glueing" construction used to formulate models to CLL looks a bit like the notion of "biorthogonality" or "TT-closure" sometimes to interpet higher-order programming languages, but with some very intriguing differences.

  Pitts's Parametric Polymorphism and Operational Equivalence is a good introduction to biorthogonality, though the actual origins of the idea are a bit mysterious to me. At any rate, the idea is that if you have a program value, then its "orthogonal" is the set of continuations which won't crash when supplied the value as an argument. Similarly, if you have a continuation, then its orthogonal is the set of values that won't crash the continuation. So if you take a set of values, and then take their orthogonal, and then take their orthogonal again, you have a new, potentially bigger, set of values. A "biorthogonal" is a set of values which remains the same when you take its double orthogonal. This means you can equivalently think of a set of values as the set of continuations which accept it, which is often quite convenient for defining the meaning of a type.

  With double glueing, you again think of a type in as a set of values which make it up, and a set of continuations it can supply. But unlike with biorthogonality, there is no procedure for constructing the continuations from the values or vice-versa --- instead, you get to define the values and the continuations as anything you like, as long as everything plays nicely together. This extra degree of freedom is really intriguing, and I'm curious what can be done with it.

2014 Midlands Graduate School

The 2014 Midlands Graduate School is coming up. Please attend, or send your students!

---

University of Nottingham, 22-26 April 2014

The Midlands Graduate School (MGS) in the Foundations of Computing Science is a collaboration between researchers at the Universities of Birmingham, Leicester, Nottingham and Sheffield. It was established in 1999. The MGS has two main goals: to provide PhD students with a sound basis for research in the mathematical and practical foundations of computing and to give PhD students the opportunity to make contact with established researchers in the field and their peers who are at a similar stage in their research careers.

This year, the MGS is at the University of Nottingham. It will start on 22 April and finish on 26 April.

Program

MGS2014 consists of ten courses, each with five hours of lectures plus exercise sessions. One third of the programme offers introductory (or core) courses which all participants attend. The remainder provides advanced (or specialised) courses from which each participant selects a subset depending upon his or her interests and one course given by an invited lecturer (Conor McBride).

Core Courses

Course Title	Acronym	Lecturer	Affiliation
Category Theory	CAT	Roy Crole	Leicester
Denotational Semantics	DEN	Achim Jung	Birmingham
Typed Lambda Calculus	LAM	Paul Blain Levy	Birmingham

Advanced Courses

Course Title	Acronym	Lecturer	Affiliation
Concurrency, Causality, Reversibility	CCR	Irek Ulidowski	Leicester
Theory of Randomised Search Heuristics	HEU	Dirk Sudholt, Per Kristian Lehre, Pietro S. Oliveto, Christine Zarges	Birmingham, Nottingham, Sheffield
Homotopy Type Theory	HOT	Thorsten Altenkirch	Nottingham
Infinite Data Structures	INF	Venanzio Capretta	Nottingham
Logical relations and parametricity	PAR	Uday Reddy	Birmingham
Higher-Order Functional Reactive Programming	REA	Neelakantan Krishnaswami	Birmingham

Invited Lecturer

In addition to the standard programme, Conor McBride from the University of Strathclyde will give an invited course on Dependently Typed Programming (DTP).

Registration

The deadline for registration for MGS 2014 is Friday, 21 March. The registration fee is £440.

This includes 5 nights of accommodation (from Monday 21 evening to Saturday 26 April morning), catering for lunches and coffee breaks and the conference dinner. Accommodation is at the University's Newark Hall of Residence and includes breakfast.

To register for MGS 2014, you need to book this via the University of Nottingham online store. The site will ask you to register, if this is the first time to use it. You can pay using a credit or debit card.

We recommend to register as early as possible because places will be allocated on a first-come first-serve base and it is quite possible that we run out of space before 21 March.

Contact

For any additional information, contact the local organiser, Thorsten Altenkirch, at the address txa@cs.nott.ac.uk.