The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #488

Title:A Semantic Approach to Proving Prolog Transformations Using Cut
Authors:Ross,B; Wilk,P
Date:Jul 1990
Presented:Submitted to POPL'91
Keywords:algebraic semantics, control, ccs, prolog, cut
Abstract:An algebraic AND/OR process semantics of sequential Prolog with cut is defined using Milner's's Calculus or Communicating Systems (CCS). This semantics axiomatises the operational semantics at the language level, rather than at a meta-program level. The semantics is hierarchical. A low-level semantics defines the operational semantics of AND/OR processes using CCS formulae. A higher-level semantics, whose definition is justified using the low-level semantics, defines operational behavior at an operator or computation tree level. Some program transformations which make use of cut are verified using This semantics.

[Search These Pages] [DAI Home Page] [Comment]