A type and scope safe universe of syntaxes with binding: their semantics and proofs

Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna

Research output: Contribution to conferencePaper

Abstract

Almost every programming language’s syntax 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, 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.

Conference

ConferenceInternational Conference on Functional Programming 2018
Abbreviated titleICFP 2018
CountryUnited States
CitySt. Louis
Period23/09/1829/09/18

Fingerprint

Computer programming languages
Semantics
Substitution reactions
Binders
Printing

Keywords

  • generic programming
  • syntax with binding
  • semantics
  • logical relations
  • simulation
  • fusion
  • agda

Cite this

Allais, G., Atkey, R., Chapman, J., McBride, C., & McKinna, J. (2018). A type and scope safe universe of syntaxes with binding: their semantics and proofs. Paper presented at International Conference on Functional Programming 2018, St. Louis, United States.
Allais, Guillaume ; Atkey, Robert ; Chapman, James ; McBride, Conor ; McKinna, James. / A type and scope safe universe of syntaxes with binding : their semantics and proofs. Paper presented at International Conference on Functional Programming 2018, St. Louis, United States.30 p.
@conference{a29a27f05e034bc680a2c69a3f558223,
title = "A type and scope safe universe of syntaxes with binding: their semantics and proofs",
abstract = "Almost every programming language’s syntax 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, 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.",
keywords = "generic programming, syntax with binding, semantics, logical relations, simulation, fusion, agda",
author = "Guillaume Allais and Robert Atkey and James Chapman and Conor McBride and James McKinna",
year = "2018",
month = "9",
day = "23",
language = "English",
note = "International Conference on Functional Programming 2018, ICFP 2018 ; Conference date: 23-09-2018 Through 29-09-2018",

}

Allais, G, Atkey, R, Chapman, J, McBride, C & McKinna, J 2018, 'A type and scope safe universe of syntaxes with binding: their semantics and proofs' Paper presented at International Conference on Functional Programming 2018, St. Louis, United States, 23/09/18 - 29/09/18, .

A type and scope safe universe of syntaxes with binding : their semantics and proofs. / Allais, Guillaume; Atkey, Robert; Chapman, James; McBride, Conor; McKinna, James.

2018. Paper presented at International Conference on Functional Programming 2018, St. Louis, United States.

Research output: Contribution to conferencePaper

TY - CONF

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

PY - 2018/9/23

Y1 - 2018/9/23

N2 - Almost every programming language’s syntax 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, 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.

AB - Almost every programming language’s syntax 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, 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.

KW - generic programming

KW - syntax with binding

KW - semantics

KW - logical relations

KW - simulation

KW - fusion

KW - agda

UR - https://icfp18.sigplan.org/home

M3 - Paper

ER -

Allais G, Atkey R, Chapman J, McBride C, McKinna J. A type and scope safe universe of syntaxes with binding: their semantics and proofs. 2018. Paper presented at International Conference on Functional Programming 2018, St. Louis, United States.