To congratulate Bengt for his contributions to computer science, and to commemorate the tradition in Gothenburg that he was instrumental in founding, we are organizing this symposium.

Invited speakers and programme

9.30 Robin Milner: Models, processes and bigraphs.

Abstract: Compare model building in informatics with model-building in natural science. First, a similarity: both are to do with abstracting from reality. We cannot rigorously verify that the circuit diagrams of a computer are correctly realised by an actual computing engine any more than we can rigorously verify Einstein's physical theories; we can only observe and perhaps falsify (Carl Popper).

Second, two differences: (1) For a natural scientist, reality precedes the model, and in informatics the model comes first. (2) In informatics, probably more than in natural science, we have to create a tower of models at increasing levels of abstraction; these models can (and should) be rigorous entities, and we can (and should) rigorously verify that each abstracts correctly from the those below it.

The von Neumann machine is a low-level model that has been abstracted successfully, over half a century, to higher levels. It is a platform for higher-order sequential computing, as evidenced by the multitude of high-level languages that abstract from it.

The von Neumann machine is no good for ubiquitous computing, where we are concerned with interaction in populations of informatic entities, which also reconfigure their structural (spatial) relationship. These, and their space, can be physical or virtual. What is a platform model for ways to think abstractly about ubiquitous computing? I put forward bigraphs as a Ubiquitous Abstract Machine.

Robin Milner is professor emeritus at the University of Cambridge Computer Laboratory. He received the Turing award in 1991 for his work on "1) LCF, probably the first theoretically based yet practical tool for machine assisted proof construction; 2) ML, the first language to include polymorphic type inference together with a type-safe exception-handling mechanism; 3) CCS, a general theory of concurrency". Prior to that Robin Milner had been awarded an honorary doctorate at Chalmers for his role as a source of inspiration for the development of computer science at Chalmers.

10.30 Coffee.

11.15 Per Martin-Löf: Evaluation of open expressions.

Abstract: The informal, or intuitive, semantics of type theory makes it evident that closed expressions of ground type evaluate to head normal form, whereas metamathematics, either the method of computability or the method of normalization by evaluation, is currently needed to show that expressions which are open or of higher type can be reduced to normal form. The question to be discussed is: Would it be possible to modify the informal semantics in such a way that it becomes evident that all expressions, also those that are open or of higher type, can be reduced to full normal form?

Per Martin-Löf is professor of Mathematical Logic at the Department of Mathematics at University of Stockholm. He is the creator of Intuitionistic Type Theory, a foundational language for constructive mathematics which is simultaneously a functional programming language with dependent types. This language has been very influential both in the area of programming languages and in the area of interactive proof assistants. Per Martin-Löf has collaborated with Bengt Nordström and others in Gothenburg on the application of this theory to computer science.

12.15 Lunch.

13.45 Lennart Augustsson: Haskell for DSELs: The Good, the Bad, and the Ugly.

Abstract: Haskell has turned out to be an excellent language for defining DSELs (Domain Specific Embedded Languages). Many of the commercial uses of Haskell are in fact DSELs. Two of the reasons for Haskell's success are the very light weight syntax, that can be adapted for the DSEL, and the very flexible type system that can also be adapted to the DSEL.

In this talk I'll show some examples of how Haskell works out very well, but also where it falls short of doing the best job. The ugly will also make some appearances.

Lennart Augustsson works at Standard Chartered Bank, London, England. He was previously a lecturer in Computer Science at Chalmers, and one of the initial members of the Programming Methodology Group. Lennart Augustsson did ground breaking work on compilers for lazy functional programming languages. During recent years he has held numerous industrial appointments, where he has applied functional programming in areas ranging from banking to hardware description.

14.45 Thierry Coquand: A Simple Programming Language.

Abstract: The first Technical Report of the Programming Methodology Group was "Description of a Simple Programming Language" by Bengt. It presents a typed functional programming language with types as objects. I will first recall some features of this work, and then try to explain how they can be used in the design of a simple implementation of dependent type theory.

Thierry Coquand is professor of Programming Logic at the Department of Computer Science and Engineering, University of Gothenburg. He received the Kurt Gödel Centenary Research Prize Fellowship in 2008 "for his pioneering research into the foundations of mathematics". Thierry Coquand works at the boundary between mathematical logic and theoretical computer science, and has investigated the links between mathematical proof and computer programs. He is one of Bengt Nordström's colleagues in the Programming Logic group.

15.45 Coffee.

16.15 Robin Cooper: Are natural languages formal languages?

Abstract: The logician Richard Montague, founder of what came to be known as Montague Grammar, wrote a paper called 'English as a Formal Language'. His claim was that there was no significant difference between the artificial languages of logicians and natural languages like English and Swedish. In this talk I will suggest that we need to refine this view and that there are important roles for type theoretical tools such as grammatical frameworks and record types in the analysis of how we interact using natural language.

Robin Cooper is professor of Computational Linguistics at the University of Gothenburg and is known for his pioneering work on the semantics of natural language, in particular on quantifiers. Soon after coming to Gothenburg in 1995, he and Bengt Nordström started a cooperation, which led to the founding of the Language Technology group at the Department of Computer Science and eventually to the multidisciplinary Centre of Language Technology, one of the eight focus areas of research of the University of Gothenburg.

Location