Any views expressed within media held on this service are those of the contributors, should not be taken as approved or endorsed by the University, and do not necessarily reflect the views of the University in respect of any particular issue.

【BAYES COFFEE HOUSE TECH TALK SERIES】Locally Nameless Syntax and Semantics

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: 4th 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.

css.php

Report this page

To report inappropriate content on this page, please use the form below. Upon receiving your report, we will be in touch as per the Take Down Policy of the service.

Please note that personal data collected through this form is used and stored for the purposes of processing this report and communication with you.

If you are unable to report a concern about content via this form please contact the Service Owner.

Please enter an email address you wish to be contacted on. Please describe the unacceptable content in sufficient detail to allow us to locate it, and why you consider it to be unacceptable.
By submitting this report, you accept that it is accurate and that fraudulent or nuisance complaints may result in action by the University.

  Cancel