[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, March 30, 2005
12:00(*)-1:15
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

(*) note non-standard starting time:  the 2005 Senior Class picture is
scheduled for 1145.  We will start as soon as that is done, which
should be about 1200.

Eli Barzilay

Implementing Syntactic Reflection in Nuprl

Reflection is the ability of some entity to refer to itself.  In a
logical context, it is the ability of a logic to reason about itself.
Reflection is, therefore, placed at the core of meta-mathematics,
making it an important part of formal reasoning; where it revolves
mainly around syntax and semantics --- the main challenge is in making
the syntax of the logic become part of its semantic domain.

Given its importance, it is surprising that logical computer systems
tend to avoid the subject, or provide poor tools for reflective work.
This is in sharp contrast to the area of programming languages, where
reflection is well researched and used in a variety of ways where it
plays an central role.  One factor in making reflection inaccessible
in logical systems is the relative difficulty that is immediately
encountered when formalizing syntax: dealing with formal syntax means
dealing with structures that involve bindings, and in a logical
context it seems natural to use the same formal tools to describe
syntax --- often limiting the usability of such formalizations to
specific theories and toy examples.  Godel numbers are an example for
a reflective formalism that serves its purpose, yet is impractical as
a basis for syntactical reasoning in applied systems.

In programming languages, there is a simple yet elegant strategy for
implementing reflection: instead of making a system that describes
itself, the system is made available to itself.  We name this strong
reflection, where the representation of language features via its
semantics is actually part of the semantics itself --- unlike the
usual practice in formal systems of employing weak reflection.  The
advantages of this approach is the fact that both the system and its
reflected counterpart are inherently identical, making for a
lightweight implementation.

In this work we develop the formal background and the practical
capabilities of an applied system, namely Nuprl, that are needed to
support strong reflection of its own syntax.  Achieving this is a
major milestone on the road for a fully reflected logical system.  As
we shall demonstrate, our results enable dealing with syntactical
meta-mathematical content.

Upcoming Events:

volunteers needed!

--Mitch