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.

Back to staff profile


A fresh look at commutativity : free algebraic structures via fresh lists
Kupke Clemens, Nordvall Forsberg Fredrik, Watters Sean
The 21st Asian Symposium on Programming Languages and Systems, pp. 1-20 (2023)
Set-theoretic and type-theoretic ordinals coincide
de Jong Tom, Kraus Nicolai, Nordvall Forsberg Fredrik, Xu Chuangjie
Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (2023)
Type-theoretic approaches to ordinals
Kraus Nicolai, Nordvall Forsberg Fredrik, Xu Chuangjie
Theoretical Computer Science Vol 957 (2023)
Measuring with confidence : leveraging expressive type systems for correct-by-construction software
McBride Conor, Nakov Georgi, Nordvall Forsberg Fredrik
Acta IMEKO Vol 12 (2023)
Infinite horizon extensive form games, coalgebraically
Capucci Matteo, Ghani Neil, Kupke Clemens, Ledent Jérémy, Nordvall Forsberg Fredrik
Mathematics for Computation (2023) (2023)
Quantitative polynomial functors
Nakov Georgi, Nordvall Forsberg Fredrik
27th International Conference on Types for Proofs and Programs (TYPES 2021) Leibniz International Proceedings in Informatics, LIPIcs Vol 239, pp. 10:1--10:22 (2022)

More publications

Back to staff profile

Professional Activities

Contributed talk HoTT/UF 2024: "Ordinal exponentiation in homotopy type theory"
Scottish Programming Languages Seminar Series
Contributed talk TYPES 2023: The ordinals in set theory and type theory are the same
SPLS seminar: Set theory or type theory? It doesn't matter! (For ordinals)
Contributed talk HoTT 2023: Relating ordinals in set theory to ordinals in type theory
Contributed talk CIRM: The set-theoretic and type-theoretic ordinals are the same

More professional activities


A correct-by-construction approach to approximate computation
Mardare, Radu (Principal Investigator) Ghani, Neil (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
01-Jan-2023 - 31-Jan-2027
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) / R190328-202
McBride, Conor (Principal Investigator) Atkey, Bob (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
24-Jan-2020 - 23-Jan-2022
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
Trusted Systems
Ghani, Neil (Principal Investigator) McBride, Conor (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
01-Jan-2019 - 30-Jan-2023

More projects

Back to staff profile


Dr Fredrik Nordvall Forsberg
Strathclyde Chancellor's Fellow
Computer and Information Sciences

Email: fredrik.nordvall-forsberg@strath.ac.uk
Tel: 548 3230