Nils Anders Danielsson

28 papers A* 3A 2B 4Misc 1Journal 5Unranked 10
YearRankTypeTitle / Venue / Authors
2026 J jnl
A Graded Modal Dependent Type Theory with Erasure, Formalized.
CoRR
Andreas Abel, Nils Anders Danielsson, Oskar Eriksson
2026 J jnl
Normalisation for First-Class Universe Levels.
Proc. ACM Program. Lang.
Nils Anders Danielsson, Naïm Camille Favier, Ondrej Kubánek
2023 J jnl
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.
Proc. ACM Program. Lang.
Andreas Abel, Nils Anders Danielsson, Oskar Eriksson
2021 A* conf
Higher Lenses.
LICS
Paolo Capriotti, Nils Anders Danielsson, Andrea Vezzosi
2020 — conf
Practical dependent type checking using twin types.
TyDe@ICFP
Víctor López Juan, Nils Anders Danielsson
2019 — conf
Higher Inductive Type Eliminators Without Paths.
TYPES
Nils Anders Danielsson
2018 J jnl
Up-to techniques using sized types.
Proc. ACM Program. Lang.
Nils Anders Danielsson
2017 B conf
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.
FoSSaCS
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
2016 J jnl
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.
CoRR
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
2014 — ed.
Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, PLPV 2014, January 21, 2014, San Diego, California, USA, Co-located with POPL '14
PLPV
Nils Anders Danielsson, Bart Jacobs
2013 — ed.
18th International Workshop on Types for Proofs and Programs, TYPES 2011, Bergen, Norway, September 8-11, 2011
TYPES
Nils Anders Danielsson, Bengt Nordström
2013 — conf
Correct-by-construction pretty-printing.
DTP@ICFP
Nils Anders Danielsson
2012 B conf
Bag Equivalence via a Proof-Relevant Membership Relation.
ITP
Nils Anders Danielsson
2012 A conf
Operational semantics using the partiality monad.
ICFP
Nils Anders Danielsson
2011 — conf
Frontmatter, Table of Contents, Preface, Workshop Organization.
TYPES
Nils Anders Danielsson, Bengt Nordström
2010 — conf
Beating the Productivity Checker Using Embedded Languages
PAR
Nils Anders Danielsson
2010 — conf
Beating the Productivity Checker Using Embedded Languages.
PAR@ITP
Nils Anders Danielsson
2010 Misc conf
PiSigma: Dependent Types without the Sugar.
FLOPS
Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, Nicolas Oury
2010 B conf
Subtyping, Declaratively.
MPC
Nils Anders Danielsson, Thorsten Altenkirch
2010 — conf
Termination Checking in the Presence of Nested Inductive and Coinductive Types.
PAR@ITP
Thorsten Altenkirch, Nils Anders Danielsson
2010 A conf
Total parser combinators.
ICFP
Nils Anders Danielsson
2008 A* conf
Lightweight semiformal time complexity analysis for purely functional data structures.
POPL
Nils Anders Danielsson
2008 — conf
Parsing Mixfix Operators.
IFL
Nils Anders Danielsson, Ulf Norell
2007 — —
Functional Program Correctness Through Types.
Nils Anders Danielsson
2006 — conf
A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family.
TYPES
Nils Anders Danielsson
2006 A* conf
Fast and loose reasoning is morally correct.
POPL
Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons
2004 B conf
Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values.
MPC
Nils Anders Danielsson, Patrik Jansson
2002 — conf
Matroids from modules.
MFCSIT
Nils Anders Danielsson, Michael B. Smyth