[Agda] Spring School in Generic and Indexed Programming

[Jeremy.Gibbons at comlab.ox.ac.uk]

SPRING SCHOOL ON GENERIC AND INDEXED PROGRAMMING
Wadham College, Oxford, 22nd to 26th March 2010


TOPIC

"Generic programming" is about making programs more widely applicable
via exotic kinds of parametrization - not just along the dimensions of
values or of types, but of things such as the shape of data, algebraic
structures, strategies, computational paradigms, and so on. "Indexed
programming" is a lightweight form of dependently typed programming,
constraining flexibility by allowing one to state and check
relationships between parameters: that the shapes of two arguments
agree, that an encoded value matches to some type, that values
transmitted along a channel conforms to some protocol, and so on.

The two forces of genericity and indexing balance each other nicely,
simultaneously promoting and controlling generality.  The EPSRC-funded
Generic and Indexed Programming project at Oxford has been exploring
their interaction over the period 2006 - 2010; this school is the
closing activity of the project.


LECTURERS

Six lecturers from the Programming Languages community, each an
acknowledged expert in their specialism, will cover various aspects of
generic and indexed programming. Each will give about four hours'
lectures, distributed throughout the week.

  Nate Foster (Princeton University)
  "Bidirectional Programming"

  Ralf Hinze (University of Oxford)
  "Generic Programming with Adjunctions"

  Oleg Kiselyov (Fleet Numerical Meteorology and Oceanography Center)
  "Typed Tagless Interpreters"

  Simon Peyton Jones (Microsoft Research Cambridge)
  "Type Functions"

  Jeremy Siek (University of Colorado at Boulder)
  "Concepts in C++"

  Stephanie Weirich (University of Pennsylvania)
  "Generic Programming with Dependent Types"



PREREQUISITES

The school is aimed at doctoral students in programming languages and
related areas; however, researchers and practitioners will be very
welcome, as will strong masters students with the support of a
supervisor. It will be assumed that participants have a good
understanding of typed functional programming, as in Haskell or
O'Caml.


DATES

Registration deadline: 19th February
School:                22nd March (0900) to 26th March (lunchtime)


VENUE

Lectures will be held and accommodation provided in Wadham College in
the centre of Oxford. The college celebrates its 400th anniversary in
2010; notable past members include Sir Christopher Wren, the founder
of the Royal Society, and notable present ones Marcus du Sautoy, the
mathematician and TV presenter.


COSTS

Costs will be kept low, thanks to support from EPSRC. There will be a
nominal registration fee, and B&B accommodation in college will be
about £55 per night. (Precise costs are yet to be determined.)


FURTHER INFORMATION

Further information, including instructions on how to register,
will be available soon at the website:

  http://www.comlab.ox.ac.uk/projects/gip/school.html