POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Wed 17 Jan 2024 17:30 - 17:50 at Turing Lecture - Domain-Specific Languages Chair(s): Satnam Singh

JSON Schema is the de-facto standard schema language for JSON data. The language went through many minor revisions, but the most recent versions of the language, starting from Draft 2019-09, added two novel features, \emph{dynamic references} and \emph{annotation-dependent validation}, that change the evaluation model. \emph{Modern JSON Schema} is the name used to indicate all versions from Draft 2019-09, which are characterized by these new features, while \emph{Classical JSON Schema} is used to indicate the previous versions.

These new ``modern'' features make the schema language quite difficult to understand, and have generated many discussions about the correct interpretation of their official specifications; for this reason we undertook the task of their formalization. During this process, we also analyzed the complexity of data validation in Modern JSON Schema, with the idea of confirming the PTIME complexity of Classical JSON Schema validation, and we were surprised to discover a completely different truth: data validation, that is expected to be an extremely efficient process, acquires, with Modern JSON Schema features, a PSPACE complexity.

In this paper, we give the first formal description of Modern JSON Schema, which we have discussed with the community of JSON Schema tool developers, and which we consider a central contribution of the work that we present here. We then prove that its data validation problem is PSPACE-complete. We prove that the origin of the problem lies in dynamic references, and not in annotation-dependent validation. We study the schema and data complexities, showing that the problem is PSPACE-complete with respect to the schema size even with a fixed instance, but is in PTIME when the schema is fixed and only the instance size is allowed to vary. Finally, we run experiments that show that there are families of schemas where the difference in asymptotic complexity between dynamic and static references is extremely visible, even with small schemas.

Wed 17 Jan

Displayed time zone: London change

16:50 - 18:10
Domain-Specific LanguagesPOPL at Turing Lecture
Chair(s): Satnam Singh Groq
16:50
20m
Talk
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL
Pu Sun ShanghaiTech University, Fu Song State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, China, Yuqi Chen ShanghaiTech University, China, Taolue Chen University of London
17:10
20m
Talk
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL
Will Crichton Brown University, Shriram Krishnamurthi Brown University
Pre-print
17:30
20m
Talk
Validation of Modern JSON Schema: Formalization and Complexity
POPL
Lyes Attouche Université Paris-Dauphine -- PSL, Mohamed-Amine Baazizi Sorbonne Université, Dario Colazzo Université Paris-Dauphine -- PSL, Giorgio Ghelli Universita di Pisa, Carlo Sartiani Università della Basilicata, Stefanie Scherzinger Universität Passau
DOI
17:50
20m
Talk
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL
Xueying Qin The University of Edinburgh, Liam O'Connor University of Edinburgh, Rob van Glabbeek The University of Edinburgh, Peter Hoefner Australian National University, Ohad Kammar University of Edinburgh, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print