Startseite › Forschung › Projekte › Compilation of Typed Logics (CTL)

Compilation of Typed Logics (CTL)

A major goal of the project CTL is the combination of logic languages with an expressive type system. Important design criteria are:

The efforts in the project CTL led to the creation of a type system "TYPICAL" which includes parametric polymorphism and subsorts; it allows to write very precise (and nevertheless concise) type declarations. In a first step, the type system has been applied to standard Prolog. Documentation and an implementation of a type checking and inferencing system are available at "TYPICAL for Annotated Prolog". An application of the type system to first order predicate logic including a software prototype for type analysis of programs written in the "DFG-syntax" is available here


Persons Involved