T Y P I C A L
for predicate logic
The aim of Typical is to do static type checking on logic programs.
The software will type-check first-order logic programs
with syntactical conventions used in the
"DFG Schwerpunktprogramm Deduktion"
extended with type declarations.
The type system includes subtyping and parametric
polymorphism. A description of the general idea and of the techniques
for type checking and type inferencing can be found in two technical
reports (see below). This work resulted form research done
withing the DFG-project CTL
Another major application of the Typical approach is
checking standard Prolog programs.
There is a separate page presenting
Typical for annotated Prolog.
README
A few examples of type annotated logic programs:
Software package:
(as tar-archive),
(as zip-archive)
Report `On the Use of Types in Logic Programming'
Abstract,
TeX-dvi,
PostScript,
Cover page,
BibTeX entry
Report `Type Checking and Type Inferencing for Logic Programs with
Subtypes and Parametric Polymorphism'
Abstract,
TeX-dvi,
PostScript,
Cover page,
BibTeX entry
Persons Involved:
[Typical for Annotated Prolog]
Praktische Informatik VIII
Letzte Änderung am 28.05.1998
webmaster