Sökning: id:"swepub:oai:research.chalmers.se:fd4a33f2-25c5-49b8-b279-7ac5c3fdfed2" >
Testing versus prov...
Testing versus proving in climate impact research
-
Ionescu, Cezar (författare)
-
- Jansson, Patrik, 1972 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- ISBN 9783939897491
- 2013
- 2013
- Engelska.
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783939897491 ; 19, s. 41-54
- Relaterad länk:
-
http://publications.... (primary) (free)
-
visa fler...
-
https://research.cha...
-
https://doi.org/10.4...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Software Engineering (hsv//eng)
- NATURVETENSKAP -- Geovetenskap och miljövetenskap -- Klimatforskning (hsv//swe)
- NATURAL SCIENCES -- Earth and Related Environmental Sciences -- Climate Research (hsv//eng)
Nyckelord
- dependently-typed programming
- formalization
- climate impact research
- domain-specific languages
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas