Personal profile

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.

Expertise related to UN Sustainable Development Goals

In 2015, UN member states agreed to 17 global Sustainable Development Goals (SDGs) to end poverty, protect the planet and ensure prosperity for all. This person’s work contributes towards the following SDG(s):

  • SDG 4 - Quality Education
  • SDG 8 - Decent Work and Economic Growth
  • SDG 9 - Industry, Innovation, and Infrastructure
  • SDG 12 - Responsible Consumption and Production

Education/Academic qualification

Doctor of Philosophy, Inductive-inductive definitions, Swansea University

Award Date: 1 Jan 2013

Master of Mathematics, Constructive aspects of models for non-standard analysis, Uppsala University

Award Date: 1 Jan 2009


  • type theory
  • constructive mathematics
  • programming languages
  • logic
  • verification
  • correct by construction


Dive into the research topics where Fredrik Nordvall Forsberg is active. These topic labels come from the works of this person. Together they form a unique fingerprint.
  • 1 Similar Profiles

Collaborations and top research areas from the last five years

Recent external collaboration on country/territory level. Dive into details by clicking on the dots or