1 Search Results for "Jansson, Patrik"

Testing versus proving in climate impact research

Authors: Cezar Ionescu and Patrik Jansson

Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)

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.

Cite as

Cezar Ionescu and Patrik Jansson. Testing versus proving in climate impact research. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 41-54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

  author =	{Ionescu, Cezar and Jansson, Patrik},
  title =	{{Testing versus proving in climate impact research}},
  booktitle =	{18th International Workshop on Types for Proofs and Programs (TYPES 2011)},
  pages =	{41--54},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-49-1},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{19},
  editor =	{Danielsson, Nils Anders and Nordstr\"{o}m, Bengt},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.41},
  URN =		{urn:nbn:de:0030-drops-38991},
  doi =		{10.4230/LIPIcs.TYPES.2011.41},
  annote =	{Keywords: dependently-typed programming, domain-specific languages, climate impact research, formalization}
  • Refine by Author
  • 1 Ionescu, Cezar
  • 1 Jansson, Patrik

  • Refine by Classification

  • Refine by Keyword
  • 1 climate impact research
  • 1 dependently-typed programming
  • 1 domain-specific languages
  • 1 formalization

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2013

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail