Horn Logic Denotations and Their Applications

The denotational approach developed for specifying semantics of programming languages is being applied to formally specify software systems. The role of Horn-logic and Constraints as a notation for specifying denotations is also being studied. Coupled with partial evaluation this has numerous applications from building provably correct efficient compilers (sequential or parallelizing), to automatic generation of efficient implementations and abstract interpreters, to checking program correctness, etc. This project is being done in collaboration with University of Copenhagen (Denmark) and Southampton (UK). The research is partially funded by NSF.

Use of Horn Clause Logic to specify denotational semantics is based on the observation that a notation based on Horn Clauses (pure Prolog) and Constraints facilitates inference of program properties, program transformations, etc., much more easily than the Lambda Calculus. Constraints allow one to model time, as well as automatically derive parallelizing compilers from language specifications. Language Syntax can also be very easily specified in Horn Logic.


There are a number of papers written on applications of Horn Clause Denotations to various fields. Work is still in progress on other applications.