Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




Author, Editor

Author(s):

Hanus, Michael

dblp



Editor(s):

Abramsky, S.
Maibaum, T.S.E.

dblp
dblp



BibTeX cite key*:

Hanus91b

Title, Booktitle

Title*:

Parametric Order-Sorted Types in Logic Programming

Booktitle*:

Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT-91)

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:

Brighton, UK

Language:

English

Event Date*
(no longer used):

April, 8-12

Organization:


Event Start Date:

21 May 2019

Event End Date:

21 May 2019

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

494

Number:


Month:


Pages:

181-200

Year*:

1991

VG Wort Pages:


ISBN/ISSN:


Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

This paper proposes a type system for logic programming where types are structured in two ways. Firstly, functions and predicates may be declared with types containing type parameters which are universally quantified over all types. In this case each instance of the type declaration can be used in the logic program. Secondly, types are related by subset inclusions. In this case a function or predicate can be applied to all subtypes of its declared type. While previous proposals for such type systems have strong restrictions on the subtype relation, we assume that the subtype order is specified by Horn clauses for the subtype relation $\leq$. This allows the declaration of a lot of interesting type structures, e.g., type constructors which are monotonic as well as anti-monotonic in their arguments. For instance, parametric order-sorted type structures for logic programs with higher-order predicates can be specified in our framework. This paper presents the declarative and operational semantics
of the typed logic language. The operational semantics requires a unification procedure on well-typed terms. This unification procedure is described by a set of transformation rules which generate a set of type constraints from a given unification problem. The solvability of these type constraints is decidable for particular type structures.


Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:



BibTeX Entry:

@INPROCEEDINGS{Hanus91b,
AUTHOR = {Hanus, Michael},
EDITOR = {Abramsky, S. and Maibaum, T.S.E.},
TITLE = {Parametric Order-Sorted Types in Logic Programming},
BOOKTITLE = {Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT-91)},
PUBLISHER = {Springer},
YEAR = {1991},
VOLUME = {494},
PAGES = {181--200},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Brighton, UK},
}


Entry last modified by Uwe Brahm, 08/25/2014
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
01/14/1995 06:51:41 PM
Revisions
3.
2.
1.
0.
Editor(s)
Uwe Brahm
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Edit Dates
03/15/2001 12:04:53 PM
21/01/95 20:50:24
17/01/95 21:00:52
14/01/95 19:00:53