[Prev][Next][Index][Thread]

ILPS'95 Workshop Announcement


[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]


[This announcement is being sent to various lists. We apologise
for multiple reception of this message.]

	
      Operational & Denotational Semantics of Logic Programming: 
             Extending Proof- and Model-theoretic Analyses
  
                   A workshop in association with
         ILPS'95 (International Logic Programming Symposium)
                      Portland, Oregon (USA)

			Friday, December 8th, 1995

	Logic programming grew out of research into automated theorem
proving. Since Robinson's pioneering work on unification and the
resolution rule, proof-theoretic techniques have been applied to
disjunctive logic programs, negation as failure, higher-order logic
programming and programming languages based on linear logic.  In all
of these, the focus of attention has been the use of proof-theoretic
techniques to define logic programming languages.  For example, the
languages Lygon, $\lambda$Prolog, Lolli, LO, LinLog and ACL have all,
to varying degrees, been based on analyses of the structural
properties of sequent calculi. In addition, programming languages such
as Escher are built very much in the proof-theoretic tradition and
specification languages such as Forum are also founded on
proof-theoretic principles.

        A shortcoming of these techniques is that they do not provide
an adequate basis for understanding the operational semantics of logic
programming languages derived via them: for example, depth-first
search with topmost clause-selection cannot be compared with other
strategies using elementary proof-theoretic techniques alone. In this
respect, logic programming suffers in comparison with functional
programming: the relative merits of call-by-name/value/need can be
usefully analysed using both the operational and denotational
semantics of the $\lambda$-calculus.  What is required is a setting in
which strategies can be formally expressed and their semantics studied
in terms of the semantics of the logical language. Note that least
Herbrand models (and related semantic analyses) are insufficiently
sophisticated be of much help. Indeed, it is well recognized that such
semantic approaches have significant limitations.  Their weakness lies
in their failure to represent adequately the nondeterminism inherent
in search-based computation.

	The aim of this workshop is to bring together researchers in
the areas of proof theory, logic programming language design and
programming language semantics.  At a time when there are many new
developments occurring in each of these disciplines, it is important
that each community be well-informed about the others' progress. In
particluar, we suggest that it is only by such communication that
progress will be made in understanding the design and semantics of
logic programming languages. Moreover, we suggest that both proof
theory and semantics may find challenging new problems arising in
logic programming.

	Another important aspect of this workshop is its potential to
bring together logic and functional programmers via the common grounds
of proof theory and semantics.  Logic programming is often thought of
as interpreting formulae as programs and proof-search (including
unification) as computation, whereas a functional programmer's view of
proof theory is often that a proof is a program and cut-reduction is
computation. Hence a common focus on the applications of proof theory
to programming tasks has the potential not only to explore new logic
programming techniques but also to provide a forum for the integration
of the logic and functional programming paradigms.

	The specific technical issues addressed by this workshop will
include:

	o Proof-theoretic definitions of logic programming languages;
 
	o Proof-theoretic interpretations of aggregate operators,
	     	including negation-as-failure; 

	o Operational semantics of logic programs: requirements 
		and methods;  
       
        o Nondeterminism, process theory and powerdomains: towards 
                a basis for the denotational semantics of logic programming; 
                         
	o Proof theory and (denotational) semantics as common
		frameworks for functional and logic programming.  
	
Submission Guidelines:

	Submissions for presentation at the workshop are invited.
Papers will be subject to peer review.  Papers are to be written in
English, and must not exceed 15 pages (approximately 5000
words). Authors are encouraged to submit papers via email, in either
Postscript or (self-contained) LaTeX/TeX format.  If email is
unavailable or inconvenient, six paper copies should be
submitted. Submissions should include the name, address, fax, and
email address of a contact author.

	Prospective authors are encouraged to send an expression of
interest via email on or before September 1st, including the title and
authors of the paper. Acknowledgements of submitted papers will be
sent via email within three days of receipt. 

Important Dates:

	Intention to submit:	September 1
	Submissions due: 	September 15
	Notification:		October 27
	Final version due:	November 20


Contact address:

	James Harland 
	Department of Computer Science 
 	Royal Melbourne Institute of Technology 
	GPO Box 2476V 
	Melbourne, 3001 
	Australia 
	email: jah@cs.rmit.edu.au 
	phone: +613 9660 2045 
	fax:  +613 9662 1617 

Organizers:

	James Harland
	RMIT, Australia
	jah@cs.rmit.edu.au

	David Pym 
	University of London, UK
	pym@dcs.qmw.ac.uk
	
	
---------------------------------------------------------------- 
Please address administrative mail regarding this mailinglist to
lprolog-request@cis.upenn.edu.  See http://www.cis.upenn.edu/~dale/lProlog.