Ulf Norell

I am a post doc at the Computing Science department at Chalmers.

Contents

• Research
• Papers
• Talks
• Tools
• Teaching
• Contact

Research

Papers

• Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007.
  [ abstract, pdf, bib ]

• Ulf Norell and Catarina Coquand. Type checking in the presence of meta-variables .
  [ abstract, pdf ]

• Andreas Abel, Thierry Coquand and Ulf Norell. Connecting a Logical Framework to a First-Order Logic Prover . In the proceedings of the 5th International Workshop on Frontiers of Combining Systems, FroCoS 2005. Copyright © Springer-Verlag.
  [ abstract, ps, pdf, bib ]

• Andreas Abel, Thierry Coquand and Ulf Norell. Connecting a Logical Framework to a First-Order Logic Prover (Extended Version). Technical report, Departement of Computing Science, Chalmers University of Technology, Gothenburg Sweden, 2005.
  [ abstract, ps, pdf, bib ]

• Ulf Norell. Implementing Functional Generic Programming. Licentiate thesis, Chalmers University of Technology and Göteborg University, 2004.
  [ abstract, ps, pdf, bib ]

• Ulf Norell and Patrik Jansson. Prototyping Generic Programming using Template Haskell. In the proceedings of the Seventh International Conference on Mathematics of Program Construction, MPC 2004. Copyright © Springer-Verlag.
  [ abstract, implementation, talk, ps, pdf, bib ]

• Ulf Norell and Patrik Jansson. Polytypic Programming in Haskell. In the proceedings of the 15th International Workshop on the Implementation of Functional Languages, IFL2003. Copyright © Springer-Verlag.
  [ abstract, implementation, talk, ps, pdf, bib ]

• Ulf Norell. Functional Generic Programming and Type Theory. Master's thesis, Chalmers University of Technology, Computer Science and Engineering, 2002.
  [ abstract, ps, bib ]

Talks

• A Module System for Agda, CHIT-CHAT 2006.
  [slides, abstract]

• Agda II -- Take One, video talk, May 2006.
  [slides, abstract, remarks]

• Prototyping Generic Programming using Template Haskell, MPC 2004.
  [slides]

• Polytypic Programming in Haskell, IFL 2003.
  [slides]

Tools

• AgdaLight, an experimental version of Agda, trying out some new features.

• Agda 2. The latest installment of Agda.

Teaching

Contact information