[Prev][Next][Index][Thread]
Thesis
[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
I would like to announce that my newly finished dissertation is available
at my homepage
http://www.brics.dk/~tor
Title and abstract is included below.
With best regards,
Torben Bra|ner
BRICS, University of Aarhus
-----------------------------------------------------------------------------
TITLE:
An Axiomatic Approach to Adequacy
ABSTRACT:
This thesis studies adequacy for PCF-like languages in a general categorical
framework. An adequacy result relates the denotational semantics of a program
to its operational semantics; it typically states that a program terminates
whenever the interpretation is non-bottom. The main concern is to generalise
to a linear version of PCF the adequacy results known for standard PCF, keeping
in mind that there exists a Girard translation from PCF to linear PCF with
respect to which the new constructs should be sound. General adequacy results
have usually been obtained in order-enriched categories, that is, categories
where all hom-sets are typically cpos, maps are assumed to be continuous and
fixpoints are interpreted using least upper bounds. One of the main contributions
of the thesis is to propose a completely different approach to the problem of
axiomatising those categories which yield adequate semantics for PCF and
linear PCF. The starting point
is that the only unavoidable assumption for dealing with adequacy is the
existence, in any object, of a particular "undefined" point denoting the
non-terminating computation of the corresponding type; hom-sets are pointed sets,
and this is the only required structure. In such a category of pointed objects,
there is a way of axiomatising fixpoint operators: They are maps satisfying
certain equational axioms, and furthermore, satisfying a very natural
(non-equational) axiom, with respect to "undefined" elements, called rational
openness. It is shown that this axiom is sufficient (and in a precise sense
necessary) for adequacy. The idea is developed in the intuitionistic case
(standard PCF)
as well as in the linear case (linear PCF), which is obtained by augmenting a
Curry-Howard interpretation of Intuitionistic Linear Logic with numerals and
fixpoint constants, appropriate for the linear context. Using instantiations
to concrete models of the general adequacy results, various purely syntactic
properties of linear PCF are proved to hold.
-----------------------------------------------------------------------------
########### B R I C S | Torben Bra|ner, Ph.D.
##### ##### Department of Computer Science | Research Assistant Professor
########### University of Aarhus | tor@brics.dk
##### ##### Ny Munkegade, Building 540 | +45 8942 3192 Office
##### ##### DK-8000 Aarhus C | +45 8942 3360 BRICS
##### ##### Denmark | +45 8942 3255 Fax
WWW <URL: http://www.brics.dk/~tor>