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.
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.
Notes from The Saturday ICT workshop (by Patrik Jansson, 2012-11-22)
(Ilan Chabay started out with a summary of the Thursday and Friday Narratives workshops – that part is reported elsewhere.)
Second topic was introduced by Jeremy Gibbons. We need robust modelling – we cannot assume a single shared context. Even for a long-lived single-person project, but more urgently for larger collaborations. We need assumptions to be explicit, documented, transparent, checkable. Challenge 1: make computational science results transparent and repeatable. Challenge 2: provide languages which let you write a high-level model of your program and let the computer generate the low-level code.
Third Michael Resch talked about “Verification and Validation of Simulation Models”. There is a chain (or tower) of models from theory, through modelling, numeric modelling (like discretization), programming, running and interpreting the results. To be sure about the validity of the results we need Challenge 3: validation and verification at each step (each level). This is a major challenge with many sub-parts. If we carefully explain all the potential “bugs” which could in principle invalidate our results we could easily project the image that “they have no credibility”. Thus there is the pedagogical Challenge 4: how to present results with uncertainties? There is also a historical dimension as science moves forward and consensus changes (due to improvements of theory, models and data). Journalists dig up old results (which we now know are incorrect) and make headlines based on the “contradictions” found.
Last discussion topic was introduced by David De Roure: “Knowledge Infrastructure for Global Systems Science”. This comes back to the transparency and repeatability (and multiple meanings of that) mentioned by Jeremy. The main message was that methods are as important as the data. Bundles of workflows, documents and data make up “computational research objects”. An important Challenge 5 here is how to represent these research objects so that they can be mixed and matched freely. Some support for automatic curation and repair would also be needed.
Saturday ICT chairs + presenters
- Patrik Jansson – Chalmers Univ. of Techn., firstname.lastname@example.org
- Co-chair of “Models and Narratives in GSS”
- Ilan Chabay
- Co-chair and talk: “Models and Narratives in Global Systems Science”
- Jeremy Gibbons
- Talk: Dependable Modelling
- Michael Resch
- Talk: Verification and Validation of Simulation Models
- David De Roure;
- Talk: “Knowledge Infrastructure for Global Systems Science”
- Ulf Dahlsten (first hour)
- Ralph Dum
- David Tabara
- several others (unfortunately I did not make a list)