Dr Fredrik Nordvall Forsberg

Strathclyde Chancellor's Fellow

Computer and Information Sciences

Personal statement

I am a Chancellor's Fellow in the Department of Computer and Information Sciences and a member of the  Mathematically Structured Programming group.

My goal is to understand the underlying logic and structure behind programming languages, and to use this understanding to make it easier to write correct software. To do so, I use and create techniques and tools from mathematical logic, type theory, and category theory. My research interests include:

  • data types in type theory: how can we give semantics of different classes of data types? Is one class more powerful than another? I have developed initial algebra semantics to answer such questions for inductive-inductive definitions, and quotient inductive types from homotopy type theory.
  • correct-by-construction programming: how can we get machines to help humans write the correct program? I create programming languages that make it possible to specify the meaning of programs in their type. This creates new challenges, such as extending the equational theory of programs while retaining decidable type checking, strong normalisation, and canonicity.
  • constructive mathematics and logic: how can we prove theorems and develop mathematical theories that are suitable for implementation in a computer? I am interested both in mathematical developments themselves, such as the theory of a constructive treatments of ordinals, as well as metamathematical investigations into categorical model theory and nonderivability results.
  • applied category theory: how can we describe and build large systems from smaller components? I am working to make this possible in the fields of economic game theory, and for business process languages, by using ideas and techniques from monoidal category theory.

See also my personal web page.

Publications

Connecting constructive notions of ordinals in homotopy type theory
Nordvall Forsberg Fredrik, Xu Chuangjie, Kraus Nicolai
46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021) 46th International Symposium on Mathematical Foundations of Computer Science, pp. 42:1-42:16 (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.42
Translating extensive form games to open games with agency
Capucci Matteo, Ghani Neil, Ledent Jérémy, Nordvall Forsberg Fredrik
Applied Category Theory 2021 (2021)
Type systems for programs respecting dimensions
McBride Conor, Nordvall Forsberg Fredrik
Advanced Mathematical and Computational Tools in Metrology and Testing XII (2021) (2021)
Compositional Game Theory, compositionally
Atkey Robert, Gavranović Bruno, Ghani Neil, Kupke Clemens, Ledent Jérémy, Nordvall Forsberg Fredrik
Applied Category Theory 2020 (2020)
Three equivalent ordinal notation systems in cubical Agda
Nordvall Forsberg Fredrik, Xu Chuangjie, Ghani Neil
CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pp. 172–185 (2020)
https://doi.org/10.1145/3372885.3373835
Compositional game theory with mixed strategies : probabilistic open games using a distributive law
Ghani Neil, Kupke Clemens, Lambert Alasdair, Nordvall Forsberg Fredrik
Applied category theory conference 2019, pp. 1-12 (2019)

More publications

Professional activities

Nottingham FP Lunch: "Functorial adapters in bidirectional type systems"
Invited speaker
23/4/2021
Budapest Type Theory Seminar: "Quantitative type theory and data types"
Invited speaker
31/3/2021
Topos Institute Workshop on Polynomial Functors
Keynote/plenary speaker
19/3/2021
LFCS Seminar: "Ordinal notation systems for ordinals below ε0 in modern type theories"
Invited speaker
4/2/2020
Foundations and Applications of Univalent Mathematics
Keynote/plenary speaker
20/12/2019
External examiner for Jakob von Raumer's PhD
Examiner
6/12/2019

More professional activities

Projects

Maths DTP 2021/22 University of Strathclyde | Watters, Sean
Kupke, Clemens (Principal Investigator) Nordvall Forsberg, Fredrik (Co-investigator) Watters, Sean (Research Co-investigator)
01-Jan-2021 - 01-Jan-2025
KTP - Cambridge Quantum Computing (CQC)
McBride, Conor (Principal Investigator) Atkey, Bob (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
24-Jan-2020 - 23-Jan-2022
Trusted Systems
Ghani, Neil (Co-investigator) McBride, Conor (Principal Investigator) Nordvall Forsberg, Fredrik (Co-investigator)
01-Jan-2019 - 30-Jan-2023

More projects

Address

Computer and Information Sciences
Livingstone Tower

Location Map

View University of Strathclyde in a larger map