[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>