Category Archives: GSDP

GSDP Podcasts

GSDP Podcasts

We interviewed many experts including researchers, scientists and professionals to explore the role of global system science (GSS) in addressing many issues that society is facing today and in the future. Specially we are interested in how GSS can help shape better policy making and ways to communicate complex systems thinking to the general public and policy makers. Thanks to all of the interview participants who brought a wide range of perspectives to the conversation.

The series of interviews can now be found on this blog!

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:

http://wiki.portal.chalmers.se/cse/pmwiki.php/GSDP/GSSLanguages

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

Welcome,

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

 

Candidate “definition” of GSS

As part of the Models and Data workshop we were asked to “define GSS in one sentence”. This was my contribution:

Testing versus proving in climate impact research

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

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

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.