A type and scope safe universe of syntaxes with binding : their semantics and proofs
Allais, Guillaume and Atkey, Robert and Chapman, James and McBride, Conor and McKinna, James (2021) A type and scope safe universe of syntaxes with binding : their semantics and proofs. Journal of Functional Programming, 31. e22. ISSN 0956-7968 (https://doi.org/10.1017/S0956796820000076)
Preview |
Text.
Filename: Allais_etal_JFP_2020_A_type_and_scope_safe_universe_of_syntaxes_with_binding.pdf
Accepted Author Manuscript License: Download (407kB)| Preview |
Abstract
Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of alpha-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, etc.), 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 .
ORCID iDs
Allais, Guillaume ORCID: https://orcid.org/0000-0002-4091-657X, Atkey, Robert ORCID: https://orcid.org/0000-0002-4414-5047, Chapman, James, McBride, Conor ORCID: https://orcid.org/0000-0003-1487-0886 and McKinna, James;-
-
Item type: Article ID code: 71939 Dates: DateEvent19 October 2021Published28 January 2020AcceptedSubjects: Science > Mathematics > Computer software Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 31 Mar 2020 11:18 Last modified: 12 Dec 2024 09:32 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/71939