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 elements of the type system shall support modelling of the application domain. The type system must not be a 'straight-jacket'.
- The type language shall allow static type checking.
- The overhead for writing (and reading) type information in the program shall be rather small. I.e., redundant type information shall be inferred automatically.
- Type computations shall be efficient.
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.
Funding
- Deutsche Forschungsgemeinschaft, Schwerpunktprogramm "Deduktion". See also successor page.