Tag Archives: Verification

Global Systems Science meets Programming Languages and Systems

Martin Elsman from HIPERFIT (@DIKU.dk) will present GSS meets Programming Languages and Systems in the workshop on GSS Languages, 2013-06-11.
Abstract In this talk, we demonstrate how functional programming and domain specific languages, in particular, can be useful for effectively deriving performance efficient programs and systems. As an example, we outline a system for specifying financial contracts (used in practice by the financial industry) and demonstrate the effect of applying programming language technology to derive tools for pricing contracts efficiently on modern parallel hardware. We argue that research in managing and querying big data and efficiently performing big computations (simulations), as for instance carried out by the HIPERFIT research center, is a central ingredient of the development of a Global Systems Science.

Patrik Jansson

CFP: Functional High-Performance Computing (FHPC 2013)

I just want to “advertise” the Functional High-Performance Computing workshop which this year has “Large-Scale Simulation” as their theme which I think fits very well with GSS. Half of the organizers (Fritz Henglein and Jost Berthold) are at the HIPERFIT research center in Denmark (HIPERFIT: research in tailor-made expressive programming languages, frameworks, tools and technologies for financial modeling, and effective use of modern parallel hardware without compromising correctness, transparency or portability.)


Kind regards,

Patrik Jansson



The FHPC workshop aims at bringing together researchers exploring uses
of functional (or more generally, declarative or high-level) programming
technology in application domains where large-scale computations arise
naturally and high performance is essential. Such computations would
typically — but not necessarily — involve execution on highly parallel
systems ranging from multi-core multi-processor systems to graphics
accelerators (GPGPUs), reconfigurable hardware (FPGAs), large-scale
compute clusters or any combination thereof. It is becoming apparent
that radically new and well founded methodologies for programming such
systems are required to address their inherent complexity and to
reconcile execution performance with programming productivity.


GSS Languages workshop

As part of the GSS conference in June, I’m chairing a workshop on “Formal Languages and Integrated Problem Solving procedures in GSS”. It is one of five parallel workshops on “Knowledge Technologies for GSS” on Tuesday 2013-06-11: 11.00 – 13.00. I’ve created a wiki-page with some more details about the workshop:


So far it contains the text below, but it will be completed within a few days.


Patrik Jansson


Global Systems Science (GSS) is about developing systems, theories, languages and tools for computer-aided policy making with potentially global implications. The focus of this workshop is the interaction between core computer science, software engineering and GSS. Topics covered include

  • Languages for policy formulation and enforcement
  • Software as a key to productivity and innovation in industry and academia
  • Domain Specific Languages for Financial IT

We will also touch upon

  • Dependable modelling
  • Verification and Validation of Simulation Models


Speaker: Piero Bonatti

Title: Languages for policy formulation and enforcement

Abstract: Policies govern and constrain a system’s behavior, and as such specify mappings from complex situation descriptions to decisions (or at least sets of options to support human decision making). The perfect languages for expressing such mappings should enjoy a number of features, including: clarity and conciseness, explainability, formal verifiability, and the ability of adapting to an enormous number of possible event combinations. The same requirements arise in the restricted domain of security policies. In this talk, the experience gathered in this field will be reported with the purpose of identifying the most effective languages for policy formulation.

Speaker: Jaana Nyfjord, Director Swedsoft, SICS, Sweden

Title: TBD

Speaker: Martin Elsman, HIPERFIT, DIKU, Denmark

Title: TBD


A Sustainable Energy Future through Education and Research

Patrik Jansson and Tünde Fülöp have written a short position paper on sustainable energy education and research.

Abstract (introduction)

Sustainable access to energy for a growing population is a global challenge. Our society is dependent on a stable supply of energy; industry (including agriculture, mining, manufacturing and construction), transport and heating can only work if sufficient energy is available. Over 80% of the current global use of energy is based on fossil fuels: oil, coal and gas. In addition to the potentially devastating climate effects of burning two billion years of stored hydrocarbons within a century, fossil fuels will eventually run out and we will be left with less than one fifth of the current energy supply which will clearly not be enough. Thus the energy system of the world will have to change dramatically to replace the fossil fuels with existing and new sustainable sources. This is a major global challenge for mankind.
But it is not only a technological challenge; there are also important political dimensions: we need international agreements, a stable economy and a long-term view (over several decades). The kind of global restructuring needed requires local as well as international agreements. Already now we are facing tensions due to the uneven distribution of energy production (mainly “mining” of oil, coal and gas) and consumption. Access to strategically important regions is causing conflicts and as fossil fuels run scarce, increasing prices may lead to increasing tension. Even if we disregard open conflicts, the sheer size of the energy sector makes it a major force in the global economy and with the uneven distribution of producers and consumers this force is destabilizing. The transformation towards sustainable energy solutions will take decades, so a major political challenge is long-term commitment (over several elections). In democracies this requires a voting population which is aware of the energy problem and willing to support the transition. Policymakers around the world, and their voters, need access to comprehensible and trustworthy information about potential energy sources and ways to change our strong dependence on energy.

Testing versus proving in climate impact research

Another recent paper by Cezar Ionescu and Patrik Jansson is also freely available: Full text + abstract.


Higher-order properties arise naturally in some areas of climate impact research. For example, “vulnerability measures”, crucial in assessing the vulnerability to climate change of various regions and entities, must fulfill certain conditions which are best expressed by quantification over all increasing functions of an appropriate type. This kind of property is notoriously difficult to test. However, for the measures used in practice, it is quite easy to encode the property as a dependent type and prove it correct. Moreover, in scientific programming, one is often interested in correctness “up to implication”: the program would work as expected, say, if one would use real numbers instead of floating-point values. Such counterfactuals are impossible to test, but again, they can be easily encoded as types and proven. We show examples of such situations (encoded in Agda), encountered in actual vulnerability assessments.

Dependently-typed programming in scientific computing: Examples from economic modelling

Cezar Ionescu (at PIK) and Patrik Jansson (me, at Chalmers) have just got a paper accepted which fits in well in the GSS activity.

Pre-print + abstract


Computer simulations are essential in virtually every scientific discipline, even more so in those such as economics or climate change where the ability to make laboratory experiments is limited. Therefore, it is important to ensure that the models are implemented correctly, that they can be re-implemented and that the results can be reproduced. Typically, though, the models are described by a mixture of prose and mathematics which is insufficient for these purposes. We argue that using dependent types allows us to gradually reduce the gap between the mathematical description and the implementation, and we give examples from economic modelling. We discuss the consequences that our incremental approach has on programming style and the requirements it imposes on the dependently-typed programming languages used.