Polytypic Programming in Haskell. - Ulf Norell; Patrik Jansson (IFL, 2003)

Prototyping Generic Programming in Template Haskell. - Ulf Norell; Patrik Jansson (MPC, 2004)

Connecting a Logical Framework to a First-Order Logic Prover. - Andreas Abel 001; Thierry Coquand; Ulf Norell (FroCoS, 2005)

Verifying haskell programs using constructive type theory. - Andreas Abel 001; Marcin Benke; Ana Bove; John Hughes 001; Ulf Norell (Haskell, 2005)

Parsing Mixfix Operators. - Nils Anders Danielsson; Ulf Norell (IFL, 2008)

Dependently typed programming in Agda. - Ulf Norell (TLDI, 2009)

A Brief Overview of Agda - A Functional Language with Dependent Types. - Ana Bove; Peter Dybjer; Ulf Norell (TPHOLs, 2009)

Using temporal relations to specify and test an instant messaging server. - John Hughes 001; Ulf Norell; Jérôme Sautret (AST, 2010)

Accelerating race condition detection through procrastination. - Thomas Arts; John Hughes 001; Ulf Norell; Nicholas Smallbone; Hans Svensson (Erlang Workshop, 2011)

Testing blocking operations with QuickCheck's component library. - Ulf Norell; Hans Svensson; Thomas Arts (Erlang Workshop, 2013)

Interactive programming with dependent types. - Ulf Norell (ICFP, 2013)

An Expressive Semantics of Mocking. - Josef Svenningsson; Hans Svensson; Nicholas Smallbone; Thomas Arts; Ulf Norell; John Hughes 001 (FASE, 2014)

Attribute grammars in Erlang. - Ulf Norell; Alex Gerdes (Erlang Workshop, 2015)

Testing AUTOSAR software with QuickCheck. - Thomas Arts; John Hughes 001; Ulf Norell; Hans Svensson (ICST Workshops, 2015)

Find more bugs with QuickCheck! - John Hughes 001; Ulf Norell; Nicholas Smallbone; Thomas Arts (AST@ICSE, 2016)

Mysteries of DropBox: Property-Based Testing of a Distributed Synchronization Service. - John Hughes 001; Benjamin C. Pierce; Thomas Arts; Ulf Norell (ICST, 2016)

Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs. - Jesper Cockx; Orestis Melkonian; Lucas Escot; James Chapman 001; Ulf Norell (Haskell, 2022)

Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. - Andre Knispel; Orestis Melkonian; James Chapman 001; Alasdair Hill; Joosep Jääger; William J. DeMeo; Ulf Norell (FMBC@CAV, 2024)

IntersectMBO/formal-ledger-specifications. - Andre Knispel; Orestis Melkonian; James Chapman 001; Alasdair Hill; Joosep Jääger; William J. DeMeo; Ulf Norell (DROPS Artifacts, 2024)