Bergen Language Design Laboratory (BLDL)
Programme Opening Day
1400-1415 Official opening ceremony
University of Bergen Vice-Rector for Education, Professor Kuvvet Atakan.
Faculty of Mathematics and Natural Sciences Acting Vise-Dean, Professor Rein Aasland.
Department of Informatics head, Professor Torleiv Kløve.
BLDL head, Professor Magne Haveraaen.
Carl Seger (Intel, USA; hardware design)
Interplay between language and formal verification
Departmental Lunch room, 4th level, first room on the right from the elevator
The Department of informatics, UiB, is at Thormøhlensgt. 55, NO-5008 BERGEN, 'Høyteknologisenteret' (HiB). It is a silver and blue building next to the main road from the airport to the city centre. The department front office is on the 4th level in the right "tower" when you approach the front of the building. We will be using lecture and meeting rooms in this area for the BLDL activities.
VilVite, the Bergen science centre, Thormøhlensgate 51, NO-5006 Bergen, is the building next to 'Høyteknologisenteret'. There is a free bus service (green buses) between the city centre and VilVite.
Abstracts of presentations
The design of a programming language for provably correct programs: success and failure (slides)
The functional programming language ML was designed by assembling very powerful features in a simple way. One of the drivers was the desire to be able to prove correctness of programs (Extended ML). That turned out to be much harder than expected, leading to admission of defeat, although there are alternative approaches that seem promising. Since then the landscape has changed, making a less ambitious goal, proving security properties of programs, both achievable and really useful. The presentation will end with showing some progress on that.
Evolving a widely used language: Why and how? (slides)
All language evolve/change/improve until they die. C++0x is very different from 1985 C++, today's Java is vastly different from Sun's original offering, etc. This talk considers C++'s aims and the way in which we try to improve the language to meet them. The emphasis is on the current approach to the next ISO C++ standard: C++0x.
The challenges of oil and gas data interpretation (slides)
From seismic data acquisition and processing, seismic interpretation, to economic evaluation of oil and gas reserves, oilfield data interpretation presents extraordinary challenges to computer science. As data acquisition technologies evolve and dramatically improve in efficiency, the amount of data available to geoscientists is extremely high. More memory, disk space, processor speed and a much better use of these resources is needed, and consequently, more efficient computer programming will be required to handle them robustly. This presentation will try to expose the extraordinary challenges computer science is facing in order to address the pressures of the oil and gas industry, today and tomorrow.
Easy Meta-Programming with Rascal (slides)
Meta-programs are programs that analyze, transform or generate other programs. Ordinary programs work on data; meta-programs work on programs. The range of programs to which meta-programming can be applied is large: from programs in standard languages like C and Java to domain-specific languages for describing high-level system models or applications in specialized areas like gaming or finance. In other cases, test results or performance data are also used as input for meta-programs.
Many meta-programming problems follow the EASY paradigm: Starting with some input system (initially a black box but we are gradually opening it), first relevant information is Extracted from that system and stored in an internal representation. This internal representation is then Analyzed and used to SYnthesize results. If the synthesis indicates this, these steps can be repeated over and over again.
Rascal is a new language for meta-programming that supports all phases of the EASY paradigm and is intended for solving problems in the domain of source code analysis and transformation. It has a Java-like syntax and a rich feature set including syntax analysis, pattern matching, relational calculus and term rewriting. The Rascal library provides tools ranging from Java fact extraction, access to various repositories (e.g. Subversion), and visualization. The talk gives a high-level overview of the goals and features of the Rascal language, shows some examples and concludes with research challenges. More information is available at http://www.meta-environment.org/Meta-Environment/Rascal.
Composing Domain-Specific Languages (slides)
(Separation of concerns requires linguistic integration)
The history of programming languages shows a progressive development from low-level programming languages close to the machine, to high-level languages close to the problems being solved with software. Domain-specific languages take this a step further than general purpose programming languages by making assumptions about the class of applications for which the language is intended. Complete applications typically require programs in multiple (technical) domains, which can be catered for by separate domain-specific languages. While such separation of concerns is beneficial for domain expressivity, it often leads to loose coupling and lack of static verification. Hence, the design of individual DSLs needs to be complemented with their linguistic integration.
In this talk, I illustrate these ideas with the design of WebDSL, a domain-specific language for data centric web applications. WebDSL linguistically integrates the definition of data models, user interfaces, actions, access control rules, data validation rules, styling rules, and workflow definitions. While maintaining separation between these concerns through specialized sub-languages, linguistic integration ensures static consistency checking and correct code generation. The language allows developers to concentrate on the essential design of web applications, abstracting from accidental complexity, such as the details of data persistence. The combination of high-level and low-level constructs ensures high expressivity, while supporting customization to application requirements.
Interplay between language and formal verification (slides)
At Intel hardware design we have a highly customized functional language environment that provides the basis for our formal verification tools. These have been extended many times in different ways. The presentation will look at the interplay between the language and our formal verification environment.