Using modes to ensure subject reduction for typed logic programs with subtyping

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We consider a general prescriptive type system with parametricp olymorphism and subtyping for logic programs. The property of subject reduction expresses the consistency of the type system w.r.t. the execution model: if a program is “well-typed”, then all derivations starting in a “well-typed” goal are again “well-typed”. It is well-established that without subtyping, this property is readily obtained for logicp rograms w.r.t. their standard (untyped) execution model. Here we give syntactic conditions that ensure subject reduction also in the presence of general subtyping relations between type constructors. The idea is to consider logic programs with a fixed dataflow, given by modes.

Original languageEnglish
Title of host publicationFST TCS 2000
Subtitle of host publicationFoundations of Software Technology and Theoretical Computer Science - 20th Conference, Proceedings
EditorsSanjiv Kapoor, Sanjiva Prasad
PublisherSpringer Verlag
Pages214-226
Number of pages13
ISBN (Print)3540414134, 9783540414131
DOIs
Publication statusPublished - 1 Jan 2000
Externally publishedYes
Event20th Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2000 - New Delhi, India
Duration: 13 Dec 200015 Dec 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1974
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2000
Country/TerritoryIndia
CityNew Delhi
Period13/12/0015/12/00

Fingerprint

Dive into the research topics of 'Using modes to ensure subject reduction for typed logic programs with subtyping'. Together they form a unique fingerprint.

Cite this