TYPES at Edinburgh
TYPES is an EU Framework 6 project, involving 15 main sites and 20
subsites across Europe. The TYPES consortium has been active and
continuously supported by the EU for more than 16 years. The current
TYPES project, from Sept 2004 through Apr 2008, is co-ordinated by
Bengt Nordström at Chalmers Technical University, Göteborg
Sweden. You can find further information about TYPES at
Edinburgh University is one of the TYPES main sites. The research
institutes participating in TYPES from the Edinburgh University School of
Informatics are
TYPES participants at Edinburgh include
- Randy Pollack
(contact person)
- David Aspinall
- James Cheney
- Lucas Dixon
- Jacques Flueriot
- Paul Jackson
- Alberto Momigliano
- John Power
TYPES topical workshops organized by Edinburgh site:
- The workshop MERLIN 2005,
MEchanized Reasoning about Languages with varIable biNding, 30
September 2005, was organised by Alberto Momigliano and Randy Pollack
of the Edinburgh site. It took place at the Tallinn site. The full
proceedings are
available. (See also printed
proceedings.)
- The workshop
MathWiki, 31 Oct - 1 Nov 2007, was organized by Randy Pollack.
It discussed ideas supporting large scale formal mathematics:
Libraries, searching, web interfaces, notation, proof languages,
collaborative working, use of large scale computing resources, etc.
Recent TYPES site visits:
- 29 May - 2 June, 2006. Lucas Dixon visited TUM.
The visit to Munich was primarily to develop a strategy for coordinating
development of Isabelle/Isar, IsaPlanner and Proof General. As well as
establishing this we also wanted to review a number of technical issues
in Isabelle. In particular, we discussed at length the need for an
internal representation of proofs suitable for proof general and
IsaPlanner. We clarified what was feasible and what was needed. Lucas
Dixon presented the the proof planning work at edinburgh and illustrated
a possible integration with proof general. We made improvements to
IsaPlanner and Isabelle during the visit as well as establishing a plan
for implemented the richer representation of proofs in Isabelle,
motivated by the talk. This representation will extend the interface for
Isabelle and support further research into proof automation using
IsaPlanner.
Lucas gave a seminar entitled
Proof Planning in Isabelle and Beyond.
TYPES Review 2006
Randy Pollack's contribution to the
TYPES review in Brussels on 29 Aug. 2006.