Andrew Pitts, University of Cambridge will give a talk, in person and online, for the Coffee House Tech Talk Series. Details of the talk are below.

Speaker: Andrew Pitts, University of Cambridge

Title: Locally Nameless Syntax and Semantics

When: 11am Tue 7 Nov

Where: 4^th floor Bayes Centre

External link: https://meeting.huaweicloud.com/welink/webrtc/?lang=en-US#/j/94998553

Passcode: 104582

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.

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.

【BAYES COFFEE HOUSE TECH TALK SERIES】Locally Nameless Syntax and Semantics / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0