Dr Fredrik Nordvall Forsberg

Senior Lecturer

Computer and Information Sciences

Contact

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

Professional Activities

Scottish Programming Languages and Verification Summer School 2024
Organiser
29/7/2024
Contributed talk TYPES 2024: "Extensional Finite Sets and Multisets in Type Theory"
Contributor
13/6/2024
Contributed talk TYPES 2024: "Constructive Ordinal Exponentiation in Homotopy Type Theory"
Speaker
13/6/2024
Hausdorff Research Institute for Mathematics
Visiting researcher
26/5/2024
Contributed talk HoTT/UF 2024: "Ordinal exponentiation in homotopy type theory"
Speaker
2/4/2024
TYPES steering committee (External organisation)
Member
2024

More professional activities

Projects

A correct-by-construction approach to approximate computation
Mardare, Radu (Principal Investigator) Nordvall Forsberg, Fredrik (Co-investigator)
01-Nov-2023 - 31-Oct-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-Oct-2021 - 01-Oct-2025
Industrial CASE Account - University of Strathclyde 2021 | Braithwaite, Dylan
Hedges, Julian (Principal Investigator) Nordvall Forsberg, Fredrik (Co-investigator) Braithwaite, Dylan (Research Co-investigator)
01-Oct-2021 - 01-Oct-2025
Maths DTP 2020 University of Strathclyde | Capucci, Matteo
Nordvall Forsberg, Fredrik (Principal Investigator) Hedges, Julian (Co-investigator) Capucci, Matteo (Research Co-investigator)
01-Oct-2020 - 01-Oct-2024
KTP - Cambridge Quantum Computing (CQC) / R190328-202
McBride, Conor (Principal Investigator) Atkey, Bob (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
24-Feb-2020 - 23-Feb-2022
KTP - Cambridge Quantum Computing (CQC)
McBride, Conor (Principal Investigator) Atkey, Bob (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
24-Feb-2020 - 23-Feb-2022

More projects

Back to staff profile

Contact

Dr Fredrik Nordvall Forsberg
Senior Lecturer
Computer and Information Sciences

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