About me

I am a Chancellor's Fellow and Senior Lecturer in the Mathematically Structured Programming Group at the University of Strathclyde.

Before coming to Strathclyde, 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.

Fredrik Nordvall Forsberg

Publications

See fnf.bib for a collection of bibtex entries.

2023

  • C. Kupke, F. Nordvall Forsberg and S. Watters: A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists
    APLAS 2023. The final publication is available at www.springerlink.com.
    Best Paper award.
    Bibtex PDF Agda code
    
      @INPROCEEDINGS{kupkeNordvallForsbergWatters2023freshlists,
        author    = {Kupke, Clemens and Nordvall Forsberg, Fredrik and Watters, Sean},
        title     = {A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists},
        booktitle = {The 21st Asian Symposium on Programming Languages and Systems (APLAS '23)},
        editor    = {Hur, Chung-Kil},
        publisher = {Springer},
        pages     = {135--154},
        year      = {2023},
        doi       = {10.1007/978-981-99-8311-7_7},
      }
  • T. de Jong, N. Kraus, F. Nordvall Forsberg and C. Xu: Set-Theoretic and Type-Theoretic Ordinals Coincide
    LICS 2023.
    Bibtex PDF Agda code
    
      @INPROCEEDINGS{deJongKrausNordvallForsbergXu2023STTTord,
        author    = {de Jong, Tom and Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
        title     = {Set-Theoretic and Type-Theoretic Ordinals Coincide},
        booktitle = {38th Annual {ACM/IEEE} Symposium on Logic in Computer Science (LICS '23)},
        pages     = {1--13},
        publisher = {{IEEE} Computer Society},
        year      = {2023},
        doi       = {10.1109/LICS56636.2023.10175762},
      }
  • N. Kraus, F. Nordvall Forsberg and C. Xu: Type-Theoretic Approaches to Ordinals
    Journal paper in Theoretical Computer Science. Note: David Wärn found a mistake in the proof of Theorem 74, and a strengthening of Theorem 73 in the published version. We have made corrections in the version hosted here.
    Bibtex PDF Agda code
    
      @ARTICLE{KrausNordvallForsbergXu2023ordTT,
        author    = {Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
        title     = {Type-Theoretic Approaches to Ordinals},
        journal   = {Theoretical Computer Science},
        volume    = {957},
        publisher = {Elsevier},
        year      = {2023},
        doi       = {10.1016/j.tcs.2023.113843},
      }
  • C. McBride, G. Nakov and F. Nordvall Forsberg: Measuring with confidence: leveraging expressive type systems for correct-by-construction software
    Invited peer-reviewed submission to a special issue of the journal Acta IMEKO.
    Bibtex PDF
    
      @ARTICLE{McBrideNakovNordvallForsberg2023typesMetrology,
        author  = {McBride, Conor and Nakov, Georgi and Nordvall Forsberg, Fredrik},
        title   = {Measuring with confidence: leveraging expressive type systems for correct-by-construction software},
        journal = {Acta {IMEKO}},
        year    = {2023},
        pages   = {1-5},
        volume  = {12},
        number  = {1},
        doi     = {10.21014/actaimeko.v12i1.1412},
      }

2022

  • G. Nakov and F. Nordvall Forsberg: Quantitative Polynomial Functors
    Post-proceedings of TYPES 2021.
    Bibtex PDF
    
      @INPROCEEDINGS{NakovNordvallForsberg2022qpf,
        author    = {Nakov, Georgi and Nordvall Forsberg, Fredrik},
        title     = {Quantitative Polynomial Functors},
        year      = {2022},
        pages     = {10:1--10:22},
        booktitle = {27th International Conference on Types for Proofs and Programs (TYPES '21)},
        series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
        volume    = {239},
        editor    = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
        publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
        doi       = {10.4230/LIPIcs.TYPES.2021.10},
      }
  • C. McBride and F. Nordvall Forsberg: Type systems for programs respecting dimensions
    Advanced Mathematical and Computational Tools in Metrology and Testing XII.
    Bibtex PDF
    
      @INCOLLECTION{mcBrideNordvallForsberg2022dimensions,
        author    = {McBride, Conor and Nordvall Forsberg, Fredrik},
        title     = {Type systems for programs respecting dimensions},
        booktitle = {Advanced Mathematical and Computational Tools in Metrology and Testing {XII}},
        editor    = {Pavese, Franco and Forbes Alistair and Zhang, Nien-Fan and Chunovkina, Anna},
        publisher = {World Scientific},
        series    = {Advances in Mathematics for Applied Sciences},
        volume    = {90},
        pages     = {331--345},
        year      = {2022},
        doi       = {10.1142/9789811242380_0020},
      }

2021

  • N. Kraus, F. Nordvall Forsberg and C. Xu: Connecting Constructive Notions of Ordinals in Homotopy Type Theory
    MFCS 2021. Extended and improved journal version available above.
    Bibtex PDF Agda code
    
      @INPROCEEDINGS{KrausNordvallForsbergXu2021ordHoTT,
        author    = {Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
        title     = {Connecting Constructive Notions of Ordinals in Homotopy Type Theory},
        booktitle =   {46th International Symposium on Mathematical Foundations of Computer Science (MFCS '21)},
        editor    = {Filippo Bonchi and Simon J. Puglisi},
        publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
        series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
        volume    = {202},
        pages     = {70:1--70:16},
        doi       = {10.4230/LIPIcs.MFCS.2021.70},
        year      = {2021},
      }
  • M. Capucci, N. Ghani, J. Ledent and F. Nordvall Forsberg: Translating Extensive Form Games to Open Games with Agency
    ACT 2021.
    Selected for Distinguished presentation.
    Bibtex PDF
    
      @INPROCEEDINGS{capucciGhaniLedentNordvallForsberg2021extformCGT,
        author    = {Capucci, Matteo and Ghani, Neil and Ledent, J{\'e}r{\'e}my and Nordvall Forsberg, Fredrik},
        title     = {Translating Extensive Form Games to Open Games with Agency},
        booktitle = {Applied Category Theory 2021},
        series    = {Electronic Proceedings in Theoretical Computer Science},
        volume    = {372},
        editor    = {Kohei Kishida},
        pages     = {221--234},
        year      = {2021},
        doi       = {10.4204/EPTCS.372.16},
      }

2020

  • R. Atkey, B. Gavranovic, N. Ghani, C. Kupke, J. Ledent and F. Nordvall Forsberg: Compositional Game Theory, Compositionally
    ACT 2020.
    Bibtex PDF
    
      @INPROCEEDINGS{atkeyGavranovicGhaniKupkeLedentNordvallForsberg2020compcgt,
        author    = {Atkey, Robert and Gavranovi{\'c}, Bruno and Ghani, Neil and Kupke, Clemens and Ledent, J{\'e}r{\'e}my and Nordvall Forsberg, Fredrik},
        title     = {Compositional Game Theory, Compositionally},
        pages     = {198--214},
        booktitle = {3rd International Applied Category Theory Conference (ACT '20)},
        editor    = {Spivak, David I. and Vicary, Jamie},
        series    = {{EPTCS}},
        volume    = {333},
        year      = {2020},
        doi       = {10.4204/EPTCS.333.14},
      }
  • F. Nordvall Forsberg, C. Xu, and N. Ghani: Three Equivalent Ordinal Notation Systems in Cubical Agda
    CPP 2020.
    Bibtex PDF Agda code
    
      @INPROCEEDINGS{NordvallForsbergXu2020ord,
        author    = {Nordvall Forsberg, Fredrik and Xu, Chuangjie and Ghani, Neil},
        title     = {Three Equivalent Ordinal Notation Systems in Cubical Agda},
        booktitle = {9th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs (CPP '20)},
        editor    = {Jasmin Blanchette and Catalin Hritcu},
        publisher = {{ACM}},
        pages     = {172--185}
        year      = {2020},
        doi       = {10.1145/3372885.3373835},
      }

2019

  • N. Ghani, C. Kupke, A. Lambert and F. Nordvall Forsberg: Compositional Game Theory with Mixed Strategies: Probabilistic Open Games Using a Distributive Law
    ACT 2019.
    Bibtex PDF
    
      @INPROCEEDINGS{ghaniKupkelambertNordvallForsberg2019probgames,
        author    = {Ghani, Neil and Kupke, Clemens and Lambert, Alasdair and Nordvall Forsberg, Fredrik},
        title     = {Compositional Game Theory with Mixed Strategies: Probabilistic Open Games Using a Distributive Law},
        booktitle = {Applied Category Theory 2019},
        editor    = {John Baez and Bob Coecke},
        series    = {{EPTCS}},
        volume    = {323},
        pages     = {95--105},
        year      = {2019},
        doi       = {10.4204/EPTCS.323.7},
      }
  • 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},
        volume  = {29},
        number  = {6},
        pages   = {810--827},
        doi     = {10.1017/S0960129518000336},
        year    = {2019},
      }

2018

  • T. Altenkirch, P. Capriotti, G. Dijkstra, N. Kraus and F. Nordvall Forsberg: Quotient Inductive-Inductive Types
    FoSSaCS 2018. The original publication is available at www.springerlink.com. Full version on the arXiv.
    Bibtex PDF
    
      @INPROCEEDINGS{altenkirchCapriottiDijkstraKrausNordvallforsberg2018qiits,
        author  = {Altenkirch, Thorsten and Capriotti, Paolo and Dijkstra, Gabe and Kraus, Nicolai and Nordvall Forsberg, Fredrik},
        title   = {Quotient Inductive-Inductive Types},
        booktitle = {FoSSaCS 2018},
        editor    = {Baier, Christel and Dal Lago, Ugo},
        series    = {Lecture Notes in Computer Science},
        volume    = {10803},
        pages     = {293--310},
        publisher = {Springer},
        year      = {2018},
        doi       = {10.1007/978-3-319-89366-2\_16},
      }
  • D. Ritter, F. Nordvall Forsberg, N. May and S. Rinderle-Ma: Optimization Strategies for Integration Pattern Compositions.
    DEBS 2018. ACM DL Author-ize serviceACM Author-ize version.
    Bibtex PDF
    
      @INPROCEEDINGS{ritterNordvallforsbergMayRinderlema2018optimizationStrategies,
        author    = {Ritter, Daniel and Nordvall Forsberg, Fredrik and May, Norman and Rinderle-Ma, Stefanie},
        title     = {Optimization Strategies for Integration Pattern Compositions},
        booktitle = {Proceedings of the 12th ACM International Conference on Distributed and Event-based Systems (DEBS '18)},
        editor    = {Hinze, Annika and Eyers, David M. and Hirzel, Martin and Weidlich, Matthias and Bhowmik, Sukanya},
        pages     = {88--99},
        doi       = {10.1145/3210284.3210295},
        publisher = {{ACM}},
        year      = {2018},
      }
  • N. Ghani, C. Kupke, A. Lambert and F. Nordvall Forsberg: A Compositional Treatment of Iterated Open Games
    Theoretical Computer Science.
    Bibtex PDF
    
      @ARTICLE{ghaniKupkeLambertNordvallforsberg2018infiniteGames,
        author  = {Ghani, Neil and Kupke, Clemens and Lambert, Alasdair and Nordvall Forsberg, Fredrik},
        title   = {A Compositional Treatment of Iterated Open Games},
        journal = {Theoretical Computer Science},
        doi     = {https://doi.org/10.1016/j.tcs.2018.05.026},
        volume  = {741},
        pages   = {48--57},
        year    = {2018}
      }

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 = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS '17)},
        pages     = {63:1--63:13},
        series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
        year      = {2017},
        volume    = {83},
        editor    = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
        publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
        doi       = {10.4230/LIPIcs.MFCS.2017.63},
      }

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 = {Foundations of Software Science and Computation Structures - 19th International Conference (FoSSaCS '16)},
        editor    = {Jacobs, Bart and L{\"o}ding, Christof},
        series    = {Lecture Notes in Computer Science},
        volume    = {9634},
        pages     = {3--19},
        publisher = {Springer, Heidelberg},
        year      = {2016},
        doi       = {10.1007/978-3-662-49630-5_1},
      }
  • 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},
        doi       = {10.1007/978-3-319-30936-1\_6},
      }

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 = {The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS '15)},
        editor    = {Ghica, Dan R.},
        series    = {Electronic Notes in Theoretical Computer Science},
        volume    = {319},
        pages     = {165--181},
        publisher = {Elsevier},
        year      = {2015},
        doi       = {10.1016/j.entcs.2015.12.011},
      }
  • 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)},
        volume    = {38},
        publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
        editor    = {Thorsten Altenkirch},
        doi       = {10.4230/LIPIcs.TLCA.2015.45},
      }
  • 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 = {Logic, Language, Information, and Computation - 22nd International Workshop (WoLLIC '15)},
        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},
        year      = {2015},
        doi       = {10.1007/978-3-662-47709-0\_7},
      }
  • 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 = {Algebra and Coalgebra in Computer Science - 5th International Conference (CALCO '13)},
         editor    = {Heckel, Reiko and Milius, Stefan},
         series    = {Lecture Notes in Computer Science},
         volume    = {8089},
         pages     = {19--33},
         publisher = {Springer},
         year      = {2013},
         doi       = {10.1007/978-3-642-40206-7\_3},
      }
  • 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 = {28th Annual {ACM/IEEE} Symposium on Logic in Computer Science (LICS '13)},
        publisher = {{IEEE} Computer Society},
        pages     = {243--252},
        year      = {2013},
        doi       = {10.1109/LICS.2013.30},
      }
  • 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 = {Interactive Theorem Proving - 4th International Conference (ITP '13)},
        editor    = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
        series    = {Lecture Notes in Computer Science},
        volume    = {7998},
        pages     = {370--385},
        publisher = {Springer},
        year      = {2013},
        doi       = {10.1007/978-3-642-39634-2\_27},
      }

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},
        doi       = {10.1515/9783110324921.259},
      }

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 = {Algebra and Coalgebra in Computer Science - 4th International Conference (CALCO '11)},
        year      = {2011},
        editor    = {Corradini, Andrea and Klin, Bartek and Cirstea, Corina},
        series    = {Lecture Notes in Computer Science},
        volume    = {6859},
        pages     = {70--84},
        publisher = {Springer},
        doi       = {10.1007/978-3-642-22944-2\_6},
      }

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 = {Computer Science Logic, 24th International Workshop (CSL '10)},
        year      = {2010},
        editor    = {Dawar, Anuj and Veith, Helmut},
        series    = {Lecture Notes in Computer Science},
        volume    = {6247},
        pages     = {454--468},
        publisher = {Springer},
        doi       = {10.1007/978-3-642-15205-4\_35},
      }

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 Tallinn theory seminar Constructive taboos for ordinals.
Tallinn Logic and Semantics Group: CS Theory Seminar, October 2022, online.
Slides
Slide from TYPES 2022 TypOS: An “Operating System” for Typechecking Actors.
TYPES 2022, June 2022, Nantes.
Slides Video
Slide from HOTTEST seminar Different Notions of Ordinals in Homotopy Type Theory.
HOTTEST seminar, March 2022, online.
Slides Video
Shot from TYPES 2021 Functorial adapters.
TYPES 2021, June 2021, online.
Video
Slide from TYPES 2021 Constructive Notions of Ordinals in Homotopy Type Theory.
TYPES 2021, June 2021, online.
Slides Video
Slide from Polynomial Functors Workshop 2021 Quantitative Polynomial Functors.
Workshop on Polynomial Functors, March 2021, Topos Institute.
Slides Video
Slide from LFCS seminar Ordinal notation systems for ordinals below ε0 in modern type theories.
LFCS seminar, February 2020, Edinburgh.
Slides
Slide from TYPES 2019 Compositional Game Theory in Type Theory.
TYPES 2019, June 2019, Oslo.
Slides
Slide from TYPES 2018 Specifying quotient inductive-inductive types.
TYPES 2018, June 2018, Braga.
Slides
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.
Office
LT1312 (floor 13, Livingstone Tower).
Phone
(+44) (0)141 548 3230.
Email
click to reveal (firstname.lastname-lastlastname@strath.ac.uk).

Last modified: Tue Jan 23 08:51:46 GMT 2024.