I am a 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.
@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 = {https://doi.org/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},
pages = {1-5},
volume = {12},
number = {1},
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},
}
@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{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},
}
@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},
}
@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},
}
@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 = {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},
}
@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},
}
@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},
}
ACM Author-ize version.
@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},
}
@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}
}
@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 = {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},
}
@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},
}
@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},
}
@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},
}
@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},
}
@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 = {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},
}
@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 = {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},
}
@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 = {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},
}
@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},
}
@MASTERSTHESIS{nordvallforsberg2009MScthesis,
author = {Nordvall Forsberg, Fredrik},
title = {Constructive aspects of models for non-standard analysis},
school = {Uppsala University},
year = {2009}
}
|
The ordinals in set theory and type theory are the same. TYPES 2023, June 2023, Valencia. Slides Video |
|
Constructive taboos for ordinals. Tallinn Logic and Semantics Group: CS Theory Seminar, October 2022, online. Slides |
|
TypOS: An “Operating System” for Typechecking Actors. TYPES 2022, June 2022, Nantes. Slides Video |
|
Different Notions of Ordinals in Homotopy Type Theory. HOTTEST seminar, March 2022, online. Slides Video |
|
Functorial adapters. TYPES 2021, June 2021, online. Video |
|
Constructive Notions of Ordinals in Homotopy Type Theory. TYPES 2021, June 2021, online. Slides Video |
|
Quantitative Polynomial Functors. Workshop on Polynomial Functors, March 2021, Topos Institute. Slides Video |
|
Ordinal notation systems for ordinals below ε0 in modern type theories. LFCS seminar, February 2020, Edinburgh. Slides |
|
Compositional Game Theory in Type Theory. TYPES 2019, June 2019, Oslo. Slides |
|
Specifying quotient inductive-inductive types. TYPES 2018, June 2018, Braga. Slides |
|
Variations on inductive-recursive definitions. Agda Implementors' Meeting XXV, May 2017, Gothenburg. Slides |
|
Comprehensive parametric polymorphism. LFCS seminar, May 2016, Edinburgh. Slides |
|
The encode-decode method in HoTT, relationally. Scottish Theorem Proving Seminar, October 2015, Dundee. Slides |
|
Inductive-inductive definitions in Intuitionistic Type Theory. Stockholm Logic seminar, June 2014, Stockholm. Slides |
|
My Summer in Munich: Extracting Haskell Programs. Realizability Seminar, February 2013, Swansea. Slides |
|
Internalising inductive-inductive definitions in Martin-Löf Type Theory. TCS Oberseminar, November 2012, LMU Institut für Informatik, Munich, Germany. Slides |
|
Elimination principles for initial dialgebras. TYPES 2011, Bergen, Norway. Slides |
|
A categorical semantics for inductive-inductive definitions. CALCO 2011, Winchester, UK. Slides |
|
Interpreting inductive-inductive definitions as indexed inductive definitions. TYPES 2010, Warsaw, Poland. Slides |
Last modified: Mon Nov 4 10:54:04 GMT 2024.