A Canonical Locally Named Representation of Binding

Randy Pollack, Masahiko Sato, Wilmer Ricciotti

Research output: Contribution to journalArticlepeer-review

Abstract

This paper is about completely formal representation of languages with binding. We have previously written about a representation following an approach going back to Frege, based on first-order syntax using distinct syntactic classes for locally bound variables vs. global or free variables (Sato and Pollack, J Symb Comput 45:598?616, 2010 ). The present paper differs from our previous work by being more abstract. Whereas we previously gave a particular concrete function for canonically choosing the names of binders, here we characterize abstractly the properties required of such a choice function to guarantee canonical representation, and focus on the metatheory of the representation, proving that it is in substitution preserving isomorphism with the nominal Isabelle representation of pure lambda terms. This metatheory is formalized in Isabelle/HOL. The final section outlines a formalization in Matita of a challenging language with multiple binding and simultaneous substitution. The Isabelle and Matita proof files are available online.
Original languageEnglish
Pages (from-to)185-207
Number of pages23
JournalJournal of Automated Reasoning
Volume49
DOIs
Publication statusPublished - 2012

Fingerprint Dive into the research topics of 'A Canonical Locally Named Representation of Binding'. Together they form a unique fingerprint.

Cite this