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.
Papers
There are a number of papers written on applications
of Horn Clause Denotations to various fields. Work is
still in progress on other applications.
-
G. Gupta "Horn Logic Denotations and Their Applications,"
The Logic Programming Paradigm: A 25 year perspective,
Springer Verlag. pp. 127-160.
(Proceedings of Workshop on Current trends and
Future Directions in Logic Programming Research, April '98).
This paper gives an overview of the whole approach.
-
A. Karshmer, G. Gupta, S. Geiger, C. Weaver.
"Reading and Writing Mathematics: The MAVIS Project,"
In Behavior and Information Technology, 1999 18(1):2-10.
-
G. Gupta, E. Pontelli, R. Felix-Cardenas, A. Lara,
"Automatic Derivation of a Parallelizing Compiler,"
In Proc. International Conference on Parallel Processing,
IEEE Press, Aug, 1998, pp. 579-586.
-
G. Gupta, E. Pontelli. "A Constraint-based Approach to
Specification and Verification of Real-time Systems,"
In Proc. IEEE Real-time Symposium, San Francisco, pp. 230-239.
Dec. '97.
-
G. Gupta "Horn Logic Denotations,"
In Proc. 1998 Joint International Conference and Symposium
on Logic Programming, MIT Press, pp. 357-358.
-
L. King, G. Gupta, E. Pontelli.
Verification of BART Controller: An Approach based on Horn
Logic and Denotational Semantics. In High
Integrity Software Systems, Kluwer Academic, to appear.
-
G. Gupta, Building the Tower of Babel:
Converting XML to VoiceXML for Accessibility.
Submitted to 7th International Conference on
Computers Helping People with Special Needs.
-
G. Gupta and E. Pontelli. A Horn Logic Denotational Framework
for Specification, Implementation, and Verification of Domain
Specific Languages, NMSU Tech. Report, 1999.
-
E. Pontelli, D. Ranjan, G. Gupta, B. Milligan.
Philog: A Domain Specific Language for Solving Phylogenetic
Problems in Biology,
. First IEEE Computer Society Bioinformatics conference, 2002.