Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML

@Article{ brucker:nano-json:2022,
  author   = {Achim D. Brucker},
  title    = {{Nano JSON:} Working with {JSON} formatted data in
              {Isabelle/HOL} and {Isabelle/ML}},
  journal  = {Archive of Formal Proofs},
  month    = {jul},
  year     = {2022},
  date     = {2022-07-29},
  note     = {\url{https://www.isa-afp.org/entries/Nano_JSON.html}, Formal
              proof development. 
              Author copy: \url{http://logicalhacking.com/publications/brucker-nano-json-2022/}},
  issn     = {2150-914x},
  keywords = {JSON, Isabelle/HOL, Isabelle/ML},
  areas    = {formal methods, software engineering},
  abstract = {JSON (JavaScript Object Notation) is a common format for
              exchanging data, based on a collection of key/value-pairs (the
              JSON objects) and lists. Its syntax is inspired by JavaScript
              with the aim of being easy to read and write for humans and
              easy to parse and generate for machines. Despite its origin in
              the JavaScript world, JSON is language-independent and many
              programming languages support working with JSON-encoded data.
              This makes JSON an interesting format for exchanging data with
              Isabelle/HOL. This AFP entry provides a JSON-like
              import-expert format for both Isabelle/ML and Isabelle/HOL. On
              the one hand, this AFP entry provides means for Isabelle/HOL
              users to work with JSON encoded data without the need using
              Isabelle/ML. On the other and, the provided Isabelle/ML
              interfaces allow additional extensions or integration into
              Isabelle extensions written in Isabelle/ML. While format is
              not fully JSON compliant (e.g., due to limitations in the
              range of supported Unicode characters), it works in most
              situations: the provided implementation in Isabelle/ML and its
              representation in Isabelle/HOL have been used successfully in
              several projects for exchanging data sets of several
              hundredths of megabyte between Isabelle and external tools.},
}