Publications and drafts

• Correct-by-Construction Pretty-Printing
  Nils Anders Danielsson
  Draft. [abstract, pdf, highlighted Agda code, tarball with code]
• Isomorphism Is Equality
  Thierry Coquand and Nils Anders Danielsson
  Draft. [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, darcs 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, darcs 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, errata]
• 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, errata]
• 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)]