Archive Page 2

Proposed Mathoverflow-style site for theoretical computer scientists

This isn’t strictly related to name binding, but it may interest some of the readers here.

There’s currently plans to set up a Mathoverflow-style site for theoretical computer scientists.  Here, theoretical computer science is being widely interpreted to include type theory, programming language semantics, automated reasoning, and so on, as well as the likes of computational complexity and computational geometry.  Some example on- and off-topic questions are provided with the proposal definition.

The proposal process is fairly simple.  If you wish to support the creation of this site, then simply follow the above link and press “Commit”.  Once the “Commit” counter reaches 100%, the site automatically launches in beta-mode.

Relating nominal and higher-order abstract syntax specifications

By Andrew Gacek, from PPDP 2010, available from Andrew Gacek’s website:

Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along similar lines but with subtle differences that make them difficult to relate. The nominal abstract syntax community has devices like names, freshness, name-abstractions with variable capture, and the new-quantifier, whereas the higher-order abstract syntax community has devices like lambda-binders, lambda conversion, raising, and the nabla-quantifier. This paper aims to unify these communities and provide a concrete correspondence between their different devices. In particular, we develop a semantics-preserving translation from alpha-Prolog, a nominal abstract syntax based logic programming language, to G-, a higher-order abstract syntax based logic programming language. We also discuss higher-order judgments, a common and powerful tool for specifications with higher-order abstract syntax, and we show how these can be incorporated into G-. This establishes G- as a language with the power of higher-order abstract syntax, the fine-grained variable control of nominal specifications, and the desirable properties of higher-order judgments.

The nabla-calculus. Functional programming with higher-order encodings.

By Carsten Schurmann, Adam Poswolsky and Jeffrey Sarnat, from TLCA 2005, available from the Elphin website:

Higher-order encodings use functions provided by one language to represent variable binders of another. They lead to concise and elegant representations, which historically have been difficult to analyze and manipulate.
In this paper we present the nabla-calculus, a calculus for defining general recursive functions over higher-order encodings. To avoid problems commonly associated with using the same function space for representations and computations, we separate one from the other. The simply-typed λ-calculus plays the role of the representation level. The computation level contains not only the usual computational primitives but also an embedding of the representation-level. It distinguishes itself from similar systems by allowing recursion under representation-level λ-binders while permitting a natural style of programming which we believe scales to other logical frameworks. Sample programs include bracket abstraction, parallel reduction, and an evaluator for a simple language with first-class continuations.

A nominal relational model for local store

Sorry for the delay in updates (thesis writing is taking priority)!  I saw Rasmus talk about this yesterday in Edinburgh.

By Rasmus Mogelberg, accepted at MFPS 2010, available from Rasmus Mogelberg’s website:

Many authors have in recent work suggested using nominal sets as a framework for modelling local store because this allows for a more elementary development than the traditional presheaf models. However, when modelling the important principle of relational reasoning for local store all these models use families of relations indexed by relations on store, and thus essentially return to presheaf models on the relational level. In this paper we show how relational reasoning can also be modelled using nominal sets. Building on a model suggested by Pitts and Shinwell we construct a relational model for local store in nominal sets in which types are interpreted as relations. These relational interpretations of types capture, in a single relation for each type, the relational reasoning principle for local store which in previous models was captured using a family of relations for each type. The relational model also demonstrates how the relations constitute a model in their own right, which hopefully means that they can be used to construct better models. Using the relational model we construct a relational parametricity principle for the operation allocating local store, and we show how this implies the relational reasoning principle.

A name abstraction functor for named sets

By Vincenzo Ciancia and Ugo Montinari, from CMCS 2008, available from Vincenzo Ciancia’s website:

The problem of dening fully abstract operational models of name passing calculi has been given some elegant solutions, such as coalgebras over presheaf categories or over nominal sets. These formalisms fail to model garbage collection of unused names, hence they do not have nice properties with respects to finite state algorithms. The category of named sets, on the other hand, was designed for the purpose of supporting ecient algorithms to handle the semantics of name passing calculi. However the theory was developed in a rather ad-hoc fashion (e.g. the existence of a final coalgebra was only proved in the finite case). In this work we introduce a name abstraction functor for named sets and show that it provides a simple and effective notion of garbage collection of unused names. Along the way, we survey a number of needed results on the category of permutation algebras, an algebra-theoretic denition of nominal sets. In particular we give a formalization of the adjunction between abstraction and concretion, an example illustrating a nominal syntax alike handling of De Bruijn indexes, and an explicit functor to model the early semantics of the π -calculus in nominal sets.

Reasoning with higher-order abstract syntax and contexts

By Amy Felty and Brigitte Pientka, from ITP 2010, available from Amy Felty’s website:

A variety of logical frameworks support the use of higher-order abstract syntax (HOAS) in representing formal systems given via axioms and inference rules and reasoning about them. In such frameworks, object-level binding is encoded directly using meta-level binding. Although these systems seem superficially the same, they differ in a variety of ways; for example, in how they handle a context of assumptions and in what theorems about a given formal system can be expressed and proven. In this paper, we present several case studies which highlight a variety of different aspects of reasoning using HOAS, with the intention of providing a basis for qualitative comparison of different systems. We then carry out such a comparison among three systems: Twelf, Beluga, and Hybrid. We also develop a general set of criteria for comparing such systems. We hope that others will implement these challenge problems, apply these criteria, and further our understanding of the trade-offs involved in choosing one system over another for this kind of reasoning.

Associated proof scripts can be found here.

Nominal domain theory for concurrency

By David Turner and Glynn Winskel, from CSL 2009, available from Glynn Winskel’s website:

This paper investigates a methodology of using FM (Fraenkel-Mostowski) sets, and the ideas of nominal set theory, to adjoin name generation to a semantic theory. By developing a domain theory for concurrency within FM sets the domain theory inherits types and operations for name generation, essentially without disturbing its original higher-order features. The original domain theory had a metalanguage HOPLA (Higher Order Process Language) and accordingly this expands to a metalanguage, Nominal HOPLA, with name generation (closely related to an earlier language new-HOPLA). Nominal HOPLA possesses an operational and denotational semantics which are related via soundness and adequacy results, again carried out within FM sets.