SWS   Info

AG Audience

English

60 Minutes

Saarbrücken

Nominal datatypes are a simple extension of the usual notion of
algebraic datatypes with facilities for declaring constructors
involving names and name-binding. In this talk I want to revisit the
topic of higher-order functional programming with nominal datatypes.
Destructing name-bindings seems to inevitably involve the use of
locally scoped names in one form or another. The original work on this
topic (such as Shinwell's Fresh patch for OCaml) used state-based
implementations of local scoping. In this talk I will discuss this and
two other possible implementations, that have greater degrees of
purity.

As far as I am concerned, the goal of this work is to arrive at a
language design that (1) can express common patterns of use of bound
names in informal algorithms that manipulate syntax with binders, but
(2) has good logical properties---for example, that can co-exist with
Constructive Type Theory. That goal has yet to be attained.

Brigitta Hansen

0681 - 93039102

--email hidden

Yes

Kaiserslautern

G26

206

passcode not visible

logged in users only