A fresh look at programming with names and binders

8 years 8 months ago
A fresh look at programming with names and binders
A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms which allow performing these manipulations in a safe and natural style has, to a large extent, remained elusive. In this paper, we present a novel approach to the problem. Our proposal can be viewed either as a programming language design or as a library: in fact, it is currently implemented within Agda. It provides a safe and expressive means of programming with names ers. It is abstract enough to support multiple concrete implementations: we present one in nominal style and one in de Bruijn style. We use logical relations to prove that "well-typed programs do not mix names with different scope". We exhibit an adequate encoding of Pitts-style nominal terms into our system. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features--Data types and structures; Po...
Nicolas Pouillard, François Pottier
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2010
Where ICFP
Authors Nicolas Pouillard, François Pottier
Comments (0)