Publications and drafts- A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
Andreas Abel, Nils Anders Danielsson and Oskar Eriksson Proceedings of the ACM on Programming Languages,
Volume 7, Issue ICFP, 2023
(ICFP 2023,
10.1145/3607862).
[abstract, pdf, highlighted Agda code, zip file with code] - Compiling Programs with Erased Univalence
Andreas Abel, Nils Anders Danielsson and Andrea Vezzosi Draft, 2021.
[abstract, pdf, extended version, highlighted Agda code, zip file with code] - Higher Lenses
Paolo Capriotti, Nils Anders Danielsson and Andrea Vezzosi 2021 36th
Annual ACM/IEEE Symposium on Logic in Computer Science
(LICS)
(10.1109/LICS52264.2021.9470613).
[abstract, pdf, highlighted Agda code, zip file with code] - Higher Inductive Type Eliminators Without Paths
Nils Anders Danielsson 25th International Conference on Types for Proofs and
Programs, TYPES 2019
(10.4230/LIPIcs.TYPES.2019.10).
[abstract, pdf, highlighted Agda code, zip file with code] - Practical Dependent Type Checking using Twin Types
Vı́ctor López Juan and Nils Anders Danielsson TyDe '20,
Proceedings of the 5th ACM SIGPLAN International Workshop
on Type-Driven Development
(10.1145/3406089.3409030).
[abstract, pdf] - Logical properties of a modality for erasure
Nils Anders Danielsson Draft, 2019.
[abstract, pdf, highlighted Agda code, zip file with code] - Total Definitional Interpreters for Time and
Space Complexity
Nils Anders Danielsson Draft, 2018.
[abstract, pdf, highlighted Agda code, zip file with code] - Up-to Techniques using Sized Types
Nils Anders Danielsson Proceedings of the ACM on Programming Languages,
Volume 2, Issue POPL, 2018
(POPL 2018,
10.1145/3158131).
[abstract, pdf, highlighted Agda code, zip file with code] - Type Theory with Weak J
Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, Simon Huber and Nicolai Kraus Two-page abstract for
TYPES 2017.
[pdf, accompanying code (may include more recent developments)] - Towards practical out-of-order unification
Nils Anders Danielsson and Vı́ctor López Juan Two-page abstract for
TYPES 2017.
[pdf] - Partiality, Revisited
The Partiality Monad as a Quotient Inductive-Inductive Type Thorsten Altenkirch, Nils Anders Danielsson and Nicolai Kraus Foundations of Software Science and Computation
Structures, 20th International Conference,
FOSSACS 2017.
This is the authors' version of the paper.
The final publication is available at Springer via
http://dx.doi.org/10.1007/978-3-662-54458-7_31.
This version contains some insignificant improvements to the
text that are not present in the published version.
[abstract, pdf, highlighted Agda code, zip file with code] - Dependent lenses
Nils Anders Danielsson Draft, 2016.
[abstract, pdf, accompanying code (may include more recent developments)] - Partiality, Revisited
Thorsten Altenkirch and Nils Anders Danielsson Two-page abstract for
TYPES 2016.
[pdf, accompanying code (may include more recent developments)] - Correct-by-Construction Pretty-Printing
Nils Anders Danielsson Proceedings of the 2013 ACM SIGPLAN Workshop on
Dependently-Typed Programming
(DTP 2013).
© Nils Anders Danielsson 2013. This is the
author's version of the work. It is posted here for your
personal use. Not for redistribution. The definitive version
was published in
DTP'13.
[abstract, pdf, highlighted Agda code, tarball with code] - Isomorphism is equality
Thierry Coquand and Nils Anders Danielsson In
Indagationes Mathematicae 24(4), 2013.
[abstract, pdf, highlighted Agda code, tarball with code] - Operational Semantics Using the Partiality Monad
Nils Anders Danielsson Proceedings of the 17th ACM SIGPLAN international
conference on Functional programming
(ICFP 2012).
© ACM, 2012. This is the author's version of the
work. It is posted here by permission of ACM for your
personal use. Not for redistribution. The definitive
version was published in ICFP '12,
http://doi.acm.org/10.1145/2364527.2364546.
[abstract, pdf, highlighted Agda code, tarball with code (also MiniAgda code)] - Bag Equivalence via a Proof-Relevant Membership Relation
Nils Anders Danielsson Interactive Theorem Proving,
Third International Conference,
ITP 2012.
The original publication is available at www.springerlink.com. [abstract, pdf, highlighted code, tarball with code, Git repository (may include more recent developments)] - Total Parser Combinators
Nils Anders Danielsson Proceedings of the 15th ACM SIGPLAN international
conference on Functional programming
(ICFP 2010).
© ACM, 2010. This is the author's version of the
work. It is posted here by permission of ACM for your
personal use. Not for redistribution. The definitive
version was published in ICFP'10,
http://doi.acm.org/10.1145/1863543.1863585.
[abstract, pdf, highlighted code, tarball with code, Git repository (includes more recent developments, does not match the tarball)] - Beating the Productivity Checker Using Embedded Languages
Nils Anders Danielsson In the proceedings of the Workshop on Partiality and
Recursion in Interactive Theorem Provers
(PAR 2010),
EPTCS 43, 2010.
[abstract, pdf, highlighted code, tarball with code] - Termination Checking in the Presence of Nested Inductive and Coinductive Types
Thorsten Altenkirch and Nils Anders Danielsson Short note supporting a talk given at
PAR 2010,
Workshop on Partiality and Recursion
in Interactive Theorem Provers.
[abstract, pdf] - Subtyping, Declaratively
An Exercise in Mixed Induction and Coinduction Nils Anders Danielsson and Thorsten Altenkirch In Mathematics of Program Construction, Tenth
International Conference,
MPC 2010.
The original publication is available at www.springerlink.com. [abstract, pdf, highlighted code, tarball with code] - ΠΣ: Dependent Types without the Sugar
Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh and Nicolas Oury In the proceedings of Functional and Logic Programming,
10th International Symposium,
FLOPS 2010.
The original publication is available at www.springerlink.com. [abstract, pdf, implementation] - Mixing Induction and Coinduction
Nils Anders Danielsson and Thorsten Altenkirch Draft, 2009.
For an extended description of the total parser combinators
described in this paper, see
Total Parser Combinators.
For an extended discussion of subtyping for recursive types, see
Subtyping, Declaratively.
For more information about working around productivity
checkers, see
Beating the Productivity
Checker Using Embedded Languages.
For another spin on coinductive operational semantics, see
Operational Semantics Using the Partiality Monad.
[abstract, pdf, highlighted code, tarball with code] - Structurally Recursive Descent Parsing
Nils Anders Danielsson and Ulf Norell Draft, never submitted, 2008.
For another, arguably more elegant, approach to total parsing, see Total Parser Combinators. [abstract, pdf, highlighted code (does not match the paper exactly)] - Parsing Mixfix Operators
Nils Anders Danielsson and Ulf Norell In Implementation and Application of Functional Languages,
20th International Symposium,
IFL 2008.
The original publication is available at www.springerlink.com. [abstract, pdf, code, highlighted code] - Functional Program Correctness Through Types
Nils Anders Danielsson PhD thesis, Chalmers University of Technology and
Göteborg University, 2007.
[abstract, pdf] - Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures
Nils Anders Danielsson Conference record of the 35th ACM SIGPLAN-SIGACT
symposium on Principles of programming languages
(POPL 2008).
© ACM, 2008. This is the author's version of the
work. It is posted here by permission of ACM for your
personal use. Not for redistribution. The definitive
version was published in POPL'08,
http://doi.acm.org/10.1145/1328438.1328457.
Accompanying technical report.
[abstract, pdf, accompanying code] - A Formalisation of the Correctness Result From "Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures"
Nils Anders Danielsson Technical report 2007:16,
Department of Computer Science and Engineering,
Chalmers University of Technology.
[abstract, pdf] - A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
Nils Anders Danielsson Types for Proofs and Programs, International Workshop,
TYPES 2006,
Revised Selected Papers, LNCS 4502, 2007.
Copyright © Springer-Verlag Berlin Heidelberg 2007. [abstract, pdf, accompanying code] - Fast and Loose Reasoning is Morally Correct
Nils Anders Danielsson, John Hughes, Patrik Jansson and Jeremy Gibbons Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2006). © ACM, 2006. This is a minor revision of the
work published in POPL'06,
http://doi.acm.org/10.1145/1111037.1111056.
Accompanying technical report.
[abstract, pdf] - Proofs Accompanying "Fast and Loose Reasoning is Morally Correct"
Nils Anders Danielsson Technical report 2007:15,
Department of Computer Science and Engineering,
Chalmers University of Technology.
[abstract, pdf] - Precise Reasoning About Non-strict Functional Programs; How to Chase Bottoms, and How to Ignore Them
Nils Anders Danielsson Licentiate thesis, 2005. [abstract, pdf] - Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values
Nils Anders Danielsson and Patrik Jansson Proceedings of the 7th International Conference on Mathematics of Program Construction, MPC 2004, LNCS 3125, 2004. Copyright © Springer-Verlag. Accompanying library: Chasing Bottoms. Extended version with most proofs available, see the first part of my licentiate thesis. [abstract, ps.gz, pdf] - Matroids from Modules
Nils Anders Danielsson and Michael B. Smyth Electronic Notes in Theoretical Computer Science, Vol. 74, Elsevier 2003. Presented at MFCSIT2002. [abstract, pdf, ps.gz] - Axiomatic Discrete Geometry
Nils Anders Danielsson Master's thesis, Imperial College of Science, Technology and Medicine, London, 2002. [abstract, pdf, ps.gz, errata (errors listed have been corrected in the online version)] Nils Anders Danielsson Last updated Fri Aug 25 13:09:47 UTC 2023. |