@INPROCEEDINGS{ChenNordvallForsbergTsai2026ttQIIRT,
  author    = {Chen, Liang-Ting and Nordvall Forsberg, Fredrik and Tsai, Tzu-Chun},
  title     = {Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda},
  booktitle = {15th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs (CPP '26)},
  editor    = {Swamy, Nikhil and Tabareau, Nicolas},
  publisher = {{ACM}},
  year      = {2026},
  doi       = {10.1145/3779031.3779090},
}

@INPROCEEDINGS{deJongKrausNordvallForsbergXu2025ordexp,
  author    = {de Jong, Tom and Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
  title     = {Ordinal Exponentiation in Homotopy Type Theory},
  booktitle = {40th Annual {ACM/IEEE} Symposium on Logic in Computer Science (LICS '25)},
  pages     = {262--274}
  publisher = {{IEEE} Computer Society},
  year      = {2025},
  doi       = {10.1109/LICS65433.2025.00027},
}

@ARTICLE{mcBrideNakovNordvallForsbergVidelaForbesLines2024labmate,
  author  = {McBride, Conor and Nakov, Georgi and Nordvall Forsberg, Fredrik and and Forbes, Alistair and Lines, Keith},
  title   = {{LabMate}: a prospectus for types for {MATLAB}},
  journal = {Measurement: Sensors},
  pages   = {101460},
  year    = {2025},
  doi     = {10.1016/j.measen.2024.101460},
}


@ARTICLE{forbesLinesNordvallForsbergMcBrideVidela2024modelstructure,
  author  = {Forbes, Alistair and Lines, Keith and Nordvall Forsberg, Fredrik and McBride, Conor and Videla, Andre},
  title   = {Preserving model structure and constraints in scientific computing},
  journal = {Measurement: Sensors},
  pages   = {101796},
  year    = {2025},
  doi     = {10.1016/j.measen.2024.101796},
}

@ARTICLE{ritterNordvallForsbergRinderleMa2024reco,
  author  = {Ritter, Daniel and Nordvall Forsberg, Fredrik and Rinderle-Ma, Stefanie},
  title   = {Responsible composition and optimization of integration processes under correctness preserving guarantees},
  journal = {Information Systems},
  volume  = {124},
  pages   = {102400},
  year    = {2024},
  doi     = {10.1016/j.is.2024.102400},
}

@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},
}

@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},
}

@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},
}

@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},
  volume  = {12},
  number  = {1},
  pages   = {1--5},
  doi     = {10.21014/actaimeko.v12i1.1412},
}

@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}
}

@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},
  year      = {2021},
  doi       = {10.4230/LIPIcs.MFCS.2021.70},
}

@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 = {4th International Conference on Applied Category Theory (ACT '21)},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {372},
  editor    = {Kohei Kishida},
  pages     = {221--234},
  year      = {2021},
  doi       = {10.4204/EPTCS.372.16},
}

@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},
}

@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 Conference on Applied Category Theory (ACT '20)},
    editor    = {Spivak, David I. and Vicary, Jamie},
    series    = {Electronic Proceedings in Theoretical Computer Science},
    volume    = {333},
    year      = {2020},
    doi       = {10.4204/EPTCS.333.14},
}

@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},
}

@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 = {2nd International Conference on Applied Category Theory (ACT '19)},
  editor    = {John Baez and Bob Coecke},
  series    = {{EPTCS}},
  volume    = {323},
  pages     = {95--105},
  year      = {2019},
  doi       = {10.4204/EPTCS.323.7},
}


@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},
  year    = {2019},
  doi     = {10.1017/S0960129518000336},
}


@INPROCEEDINGS{altenkirchCapriottiDijkstraKrausNordvallforsberg2018qiits,
  author    = {Altenkirch, Thorsten and Capriotti, Paolo and Dijkstra, Gabe and Kraus, Nicolai and Nordvall Forsberg, Fredrik},
  title     = {Quotient Inductive-Inductive Types},
  booktitle = {21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS '18)},
  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},
}

@INPROCEEDINGS{ritterNordvallforsbergMayRinderlema2018optimizationStrategies,
  author    = {Ritter, Daniel and Nordvall Forsberg, Fredrik and May, Norman and Rinderle-Ma, Stefanie},
  title     = {Optimization Strategies for Integration Pattern Compositions},
  booktitle = {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},
  publisher = {{ACM}},
  year      = {2018},
  doi       = {10.1145/3210284.3210295},
}

@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},
  volume  = {741},
  pages   = {48--57},
  year    = {2018},
  doi     = {10.1016/j.tcs.2018.05.026},
}

@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},
}


@INPROCEEDINGS{ghaniNordvallforsbergSimpson2016compParam,
  author    = {Ghani, Neil and Nordvall Forsberg, Fredrik and Simpson, Alex},
  title     = {Comprehensive parametric polymorphism: categorical models and type theory},
  booktitle = {19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS '16)},
  editor    = {Jacobs, Bart and L{\"o}ding, Christof},
  series    = {Lecture Notes in Computer Science},
  volume    = {9634},
  pages     = {3--19},
  publisher = {Springer},
  year      = {2016},
  doi       = {10.1007/978-3-662-49630-5\_1},
}

@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},
  year      = {2016},
  doi       = {10.1007/978-3-319-30936-1\_6},
}

@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 = {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},
}

@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},
  booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA '15)},
  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume    = {38},
  editor    = {Thorsten Altenkirch},
  year      = {2015},
  doi       = {10.4230/LIPIcs.TLCA.2015.45},
}

@INPROCEEDINGS{ghaniNordvallforsbergOrsanigo2015universalForall,
  author    = {Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico},
  title     = {Parametric polymorphism {---} universally},
    booktitle = {22nd International Workshop on Logic, Language, Information, and Computation (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},
}

@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},
}

@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},
}

@PHDTHESIS{nordvallforsberg2013thesis,
  author = {Nordvall Forsberg, Fredrik},
  title  = {Inductive-inductive definitions},
  school = {Swansea University},
  year   = {2013}
}

@INPROCEEDINGS{ghaniMalatestaNordvallforsbergSetzer2013positiveIR,
  author    = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik},
  title     = {Positive Inductive-Recursive Definitions},
  booktitle = {5th International Conference on Algebra and Coalgebra in Computer Science (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},
}

@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},
}

@INPROCEEDINGS{miyamotoNordvallforsbergSchwichtenberg2013nestedPE,
  author    = {Miyamoto, Kenji and Nordvall Forsberg, Fredrik and Schwichtenberg, Helmut},
  title     = {Program Extraction from Nested Definitions},
  booktitle = {4th International Conference on Interactive Theorem Proving (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},
}

@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},
}

@INPROCEEDINGS{altenkirchMorrisNordvallforsbergSetzer2011indindCatsem,
  author    = {Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik and Setzer, Anton},
  title     = {A categorical semantics for inductive-inductive definitions},
  booktitle = {4th International Conference on Algebra and Coalgebra in Computer Science (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},
}

@INPROCEEDINGS{nordvallforsbergSetzer2010inductiveinductive,
  author    = {Nordvall Forsberg, Fredrik and Setzer, Anton},
  title     = {Inductive-Inductive Definitions},
  booktitle = {24th International Workshop on Computer Science Logic (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},
}

@MASTERSTHESIS{nordvallforsberg2009MScthesis,
  author = {Nordvall Forsberg, Fredrik},
  title  = {Constructive aspects of models for non-standard analysis},
  school = {Uppsala University},
  year   = {2009}
}