Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Ulf Norell
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.
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.
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
(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.
Functional Generic Programming and Type Theory.
Master's thesis, Chalmers University of Technology, Computer
Science and Engineering, 2002.
[ abstract,
ps,
bib
]
Talks
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]