TY - JOUR
T1 - A type- And scope-safe universe of syntaxes with binding
T2 - Their semantics and proofs
AU - Allais, Guillaume
AU - Atkey, Robert
AU - Chapman, James
AU - McBride, Conor
AU - McKinna, James
N1 - Funding Information:
Allais acknowledges the support of EPSRC grant no. EP/M016951/1 Homotopy Type Theory: Programming and Verification. Part of the research leading to these results has also received funding from the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement nr. 320571. Atkey acknowledges the support of EPSRC grant no. EP/T026960/1 AISEC: AI Secure and Explainable by Construction. Chapman thanks IOHK for their support. McKinna gratefully acknowledges the support of LFCS, School of Informatics, University of Edinburgh. The authors would like to thank the ICFP and JFP reviewers for their useful comments, and the JFP editors and staff for their patience.
Publisher Copyright:
© The Author(s), 2021.
PY - 2021/10/19
Y1 - 2021/10/19
N2 - The syntax of almost every programming language includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope-safe operation (e.g., renaming, substitution, desugaring, printing), and then again for correctness proofs. We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope-safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material available online at https://github.com/gallais/generic-syntax.
AB - The syntax of almost every programming language includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope-safe operation (e.g., renaming, substitution, desugaring, printing), and then again for correctness proofs. We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope-safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material available online at https://github.com/gallais/generic-syntax.
UR - http://www.scopus.com/inward/record.url?scp=85118205274&partnerID=8YFLogxK
U2 - 10.1017/S0956796820000076
DO - 10.1017/S0956796820000076
M3 - Article
SN - 0956-7968
VL - 31
JO - Journal of Functional Programming
JF - Journal of Functional Programming
M1 - e22
ER -