Ulf Norell

I am a postdoc at the Computing Science department
at Chalmers.
Contents
Research
My research interests are interactive theorem proving and dependently
typed programming using type theory. In particular the design and
implementation of systems supporting these activities. I am a member
of the Programming Logic
and the Functional
Programming groups.
Papers
- Ana Bove, Peter Dybjer and Ulf Norell.
A Brief Overview of Agda -- A Functional Language with Dependent Types.
In the proceedings of TPHOLs 2009. Copyright © Springer Verlag.
[ pdf
, highlighted code
]
- Nils Anders Danielsson and Ulf Norell.
Structurally Recursive Descent Parsing.
Draft, 2008.
[
abstract
,
pdf
,
code
,
highlighted code
]
- Nils Anders Danielsson and Ulf Norell.
Parsing Mixfix Operators.
Accepted for publication in the proceedings of the 20th
International Symposium on the Implementation and Application of
Functional Languages
(IFL 2008).
[
abstract
,
pdf
,
code
,
highlighted code
]
- Ulf Norell.
Dependently Typed Programming in Agda.
Accepted for publication in the lecture notes from the summer school on
Advanced Functional Programming, 2008.
Copyright © Springer-Verlag.
[ pdf ]
- 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
. Draft, 2007.
[ 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
- Interactive Programming with Dependent Types, ICFP 2013.
[code (pretty), ICFP.agda, ICFPPrelude.agda]
- Playing with Agda, Agda tutorial at TPHOLs 2009
[code]
- Dependently Typed Programming in Agda, invited talk at TLDI 2009.
[abstract,
slides
]
- 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]
Agda
Teaching
Contact information
Phone (office): | +46 (0)31 772 10 54 |
Phone (mobile): | +46 (0)703 767 810 |
Room: | 6466 (EDIT building) |
Email: | ulfn@chalmers.se |
Disclaimer
Last modified: Wed Sep 25 23:41:42 2013