Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Nano_JSON


view this post on Zulip Email Gateway (Aug 22 2022 at 18:54):

From: Gerwin Klein <kleing@unsw.edu.au>
Nano JSON: Working With JSON Formatted Data in Isabelle/HOL and Isabelle/ML
by Achim D. Brucker

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.


Last updated: Apr 25 2024 at 20:15 UTC