Fredrik Nordvall Forsberg
Moved to Strathclyde
I have moved to sunny Glasgow and the Mathematically Structured Programming Group at the University of Strathclyde. My new home page can be found here. (The rest of this page is frozen in time; in particular, the list of publications below is out of date.)
PhD Student
I was a PhD student under the supervision of Anton Setzer, working in type theory.
Did you know that forgetting words in a foreign language has a left adjoint? To translate freely.
You can find my CV here.
Seminar series on realizability
More information about the seminar series on realizability here.
Last term, we had a seminar series on categorical logic.
Publications
 PhD thesis: Inductiveinductive definitions
Swansea University, 2013.
[BibTeX] [PDF]  N. Ghani, L. Malatesta and F. Nordvall Forsberg: Positive InductiveRecursive Definitions
Invited paper at CALCO 2013. The original publication is available at www.springerlink.com.
[BibTeX] [PDF]  N. Ghani, L. Malatesta, F. Nordvall Forsberg and A. Setzer: Fibred Data Types
LICS 2013.
[BibTeX] [PDF]  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]  F. Nordvall Forsberg, A. Setzer: A finite axiomatisation of inductiveinductive definitions
In Logic, Construction, Computation.
[BibTeX] [PDF]  T. Altenkirch, P. Morris, F. Nordvall Forsberg, A. Setzer: A categorical semantics for inductiveinductive definitions
CALCO 2011. The original publication is available at www.springerlink.com.
[BibTeX] [PDF]  F. Nordvall Forsberg, A. Setzer: Inductiveinductive definitions
CSL 2010. The original publication is available at www.springerlink.com.
[BibTeX] [PDF] [Extended version and Agda development]  Magister thesis: Constructive aspects of models for
nonstandard analysis
U.U.D.M. Project report 2009:10, Uppsala University, 2009.
[BibTeX] [PDF]
Selected talks
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] 