[07/11/23] Partner Event - Locally Nameless Syntax and Semantics About the event Abstract It is increasingly common to produce machine-checked definitions and proofs when presenting some piece of new programming language theory. The scientific need for formality is particularly acute when the definitions are large (or stray from simple semantic intuitions), or when the proofs are long and complicated. There is also social need: it is now not unusual for conference and journal referees to demand machine-checked developments of nitty gritty details to enable them to concentrate on assessing the underlying ideas. Modern interactive theorem proving systems (ITPs) can make the task of producing formal programming language meta-theory sufficiently fun (if still time consuming) for such tools to be used during the development of ideas as well as after the fact to check correctness. But unwise choices of mathematical representation of syntactic structure to begin with can come back to bite one when computing and proving with the representation. This is particularly so when there are operations that bind names within static scopes, where one should represent syntax in a way that factors out renaming of bound names in some way. In this talk I will review locally nameless syntax, contrasting it with nominal and completely nameless styles of representing syntax with binders. There is good evidence for the utility of this approach within existing ITPs, especially when combined with cofinite quantification over names. I will also briefly describe a new mathematical foundation for the locally nameless representation and some consequences of that. Speaker Bio Andrew Pitts is Emeritus Professor of Theoretical Computer Science in the University of Cambridge and an Emeritus Fellow of Darwin College, Cambridge. His work has ranged over category theory, constructive logic, type theory, programming language semantics, and the design of metaprogramming languages; he has a long-standing interest in the semantics and logic of names, locality and binding. He is an ACM Fellow and a recipient of the Alonzo Church Award for Outstanding Contributions to Logic and Computation. Nov 07 2023 11.00 - 12.00 [07/11/23] Partner Event - Locally Nameless Syntax and Semantics Join Huawei and Andrew Pitts for this tech talk, taking place on 7th of November. 4th floor Bayes Centre Join Online: https://meeting.huaweicloud.com/welink/webrtc/?lang=en-US#/j/94998553 Passcode: 104582
[07/11/23] Partner Event - Locally Nameless Syntax and Semantics About the event Abstract It is increasingly common to produce machine-checked definitions and proofs when presenting some piece of new programming language theory. The scientific need for formality is particularly acute when the definitions are large (or stray from simple semantic intuitions), or when the proofs are long and complicated. There is also social need: it is now not unusual for conference and journal referees to demand machine-checked developments of nitty gritty details to enable them to concentrate on assessing the underlying ideas. Modern interactive theorem proving systems (ITPs) can make the task of producing formal programming language meta-theory sufficiently fun (if still time consuming) for such tools to be used during the development of ideas as well as after the fact to check correctness. But unwise choices of mathematical representation of syntactic structure to begin with can come back to bite one when computing and proving with the representation. This is particularly so when there are operations that bind names within static scopes, where one should represent syntax in a way that factors out renaming of bound names in some way. In this talk I will review locally nameless syntax, contrasting it with nominal and completely nameless styles of representing syntax with binders. There is good evidence for the utility of this approach within existing ITPs, especially when combined with cofinite quantification over names. I will also briefly describe a new mathematical foundation for the locally nameless representation and some consequences of that. Speaker Bio Andrew Pitts is Emeritus Professor of Theoretical Computer Science in the University of Cambridge and an Emeritus Fellow of Darwin College, Cambridge. His work has ranged over category theory, constructive logic, type theory, programming language semantics, and the design of metaprogramming languages; he has a long-standing interest in the semantics and logic of names, locality and binding. He is an ACM Fellow and a recipient of the Alonzo Church Award for Outstanding Contributions to Logic and Computation. Nov 07 2023 11.00 - 12.00 [07/11/23] Partner Event - Locally Nameless Syntax and Semantics Join Huawei and Andrew Pitts for this tech talk, taking place on 7th of November. 4th floor Bayes Centre Join Online: https://meeting.huaweicloud.com/welink/webrtc/?lang=en-US#/j/94998553 Passcode: 104582
Nov 07 2023 11.00 - 12.00 [07/11/23] Partner Event - Locally Nameless Syntax and Semantics Join Huawei and Andrew Pitts for this tech talk, taking place on 7th of November.
