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.
@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 = {319}, publisher = {Springer, Heidelberg}, year = {2016} }
@INPROCEEDINGS{GhaniNordvallforsbergOrsanigo2016proofRelevantParam, author = {Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico}, title = {Proofrelevant 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 = {109131}, publisher = {Springer, Heidelberg}, year = {2016} }
@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 = {165181}, publisher = {Elsevier}, year = {2015} }
@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 = {4559}, year = {2015}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA'15)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, editor = {Thorsten Altenkirch} }
@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 = {8192}, publisher = {Springer, Heidelberg}, year = {2015} }
@ARTICLE{GhaniMalatestaNordvallforsberg2015posIR, author = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik}, title = {Positive InductiveRecursive Definitions}, journal = {Logical Methods in Computer Science}, volume = {11}, number = {1}, year = {2015}, doi = {10.2168/LMCS11(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/LMCS11(1:6)2015}, }
@PHDTHESIS{nordvallforsberg2013thesis, author = {Nordvall Forsberg, Fredrik}, title = {Inductiveinductive definitions}, school = {Swansea University}, year = {2013} }
@INPROCEEDINGS{GhaniMalatestaNordvallforsbergSetzer2013positiveIR, author = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik}, title = {Positive InductiveRecursive Definitions}, booktitle = {CALCO 2013}, editor = {Heckel, Reiko and Milius, Stefan}, series = {Lecture Notes in Computer Science}, volume = {8089}, pages = {1933}, publisher = {Springer, Heidelberg}, year = {2013} }
@INPROCEEDINGS{GhaniMalatestaNordvallforsbergSetzer2013fibredData, author = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik and Setzer, Anton}, title = {Fibred Data Types}, booktitle = {LICS 2013}, pages = {243252}, year = {2013} }
@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 PaulinMohring, Christine and Pichardie, David}, series = {Lecture Notes in Computer Science}, volume = {7998}, pages = {370385}, publisher = {Springer, Heidelberg}, year = {2013} }
@INCOLLECTION{nordvallforsbergSetzer2012finIndind, author = {Nordvall Forsberg, Fredrik and Setzer, Anton}, title = {A finite axiomatisation of inductiveinductive 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 = {259287} }
@INPROCEEDINGS{altenkirchMorrisNordvallforsbergSetzer2011indindCatsem, author = {Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik and Setzer, Anton}, title = {A categorical semantics for inductiveinductive definitions}, booktitle = {CALCO 2011}, year = {2011}, editor = {Corradini, Andrea and Klin, Bartek and Cirstea, Corina}, series = {Lecture Notes in Computer Science}, volume = {6859}, pages = {7084}, publisher = {Springer, Heidelberg} }
@INPROCEEDINGS{nordvallforsbergSetzer2010inductiveinductive, author = {Nordvall Forsberg, Fredrik and Setzer, Anton}, title = {InductiveInductive Definitions}, booktitle = {CSL 2010}, year = {2010}, editor = {Dawar, Anuj and Veith, Helmut}, series = {Lecture Notes in Computer Science}, volume = {6247}, pages = {454468}, publisher = {Springer, Heidelberg} }
@MASTERSTHESIS{nordvallforsberg2009MScthesis, author = {Nordvall Forsberg, Fredrik}, title = {Constructive aspects of models for nonstandard analysis}, school = {Uppsala University}, year = {2009} }
The encodedecode method in HoTT, relationally. Scottish Theorem Proving Seminar, October 2015, Dundee. [Slides] 

My Summer in Munich: Extracting Haskell Programs. Realizability Seminar, February 2013, Swansea. [Slides] 

Internalising inductiveinductive definitions in MartinLö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 inductiveinductive definitions. CALCO 2011, Winchester, UK. [Slides] 

Interpreting inductiveinductive definitions as indexed inductive definitions. TYPES 2010, Warsaw, Poland. [Slides] 

Formalising inductiveinductive definitions. Invited participant, Program Extraction and Constructive Proofs 2010, Brno, Czech Republic. [Slides] 

Inductiveinductive definitions. BCTCS 2010, Edinburgh, UK. [Abstract] [Slides] 
Last modified: Thu Jan 5 14:46:02 GMT 2017.