🚀 go-pugleaf

Christian Doppler Labor fuer Expertensysteme
 and 
Lecture Series ``Collegium Logicum''
Kurt Goedel Society

University of Technology, Vienna, Austria


Lecture Announcement
--------------------

Maurizio Martelli
-----------------
D.I.S.I. - Dipartimento di Informatica e Scienze dell'Informazione
Universit`a di Genova, Viale Benedetto XV, 3, 16132 - Genoa, Italy
		
Reconsidering Objects in Linear Logic
-------------------------------------	
Monday, January 30, 1995, 14:00


ABSTRACT:
Girard's Linear Logic captures the essence of a logic
suitable for computer science. Indeed, following Heyting's 
intuition of it proofs as computations, the linear logic 
rules express the operational flavour of the behaviour of
programming constructs.

In the Logic Programming setting, these aspects have been 
investigated by Miller.  His work results in the definition of a
powerful specification language called Forum.
This language is a presentation of full Higher-Order Linear 
Logic, based on a fragment of its set of connectives.

In our current work we are using Forum as a specification language for
object-oriented programming, i.e. we have defined an object
model on top of Forum which can be used as the semantical 
counterpart of o.o. features.

Our aim is to represent in a sequent, the global state of the
computation of an abstract o.o. system (i.e. which can be 
further instantiated to obtain the specification of a real o.o.
programming language). The global state, namely objects and 
messages, flow together in the right-hand side of the
sequents. Class definitions are represented in the left hand-side 
of the sequents as particular re-usable formulas.

We consider an object as a particular higher-order term containing 
both data and methods. Data abstraction is achieved using the 
universal quantification the higher-order variables representing 
the attributes constructors, whose scoping extends over the method
definitions.

Such an approach seems very promising as it shows enough 
flexibility to be applied to different types of o.o. systems.
In this way various dimensions of object-orientation can be 
studied from a logical perpective.

The  functionalities of such systems are specified by a Forum program
which actually plays the role of an inferencial engine over our
representation.

A future application of such a proposal  is to exploit  the 
resulting logical framework to reason about  o.o. program 
properties and in particular to prove their equivalence.


PLACE: 
Seminarraum SEM 181A des Instituts fuer Informationssysteme,
Paniglgasse 16, 1040 Wien, 1.Stock.


------------------------
Christian Doppler Labor fuer Expertensysteme
Technische Universitaet Wien
Paniglgasse 16, A-1040 Wien

Kurt-Goedel-Gesellschaft
Technische Universitaet Wien
Institut fuer Computersprachen E185.2
Resselgasse 3/1, A-1040 Wien

Tel: (+43 1) 588 01/4088
Fax: (+43 1) 504 15 89
email: kgs@logic.tuwien.ac.at

Mit Unterstuetzung des
Bundesministeriums fuer Wissenschaft und Forschung