Patrik Jansson

Professor of Computer Science


Curriculum vitae



+46317725415


Computer Science and Engineering

Chalmers University of Technology

Room number: EDIT-6452
My office is in the EDIT building of campus Johanneberg, near Rännvägen 6.



FPClimate seminar 2


April 08, 2024

A short description of the second seminar of the FPClimate course. The first seminar has its own blog post.

Lecture (slides, source) by Prof. Cezar Ionescu

  • about Vulnerability Modelling with Functional Programming and Dependent Types

    • (Prof. Ionescu very sadly passed away after severe illness in October 2024.)
  • Background: Algebra of Programming (the book, by Richard Bird and Ooge de Moor)

    • Category theory is an extensible language for precisely formulating mathematical theories (concepts, models, etc.).
    • One such extension is particularly well-suited for formulating functional programs.
    • Further extensions allow us to formulate specifications.
    • There are other frameworks with similar properties: higher-order logics (dependent types), Hoare logics, etc.
    • The categorical framework is good for equational reasoning.
  • Potsdam Institute for Climate Impact Research (PIK)

  • Vulnerability modelling [the paper this seminar is about]

    • Motivated by a surge in "Vulnerability assessment" work in the climate change community.
    • Cezar's paper first submitted in 2010, published 2014, Journal version 2016!
    • ["Vulnerability Modelling with Functional Programming and Dependent Types"(doi:10.1017/S0960129514000139) [Ionescu, 2016] <doi:10.1017/S0960129514000139>
  • Definitions of Vulnerability

    • There were many attempts at defining "vulnerability" around 2000
    • [Thywissen 2006]lists 36 definitions!
  • The Structure of Vulnerability (according to [Ionescu, 2016]) Illustrated by the following Haskell code:

    possible       ::  Functor f => State -> f Evolution
    harm           ::  Preorder v => Evolution -> v
    measure        ::  Functor f, Preorder v, Preorder w => f v -> w
    vulnerability  ::  Preorder w => State -> w
    vulnerability  =   measure . fmap harm . possible

- The paper presents a few examples which fit this structure.

  • Vulnerability measures

    • should be monotonic
    • can be related by natural transformations between representations of possibility
    • should be "compatible\"
  • Next stage: dependent types

    • (under the influence of Patrik Jansson)
    • moving the categorical machinery to the new framework
  • Conclusions

    • Main idea: formulate problems as programming correctness problems!
    • This can be useful in contexts where simulation is used to replace experiments (climate science, social science, political theory, etc.).
    • Type theory can formulate both correctness conditions and the programs themselves.
    • Moreover, the correctness proofs are then mechanically checked.


Share

Tools
Translate to