Research Associate

I am a postdoc in the Mathematically Structured Programming Group at the University of Strathclyde, working with Neil Ghani.

Before that, I was a postdoc in the Theory Group at the University of Birmingham, working with Dan Ghica. Before that, I did a PhD at Swansea University under the supervision of Anton Setzer.

I have a CV.

Publications

2017

  • N. Ghani, F. Nordvall Forsberg and F. Orsanigo: Universal properties for universal types in bifibrational parametricity
    Journal paper in MSCS.
    Bibtex PDF
    
      @ARTICLE{ghaniNordvallforsbergOrsanigo2017universalUniversal,
        author  = {Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico},
        title   = {Universal properties for universal types in bifibrational parametricity},
        journal = {Mathematical Structures in Computer Science},
        year    = {2017}
      }
  • N. Ghani, C. McBride, F. Nordvall Forsberg and S. Spahn: Variations on inductive-recursive definitions
    MFCS 2017.
    Bibtex PDF Agda development
    
      @INPROCEEDINGS{ghaniMcBrideNordvallforsbergSpahn2017variationsIR,
        author    = {Ghani, Neil and McBride, Conor and Nordvall Forsberg, Fredrik and Spahn, Stephan},
        title     = {Variations on inductive-recursive definitions},
        booktitle = {MFCS 2017},
        editor    = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
        series    = {LIPIcs},
        volume    = {83},
        publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
        year      = {2017}
      }

2016

  • N. Ghani, F. Nordvall Forsberg and A. Simpson: Comprehensive parametric polymorphism: categorical models and type theory
    FoSSaCS 2016. The original publication is available at www.springerlink.com.
    EATCS Best ETAPS Theory paper award, Computing Reviews 21st Annual Best of Computing List
    Bibtex PDF
    
      @INPROCEEDINGS{ghaniNordvallforsbergSimpson2016compParam,
        author    = {Ghani, Neil and Nordvall Forsberg, Fredrik and Simpson, Alex},
        title     = {Comprehensive parametric polymorphism: categorical models and type theory},
        booktitle = {FoSSaCS 2016},
        editor    = {Jacobs, Bart and L{\"o}ding, Christof},
        series    = {Lecture Notes in Computer Science},
        volume    = {9634},
        pages     = {3--19},
        publisher = {Springer, Heidelberg},
        year      = {2016}
      }
  • N. Ghani, F. Nordvall Forsberg and F. Orsanigo: Proof-relevant parametricity
    WadlerFest 2016. The original publication is available at www.springerlink.com.
    Bibtex PDF
    
      @INPROCEEDINGS{ghaniNordvallforsbergOrsanigo2016proofRelevantParam,
        author    = {Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico},
        title     = {Proof-relevant parametricity},
        booktitle = {A List of Successes That Can Change the World},
        editor    = {Lindley, Sam and McBride, Conor and Sannella, Don and Trinder, Phil},
        series    = {Lecture Notes in Computer Science},
        volume    = {9600},
        pages     = {109--131},
        publisher = {Springer, Heidelberg},
        year      = {2016}
      }

2015

  • N. Ghani, P. Johann, F. Nordvall Forsberg, F. Orsanigo and T. Revell: Bifibrational functorial semantics of parametric polymorphism
    MFPS XXXI.
    Bibtex PDF
    
      @INPROCEEDINGS{ghaniJohannNordvallforsbergOrsanigoRevell2015bifibParam,
        author    = {Ghani, Neil and Johann, Patricia and Nordvall Forsberg, Fredrik and Orsanigo, Federico and Revell, Timothy},
        title     = {Bifibrational functorial semantics of parametric polymorphism},
        booktitle = {MFPS 2015},
        editor    = {Ghica, Dan R.},
        series    = {Electronic Notes in Theoretical Computer Science},
        volume    = {319},
        pages     = {165--181},
        publisher = {Elsevier},
        year      = {2015}
      }
  • R. Atkey, N. Ghani, F. Nordvall Forsberg, T. Revell and S. Staton: Models for Polymorphism over Physical Dimensions
    TLCA 2015.
    Bibtex PDF
    
      @INPROCEEDINGS{atkeyGhaniNordvallforsbergRevellStaton2015dimensionModels,
        title     = {Models for Polymorphism over Physical Dimensions},
        author    = {Atkey, Robert and Ghani, Neil and Nordvall Forsberg, Fredrik and Revell, Timothy and Staton, Sam},
        pages     = {45--59},
        year      = {2015},
        booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA'15)},
        series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
        editor    = {Thorsten Altenkirch}
      }
  • N. Ghani, F. Nordvall Forsberg and F. Orsanigo: Parametric polymorphism — universally
    WoLLIC 2015. The original publication is available at www.springerlink.com, but the type-setting there has been butchered by Springer. (Extended and improved journal version available above.)
    Bibtex PDF
    
      @INPROCEEDINGS{ghaniNordvallforsbergOrsanigo2015universalForall,
        author    = {Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico},
        title     = {Parametric polymorphism {---} universally},
        booktitle = {WoLLIC 2015},
        editor    = {de Paiva, Valeria and de Queiroz, Ruy and Moss, Lawrence S. and Leivant, Daniel and de Oliveira, Anjolina G.},
        series    = {Lecture Notes in Computer Science},
        volume    = {9160},
        pages     = {81--92},
        publisher = {Springer, Heidelberg},
        year      = {2015}
      }
  • N. Ghani, L. Malatesta and F. Nordvall Forsberg: Positive Inductive-Recursive Definitions
    Journal paper in LMCS.
    Bibtex PDF Agda development
    
      @ARTICLE{ghaniMalatestaNordvallforsberg2015posIR,
         author    = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik},
         title     = {Positive Inductive-Recursive Definitions},
         journal   = {Logical Methods in Computer Science},
         volume    = {11},
         number    = {1},
         year      = {2015},
         doi       = {10.2168/LMCS-11(1:13)2015},
      }
  • U. Berger, A. Lawrence, F. Nordvall Forsberg and M. Seisenberger: Extracting verified decision procedures: DPLL and Resolution
    Journal paper in LMCS.
    Bibtex PDF
    
      @ARTICLE{bergerLawrenceNordvallforsbergSeisenberger2015extractingDPLL,
         author    = {Berger, Ulrich and Lawrence, Andrew and Nordvall Forsberg, Fredrik and Seisenberger, Monika},
         title     = {Extracting verified decision procedures: {DPLL} and Resolution},
         journal   = {Logical Methods in Computer Science},
         volume    = {11},
         number    = {1},
         year      = {2015},
         doi       = {10.2168/LMCS-11(1:6)2015},
      }

2014

  • PhD thesis: Inductive-inductive definitions
    Swansea University, submitted November 2013.
    Bibtex PDF
    
      @PHDTHESIS{nordvallforsberg2013thesis,
         author    = {Nordvall Forsberg, Fredrik},
         title     = {Inductive-inductive definitions},
         school    = {Swansea University},
         year      = {2013}
      }

2013

  • N. Ghani, L. Malatesta and F. Nordvall Forsberg: Positive Inductive-Recursive Definitions
    Invited paper at CALCO 2013. The original publication is available at www.springerlink.com. (Extended and improved journal version available above.)
    Bibtex PDF
    
      @INPROCEEDINGS{ghaniMalatestaNordvallforsbergSetzer2013positiveIR,
         author    = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik},
         title     = {Positive Inductive-Recursive Definitions},
         booktitle = {CALCO 2013},
         editor    = {Heckel, Reiko and Milius, Stefan},
         series    = {Lecture Notes in Computer Science},
         volume    = {8089},
         pages     = {19--33},
         publisher = {Springer, Heidelberg},
         year      = {2013}
      }
  • N. Ghani, L. Malatesta, F. Nordvall Forsberg and A. Setzer: Fibred Data Types
    LICS 2013.
    Bibtex PDF
    
      @INPROCEEDINGS{ghaniMalatestaNordvallforsbergSetzer2013fibredData,
        author    = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik and Setzer, Anton},
        title     = {Fibred Data Types},
        booktitle = {LICS 2013},
        pages     = {243--252},
        year      = {2013}
      }
  • K. Miyamoto, F. Nordvall Forsberg, H. Schwichtenberg: Program extraction from nested definitions
    ITP 2013. The original publication is available at www.springerlink.com.
    Bibtex PDF
    
      @INPROCEEDINGS{miyamotoNordvallforsbergSchwichtenberg2013nestedPE,
        author    = {Miyamoto, Kenji and Nordvall Forsberg, Fredrik and Schwichtenberg, Helmut},
        title     = {Program Extraction from Nested Definitions},
        booktitle = {ITP 2013},
        editor    = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
        series    = {Lecture Notes in Computer Science},
        volume    = {7998},
        pages     = {370--385},
        publisher = {Springer, Heidelberg},
        year      = {2013}
      }

2012

  • F. Nordvall Forsberg, A. Setzer: A finite axiomatisation of inductive-inductive definitions
    In Logic, Construction, Computation.
    Bibtex PDF
    
      @INCOLLECTION{nordvallforsbergSetzer2012finIndind,
        author    = {Nordvall Forsberg, Fredrik and Setzer, Anton},
        title     = {A finite axiomatisation of inductive-inductive definitions},
        booktitle = {Logic, Construction, Computation},
        publisher = {Ontos Verlag},
        year      = {2012},
        editor    = {Berger, Ulrich and Diener Hannes and  Schuster, Peter and Seisenberger, Monika},
        volume    = {3},
        series    = {Ontos mathematical logic},
        pages     = {259--287}
      }

2011

  • T. Altenkirch, P. Morris, F. Nordvall Forsberg, A. Setzer: A categorical semantics for inductive-inductive definitions
    CALCO 2011. The original publication is available at www.springerlink.com.
    Bibtex PDF
    
      @INPROCEEDINGS{altenkirchMorrisNordvallforsbergSetzer2011indindCatsem,
        author    = {Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik and Setzer, Anton},
        title     = {A categorical semantics for inductive-inductive definitions},
        booktitle = {CALCO 2011},
        year      = {2011},
        editor    = {Corradini, Andrea and Klin, Bartek and Cirstea, Corina},
        series    = {Lecture Notes in Computer Science},
        volume    = {6859},
        pages     = {70--84},
        publisher = {Springer, Heidelberg}
      }

2010

  • F. Nordvall Forsberg, A. Setzer: Inductive-inductive definitions
    CSL 2010. The original publication is available at www.springerlink.com.
    Bibtex PDF
    
      @INPROCEEDINGS{nordvallforsbergSetzer2010inductiveinductive,
        author    = {Nordvall Forsberg, Fredrik and Setzer, Anton},
        title     = {Inductive-Inductive Definitions},
        booktitle = {CSL 2010},
        year      = {2010},
        editor    = {Dawar, Anuj and Veith, Helmut},
        series    = {Lecture Notes in Computer Science},
        volume    = {6247},
        pages     = {454--468},
        publisher = {Springer, Heidelberg}
      }

2009

  • Magister thesis: Constructive aspects of models for non-standard analysis
    U.U.D.M. Project report 2009:10, Uppsala University, 2009.
    Bibtex PDF
    
      @MASTERSTHESIS{nordvallforsberg2009MScthesis,
        author = {Nordvall Forsberg, Fredrik},
        title  = {Constructive aspects of models for non-standard analysis},
        school = {Uppsala University},
        year   = {2009}
      }

Selected talks

Slide from AIM Variations on inductive-recursive definitions.
Agda Implementors' Meeting XXV, May 2017, Gothenburg.
Slides
Slide from LFCS seminar Comprehensive parametric polymorphism.
LFCS seminar, May 2016, Edinburgh.
Slides
Slide from STP The encode-decode method in HoTT, relationally.
Scottish Theorem Proving Seminar, October 2015, Dundee.
Slides
Slide from STP Inductive-inductive definitions in Intuitionistic Type Theory.
Stockholm Logic seminar, June 2014, Stockholm.
Slides
Slide from Realisability seminar My Summer in Munich: Extracting Haskell Programs.
Realizability Seminar, February 2013, Swansea.
Slides
Slide from LMU 2012 Internalising inductive-inductive definitions in Martin-Löf Type Theory.
TCS Oberseminar, November 2012, LMU Institut für Informatik, Munich, Germany.
Slides
Slide from TYPES 2011 Elimination principles for initial dialgebras.
TYPES 2011, Bergen, Norway.
Slides
Slide from CALCO 2011 A categorical semantics for inductive-inductive definitions.
CALCO 2011, Winchester, UK.
Slides
Title slide TYPES 2010 Interpreting inductive-inductive definitions as indexed inductive definitions.
TYPES 2010, Warsaw, Poland.
Slides

Contact

Address
Computer & Information Sciences, Livingstone Tower, 26 Richmond Street, Glasgow, G1 1XH, UK.
Phone
(+44) (0)7787 959866.
Email
click to reveal (firstname.lastname-lastlastname@strath.ac.uk).

Last modified: Thu Sep 7 12:25:36 BST 2017.