A Core Calculus for Documents: Or, Lambda: The Ultimate Document
Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that model these languages. This matters because the interaction between document and program can be subtle and error-prone. In this paper we describe several such problems, then taxonomize and formalize document languages as levels of a document calculus. We employ the calculus as a foundation for implementing complex features such as reactivity, as well as for proving theorems about the boundary of content and computation. We intend for the document calculus to provide a theoretical basis for new document languages, and to assist designers in cleaning up the unsavory corners of existing languages.
Wed 17 JanDisplayed time zone: London change
16:50 - 18:10 | |||
16:50 20mTalk | 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 20mTalk | A Core Calculus for Documents: Or, Lambda: The Ultimate Document POPL Pre-print | ||
17:30 20mTalk | 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 20mTalk | 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 |